Assignment Statements


     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: