More Axiomatic Program Verification
OVERVIEW
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