A formal method is a method which makes use of a formal notation or language for specification or mathematical modelling. Systems treated by formal methods have predominantly been information processing systems, but there is no obvious reason why formal methods should be applicable only to the development of information systems. | A formal specification language is a language having a well defined syntax and semantics which is suitable for describing or specifying systems of some kind. Normally programming languages are not considered to be formal specification languages, however precisely their syntax and semantics may be defined, unless they are used for purposes other than writing programs. Some languages may be suitable for use either as programming languages, or as specification languages, for example, pure functional programming languages. |
The rationale for the use of formal specification languages is to facilitate an understanding of the system sufficiently precise to make conclusions drawn about the system more reliable than they otherwise might be. A formal specification supports formal reasoning, which, because it can be checked by machine can be made very reliable indeed. Formal proofs, though, must usually be very detailed. Even with machine support for their construction, formal proofs are liable to require considerable effort to construct and check. |
The use of formal methods for the development of information systems is sometimes advocated by analogy with the use of mathematical techniques in other engineering disciplines.
Because the use of mathematical techniques is pervasive in engineering, it is claimed that the use of formal methods is necessary in Information Systems Engineering for this discipline to achieve the same professional standards as other branches of engineering.
This analogy neglects the important distinction between informal mathematical techniques and formal methods. If they use formal models, Information Systems Engineers go beyond the methods of other engineering disciplines. |
Taking a broad view of formal methods, they are potentially applicable in all engineering disciplines. One reason why all engineering disciplines might benefit from formal methods is that the use of formal descriptions permits machine processing of specifications, which may be beneficial in a variety of ways. |