= Formal methods
<Formal methods> use mathematically defined models, specifications and reasoning techniques to describe and analyze systems. They include writing a <formal specification>, proving properties through <formal verification>, exploring a finite model by <model checking> and deriving information through <static program analysis>. A method's guarantee is relative to its model and assumptions.
For example, a loop summing an <array> can maintain the invariant that the current accumulator equals the sum of the entries already visited. Initialization, preservation by one iteration and the exit condition establish the returned sum; a separate <loop variant>[termination argument] shows that an answer is reached. Arithmetic and <array index>[array bounds] must be specified, since a <mathematical proof>[proof] using unbounded <integers> need not describe overflowing <integer arithmetic>[machine arithmetic].<An Axiomatic Basis for Computer Programming by Tony Hoare>[assignment and iteration rules, and reservations about arithmetic and termination]{ref}
Back to article page
