S ::= I ':=' E
The definition of wp for the assignment statement is as follows:
wp( I := E, Q ) = Q[ E/I ]
This rule involves a new notation: Q[E/I], which is defined to be the assertion Q, with E replacing all free occurrences of the identifier I in Q.
An identifier I is free in a logical assertion Q if it is not bound by either the existential quantifier “there exists” ∃ or the universal quantifier “for all” ∀.
Thus, in the following assertion, j is free, but i is bound (and thus not free):
Q = ( for all i, a[i] > a[j] )
In this case Q[1/j] = (for all i, a[i]>a[1]), but Q[1/i] = Q because i is not free.
In commonly occurring assertions, this should not become a problem, and in the absence of quantifiers, one can simply read Q[E/I] as replacing all occurrences of I by E.
The axiomatic semantics wp(I:=E, Q) = Q[E/I] simply says that, for Q to be true after the assignment I := E, whatever Q says about I must be true about E before the assignment is executed.
Two examples of finding the assignment semantics are as follows:
- First, consider the previous example
wp(x:=x+1, x>0).
Here Q = (x>0) and Q[(x+1)/x] = (x+1 > 0).
Thus,
wp( x := x + 1, x > 0 ) = ( x+1 > 0 ) = ( x > -1 )
which is what we obtained before.
- Similarly,
wp( x := x + 1, x = A )
= ( x = A ) [( x + 1 ) / x]
= ( x + 1 = A )
= ( x = A - 1 )