Axiomatic Program Verification (Hoare's Method)

OVERVIEW



AXIOMS, and AXIOMS of ASSIGNMENT

No need to prove axioms... they are axiomatic, they are taken as given... they come from three places

RULES OF INFERENCE



INFERENCE RULE FOR WHILE LOOP

We introduce the notion of an "invariant", an assertion that holds anytime execution is just before evaluation of the boolean expression for the loop.
         { P and B } S { P }
   ---------------------------------
    { P } while B do S { P and ~B }
Our 'invariant' is represented in the schematic as 'P'

The rule says that if P is invariant over one body execution, then it is invariant over the entire life of the loop; also, the loop body is traversed when the boolean is true, and the boolean is false when the entire loop completes.


Example: Remainder Program

We now have enough information to do a simple proof.


INFERENCE RULE FOR CONDITIONAL STATEMENTS

You might find it useful to draw flowcharst of these control structures and annotate them to see how the rules come about.

INFERENCE RULE FOR CASE STATEMENT

Assume in this case the variable C will evaluate to some value in the collection V1, V2, ... Vn:
   forall i (1 <= i <= n ==> { P and C = Vi } Si { Q })
  --------------------------------------------------
    { P } case C of V1: S1; ... Vn: Sn; end { Q }

Here is a version in which the CASE has a default clause, to take effect if the variable C produces a value that is not represented in the CASE:

   forall i ( 1 <= i <= n ==> { P and C = Vi } Si { Q } ) ,
       { P and C!=V1 and C!= V2 and ... and C!=Vn } Sd { Q }
  ----------------------------------------------------- -----
    { P } case C of V1: S1; ... Vn: Sn; default: Sd end { Q }


REPEAT LOOP INFERENCE RULE

Here is the flow diagram for a REPEAT loop. It has been annotated with generic assertions that we know to be true at various points in execution, assuming P is true going into the loop:
   REPEAT S until B 


                        { Q and ~B }
               +--------------------------------+
               |                                | 
               V                                |
    -------------------->[ S ]--------------->< B >--------------->
     { P }       { P }           { Q }                { Q and B }

The inference rule we glean from this annotated flow diagram is as follows:

{ P } S { Q }, (Q and ~B) ==> P
-------------------------------------
{ P } repeat S until B { Q and B }

Another way to get at a rule for REPEAT loops is to unfold the REPEAT into a loop body followed by a WHILE and then apply the WHILE rule and composition/consequence.