More Axiomatic Program Verification

OVERVIEW

Inference rule for multi-assignment
Example: exponentiation program
Verification method for arrays
Example: array manipulation
Generating new inference rules

AXIOMS: Multi-assignment

We can modify the assignment axiom schema to allow for multiple, simultaneous assignments.

useful in specification

(for some reason) does not generally appear in programming languages.

    { P:x1/v1,...,xn/vn } 
       x1, ..., xn := v1, ..., vn 
    { P }

means calculate all values for the vi's with current values of xi's, then do the substitutions of the new values for the variables.
Order is left to right.
Assume all xi's are distinct...

Duplicates are eliminated using order:

   x, y, x, z := t, w+3, w+t, k

becomes

   y, x, z := w+3, w+t, k

EXAMPLES

    { 12 > 0 and 15 > 0 } 
        x, y := 12, 15 
    { x > 0 and y > 0 }


    { b > a }  /* a swap */  
        a, b := b, a  
    { a > b }


    { m * 5 = 50 and t + 1 = 26 } 
         m, t := m * 5, t + 1 
    { m = 50 and t = 26 }

Consider the difference:

    /* assignment sequence */
    { a = b = c = 10 }
        a := 12
        b := a+4
        c := b*2
    { a = 12 and b = 16 and c = 32 }
 

    /* multi-assignment */
    { a = b = c = 10 }
        a, b, c := 12, a+4, b*2
    { a = 12 and b = 14 and c = 20 }

Proof Example: Exponentiation

This is more complicated example containing while loop, if-then-else, and multi-assignment. Generating the loop invariant also requires a new trick.

VERIFYING PROGRAMS WITH ARRAYS

up to now we have dealt with simple variables, for which textual substitution works fine.
more complicated data structures require new methods of manipulating predicates.
meaning of array expressions depends on the subscript value... simple substitution fails.
Failure example:
```
   { a[3] = 4 } a[i] := 9 { a[3] = 4 }
```
This assertion is obtained with our current assignment axiom schema:
```
   { a[3] = 4 } a[i] := 9 { a[3] = 4 }
```
Since there is no textual occurrance of "a[i]" in the postcondition, it does not change to become the given precondition.
Our assignment axiom says this should be a tautology, a true assertion... However, once a[i] := 9 is executed, we cannot be sure a[3] is still 4... it depends on what value the subscript "i" has when the assignment is executed. So something is wrong here...
We must treat an array as a single entity, like a variable is a single entity... There is no concept of changing "part" of a variable's value.
We treat an array as a function, that is, a mapping from subscript values to element values.
When assign a new value to an array element, a whole new mapping is created, one that is very similar to the mapping started with... keep track of the changes.
Mapping example
```
   a[i] := 12
```
produces a mapping almost exactly like the mapping "a" except that the new mapping takes subscript "i" to the value "12"

Alpha notation

      alpha(a,i,12)

is our notation for saying:

a new mapping is named "alpha(a,i,12)"
this new mapping behaves like the mapping named "a" except at "i", where it returns "12"

This new mapping can be used as an array name is used...

Formal definition:

                        | i != k then x[k]
     alpha(x,i,f)[k] = -|
                        | i = k then f

Another example

    a[i] := 12;
    a[k] := 27;

produces a new mapping

    alpha( alpha(a,i,12), k, 27 )

notation: shorten nested "alphas" by listing the base mapping followed by a list of location/value pairs:
```
   alpha(a,i:12,k:27)
```

ARRAY ASSIGNMENT AXIOMS

These notes about arrays can be summrized by another form of assignment axiom schema ...
For assignment statements with an array element on the left-side:
```
   { P x/alpha(x,i,f) } x[i] := f { P }
```
Good mnemonic:
```
       alpha(x,i,f)
            /  |   \
           x  [i] := f
```
Note: for assignment statement with array element on right-side, the original assignment axioms apply with normal textual substitution...

Examples of Array Assignment Axioms

   { Q: alpha(r,j,14)[j] < alpha(r,j,14)[k] }
       r[j] := 14
   { P: r[j] < r[k] }

Note: the substitution that has occurred is to replace "r" by "alpha(r,j,14)"
the subscript expressions like "[j]" etc. remain unchanged...

Successive assignments:

   { alpha(alpha(b,i,k),j,j+1)[m] = f(x) }
       b[i] := k
   { alpha(b,j,j+1)[m] = f(x) }    by A.A. axiom

and

   { alpha(b,j,j+1)[m] = f(x) }
       b[j] := j + 1
   { b[m] = f(x) }                 by A.A. axiom

so,

   { alpha(alpha(b,i,k),j,j+1)[m] = f(x) }
       b[i] := k
       b[j] := j + 1
   { b[m] = f(x) }                 by Composition

Proof Example: Using Arrays

This program does a left shift of elements in an array.

GENERATING NEW HOARE INFERENCE RULES

language designer must create inference rules for the control structures in a language
draw control structure as a flow graph
annotate the flow graph with information you know to be "true" at various points
start annotations with { P } on incoming arcs
"push" { P } around according to flow graph lines and transform it according to how you know the control structure works.
Examples: repeat-until loop, repeat-while loop, C switch