Axiomatic Program Verification (Hoare's Method)

OVERVIEW

Axioms of assignment
Supporting inference rules
Inference rule for WHILE loop
Proof example: Remainder program
IF-THEN-ELSE inference rules
CASE inference rules
REPEAT loop inference rule

AXIOMS, and AXIOMS of ASSIGNMENT

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

Arithmetic, etc... as we expect from previous math
Assignment (axiom schemata}
```
{ P:x/f }  x := f  { P }
```
- The P:x/f notation means 'take P, find all free textual occurances of 'x' and replace them textually with 'f'
- The axiom states that whatever is true of 'f' before assignment is true of 'x' after.
- Assignment axioms capture the essence of how an imperative programming language does its work.
- Examples
```
  { 12 < 100 } d := 12 { d < 100 }

  { (3+r*z) >= 0 and m < (3+r*z) }
        k := 3 + r * z
  { k >= 0 and m < k }
```
Constraints from a system or an implementation. For example,
```
   exists x ( forall y ( y <= x ) )
```
says there is MAXINT in your language.

RULES OF INFERENCE

one for each control structure
some extra for simplification of argument

Composition

Allows two Hoare triples to be "glued together" if they share a common pre- and post- condition.

    { P } S1 { Q },  { Q } S2 { R }
   ----------------------------------
          { P } S1; S2 { R }

Example:

   { 10 < 20 } a := 10     { a < 20 }
   { a < 20 }  a := a + 5  { a < 25 }

can be combined:

   { 10 < 20 }  a := 10; a := a + 5  { a < 25 }

Consequence

Allows two "back to back" assertions to be glued together. There are two forms of this rule:

We can 'strengthen' (restrict) a precondition

    { Q } S { R },  P ==> Q
   --------------------------
         { P } S { R }

Examples:

   { y + 5 > 10 } x := y + 5 { x > 10}  
      can become  { y > 5 } x := y + 5 { x > 10 } 
      since       y > 5 ==> y + 5 > 10

   { y + 5 > 10 } x := y + 5 { x > 10 }  
      can become  { y + 5 > 15 } x := y + 5 { x > 10 } 
      since       y + 5 > 15 ==> y + 5 > 10

We can 'weaken' (relax) a postcondition

   { P } S { Q },  Q ==> R
   --------------------------
        { P } S { R }

Example:

   { x > 100 } x := x + 12 { x > 112 }
       can become  { x > 100 } x := x + 12 { x > 0 }
       since       x > 112 ==> x > 0

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.

If-then

   { P and B } S { Q },  (P and ~B) ==> Q
   ----------------------------------------
          { P } if B then S { Q }

Examle of use in a proof.

If-then-else

   { P and B } S1 { Q },  { P and ~B } S2 { Q }
   ----------------------------------------------
        { P } if B then S1 else S2 { Q }

Examle of use in a proof.

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.