Definition
Program Proofing
Program proofing (or program verification) is the formal process of proving that a program
is correct with respect to a formal specification.
Methods
Hoare Calculus
Decompose correctness assertions into simpler ones using inference rules until only true statements and valid formulas remain. This method uses the Hoare calculus directly.
Definition
Link to originalHoare Calculus
The Hoare calculus is a calculus for reasoning about the correctness of programs. It uses Hoare triples together with axioms and inference rules to show that a program transforms states satisfying a precondition into states satisfying a postcondition.
Weakest Precondition
Calculate the weakest formula
Definition
Link to originalWeakest Precondition
The weakest precondition of a program
and a postcondition is the most general (least restrictive) formula such that the Hoare triple is totally correct. Equivalently,
characterises exactly the states from which terminates in a state satisfying . If a precondition
implies , then is totally correct.
Strongest Postcondition
Calculate the strongest formula
Definition
Link to originalStrongest Postcondition
The strongest postcondition of a program
and a precondition is the most specific (most restrictive) formula such that the Hoare triple is partially correct. Equivalently, it is the set of states reached by executing
from states satisfying : If a postcondition
is implied by , then is partially correct.