# Axiomatic Program Verification (Hoare's Method) ## 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:

1. 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
```
2. 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.