# More Axiomatic Program Verification

## 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