Formal Methods
Formal methods is the term applied to the analysis of software (and computer hardware) whose results are obtained purely through the use of rigorous mathematical methods. The mathematical techniques used include denotational semantics, axiomatic semantics, operational semantics, and abstract interpretation.
By a straightforward reduction to the halting problem it is possible to prove that (for any Turing complete language) finding all possible run-time errors in an arbitrary program (or more generally any kind of violation of a specification on the final result of a program) is undecidable: there is no mechanical method that can always answer truthfully whether a given program may or may not exhibit runtime errors. This result dates from the works of Church, Gödel and Turing in the 1930s (see the halting problem and Rice's theorem). As with many undecidable questions, one can still attempt to give useful approximate solutions.
Some of the implementation techniques of formal static analysis include:
- Model checking considers systems that have finite state or may be reduced to finite state by abstraction;
- Data-flow analysis is a lattice-based technique for gathering information about the possible set of values;
- Abstract interpretation models the effect that every statement has on the state of an abstract machine (i.e., it 'executes' the software based on the mathematical properties of each statement and declaration). This abstract machine over-approximates the behaviours of the system: the abstract system is thus made simpler to analyze, at the expense of incompleteness (not every property true of the original system is true of the abstract system). If properly done, though, abstract interpretation is sound (every property true of the abstract system can be mapped to a true property of the original system). The Frama-c value analysis plugin and Polyspace heavily rely on abstract interpretation.
- Use of assertions in program code as first suggested by Hoare logic. There is tool support for some programming languages (e.g., the SPARK programming language (a subset of Ada) and the Java Modeling Language — JML — using ESC/Java and ESC/Java2, Frama-c WP (weakest precondition) plugin for the C language extended with ACSL (ANSI/ISO C Specification Language) ).
Read more about this topic: Static Program Analysis
Famous quotes containing the words formal and/or methods:
“It is in the nature of allegory, as opposed to symbolism, to beg the question of absolute reality. The allegorist avails himself of a formal correspondence between “ideas” and “things,” both of which he assumes as given; he need not inquire whether either sphere is “real” or whether, in the final analysis, reality consists in their interaction.”
—Charles, Jr. Feidelson, U.S. educator, critic. Symbolism and American Literature, ch. 1, University of Chicago Press (1953)
“The philosopher is in advance of his age even in the outward form of his life. He is not fed, sheltered, clothed, warmed, like his contemporaries. How can a man be a philosopher and not maintain his vital heat by better methods than other men?”
—Henry David Thoreau (1817–1862)