Hoare logic is a way of inserting annotations into code to make proofs about program behavior simpler.
//{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:
Definition: for ,
,
Note that this is in general not the same as when relation is non-deterministic.
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:
Let and
be formulas in our language
(see simple programming language). We define Hoare triples on these syntactic entities by taking their interpretation as sets and relations:
means
In words: if we start in a state satisfying and execute
, we obtain a state satisfying
.
We then similarly extend the notion of and
to work on formulas and commands. We use the same notation and infer from the context whether we are dealing with sets and relations or formulas and commands.
We can prove this from