Formal Design Verification

Formal methods should be part of the education of every computer scientist and software engineer, just as the appropriate branch of applied mathematics is a necessary part of the education of all other engineers. A design can be expressed informally for example, in English, semi-formally for example, as a Petri net, or formally. The formal language is mathematics, although the tools used to create designs expressed in a formal language hide some, if not all, of the mathematics from the user. Formal methods transfer the principles of mathematical reasoning to the specification and implementation of technical systems the completeness, consistency or correctness of a specification or implementation. Formal methods are surprisingly feasible for mainstream software development and give good return on investment. It is difficult to classify cleanly the types of formal languages and tools that are available.