formal methods

In computer science, formal methods refers to mathematically based techniques for the specification, development and verification of software and hardware systems (). The role of formal methods in software engineering engenders much controversy.

Taxonomy

As with the sub-discipline of programming language semantics, formal methods may be roughly classified as follows:

Denotational semantics, in which the meaning of a system is expressed as a mathematical function. Proponents of such methods rely on the well-understood nature of functions to give meaning to the system; critics point out that not every system may be intuitively viewed as a function.
Operational semantics, in which the meaning of a system is expressed as a sequence of actions of a (presumably) simpler computational model. Proponents of such methods point to the simplicity of their models as a means to expressive clarity; critics counter that the problem of semantics has just been delayed (who defines the semantics of the simpler model?).
Axiomatic semantics, in which the meaning of the system is expressed in terms of preconditions and postconditions which are true before and after the system performs a task, respectively. Proponents note the connection to classical logic; critics note that such semantics never really describe what a system does (merely what is true before and afterwards).

Uses

Formal methods can be applied at various points through the development process. (For convenience, we use terms common to the waterfall model, though any development process could be used.)

Specification

Formal methods may be used to give a description of the system to be developed, at whatever level(s) of detail desired. This formal description can be used to guide further development activities (see following sections); additionally, it can be used to verify that the requirements for the system being developed have been completely and accurately specified. The need for formal specification systems has been noted for years. In the ALGOL 60 Report, John Backus presented a formal notation for describing programming language syntax (later named Backus normal form (BNF)); Backus also described the need for a notation for describing programming language syntax. The report promised that a new notation, as definitive as BNF, would appear in the near future; it never appeared.

Development

Once a formal specification has been developed, the specification may be used as a guide while the concrete system is developed (i.e. realized in software and/or hardware). Examples:

If the formal specification is in an operational semantics, the observed behavior of the concrete system can be compared with the behavior of the specification (which itself should be executable or simulateable). Additionally, the operational commands of the specification may be ameneable to direct translation into executable code.
If the formal specification is in an axiomatic semantics, the preconditions and postconditions of the specification may become assertions in the executable code.

Verification

Once a formal specification has been developed, the specification may be used as the basis for proving properties of the specification (and hopefully by inference the developed system).