Formal methods can be applied at various points through the
development process.
Specification Formal methods may be used to give a formal description of the system to be developed, at whatever level of detail desired. Further formal methods may depend on this specification to synthesize a program or to verify the correctness of a system. Alternatively, specification may be the only stage in which formal methods is used. By writing a specification, ambiguities in the informal requirements can be discovered and resolved. Additionally, engineers can use a formal specification as a reference to guide their development processes. The need for formal specification systems has been noted for years. In the
ALGOL 58 report,
John Backus presented a formal notation for describing
programming language syntax, later named
Backus normal form then renamed
Backus–Naur form (BNF). Backus also wrote that a formal description of the meaning of syntactically valid ALGOL programs was not completed in time for inclusion in the report, stating that it "will be included in a subsequent paper." However, no paper describing the formal semantics was ever released.
Synthesis Program synthesis is the process of automatically creating a program that conforms to a specification. Deductive synthesis approaches rely on a complete formal specification of the program, whereas inductive approaches infer the specification from examples. Synthesizers perform a search over the space of possible programs to find a program consistent with the specification. Because of the size of this search space, developing efficient search algorithms is one of the major challenges in program synthesis.
Verification Formal verification is the use of software tools to prove properties of a formal specification, or to prove that a formal model of a system
implementation satisfies its specification. Once a formal specification has been developed, the specification may be used as the basis for
proving properties of the specification, and by inference, properties of the system implementation.
Sign-off verification Sign-off verification is the use of a formal verification tool that is highly trusted. Such a tool can replace traditional verification methods (the tool may even be certified).
Human-directed proof Sometimes, the motivation for proving the
correctness of a system is not the obvious need for reassurance of the correctness of the system, but a desire to understand the system better. Consequently, some proofs of correctness are produced in the style of
mathematical proof: handwritten (or typeset) using
natural language, using a level of informality common to such proofs. A "good" proof is one that is readable and understandable by other human readers. Critics of such approaches point out that the
ambiguity inherent in natural language allows errors to be undetected in such proofs; often, subtle errors can be present in the low-level details typically overlooked by such proofs. Additionally, the work involved in producing such a good proof requires a high level of mathematical sophistication and expertise.
Automated proof In contrast, there is increasing interest in producing proofs of correctness of such systems by automated means. Automated techniques fall into three general categories: •
Automated theorem proving, in which a system attempts to produce a formal proof from scratch, given a description of the system, a set of logical
axioms, and a set of
inference rules. •
Model checking, in which a system verifies certain properties by means of an exhaustive search of all possible states that a system could enter during its execution. •
Abstract interpretation, in which a system verifies an over-approximation of a behavioural property of the program, using a fixpoint computation over a (possibly complete)
lattice representing it. Some
automated theorem provers require guidance as to which properties are "interesting" enough to pursue, while others work without human intervention. Model checkers can quickly get bogged down in checking millions of uninteresting states if not given a sufficiently abstract model. Proponents of such systems argue that the results have greater mathematical certainty than human-produced proofs, since all the tedious details have been algorithmically verified. The training required to use such systems is also less than that required to produce good mathematical proofs by hand, making the techniques accessible to a wider variety of practitioners. Critics note that some of those systems are like
oracles: they make a pronouncement of truth, yet give no explanation of that truth. There is also the problem of "
verifying the verifier"; if the program that aids in the verification is itself unproven, there may be reason to doubt the soundness of the produced results. Some modern model checking tools produce a "proof log" detailing each step in their proof, making it possible to perform, given suitable tools, independent verification. The main feature of the abstract interpretation approach is that it provides a sound analysis, i.e. no false negatives are returned. Moreover, it is efficiently scalable, by tuning the abstract domain representing the property to be analyzed, and by applying widening operators to get fast convergence. ==Techniques==