Slide 11.2: Assignment statements

Slide 11.1: Axiomatic semantics of a language
Slide 11.3: If-statements
Home

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:

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 )