Hoare logic is a way of inserting annotations into code to make proofs about program behavior simpler. We first explain them using sets and relations.
//{0 <= y} i = y; //{0 <= y & i = y} r = 0; //{0 <= y & i = y & r = 0} while //{r = (y-i)*x & 0 <= i} (i > 0) ( //{r = (y-i)*x & 0 < i} r = r + x; //{r = (y-i+1)*x & 0 < i} i = i - 1 //{r = (y-i)*x & 0 <= i} ) //{r = x * y}
When (sets of states) and (relation on states, command semantics) then Hoare triple
means
We call precondition and postcondition.
Note: weakest conditions (predicates) correspond to largest sets; strongest conditions (predicates) correspond to smallest sets that satisfy a given property (Graphically, a stronger condition denotes one quadrant in plane, whereas a weaker condition denotes the entire half-plane.)
is the the smallest set such that , that is:
If we have a relation and a set of errors , we can check if program meets specification by checking:
In other words, we obtain an upper bound on the set of states from which we do not reach error. We next introduce the notion of weakest precondition, which allows us to express from given as complement of error states .
Definition: for , ,
Note that this is in general not the same as when then relation is non-deterministic or partial.
is the largest set such that , that is:
We next list several more lemmas on properties of wp, sp, and Hoare triples.
If instead of good states we look at the completement set of “error states”, then corresponds to doing backwards. In other words, we have the following:
The following three conditions are equivalent:
The condition
is equivalent to
If and then also .
We write this as the following inference rule:
The following inference rule holds:
Proof is by transitivity.
By Expanding Paths condition above, we then have:
In fact, , so we have
This is the rule for non-deterministic loops.