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

- 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

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

{ 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 }

/* 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 }

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

is our notation for saying:alpha(a,i,12)

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

**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)

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

{ 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. axiomand

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

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

- 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