Mathematics supports abstraction and therefore is a powerful medium for modeling. Because they are exact, mathematical specifications are unambiguous and can be validated to uncover contradictions and incompleteness. It allows a developer to validate a specification for functionality. It is possible to demonstrate that a design matches a specification, and that some program code is a correct reflection of a design
How is the mathematics of formal languages applied in software development? What engineering issues have been addressed by their application? Formal methods are of global concern in software engineering. They are directly applicable during the requirements, design, and coding phases and have important consequences for testing
They have influenced the development and standardization of many programming languages, the programmer’s most basic tool. They are important in ongoing research that may change standard practice, particularly in the areas of
specifications and design methodology. They are entwined with lifecycle models that may provide an alternative to the waterfall model, namely rapid prototyping, the Cleanroom variant on the spiral model, and “transformational” paradigms.
The concept of formalism in formal methods is borrowed from certain trends in 19th and 20th century mathematics. Formal methods are merely an adoption of the axiomatic method, as developed by these trends in mathematics, for software engineering. Mastery of formal methods in software requires an understanding of this mathematics background. Mathematical topics of interest include formal logic, both the propositional calculus and predicate logic, set theory, formal languages, and automata such as finite state machines.