Slide 10.7: General properties of wp
Slide 11.2: Assignment statements
Home

Axiomatic Semantics of a Language

The assertions involved in an axiomatic specificator are primarily statements about the side effects of language constructs; that is, they are statements involving identifiers and environments. For example, the assertion Q = {x > 0} is an assertion about the value of x in an environment. The abstract syntax for which we will define the wp operator is the following: 
     P ::= L
     L ::= S ';' L1 | S
     S ::= I ':=' E
         | 'if'  E  'then'  L1  'else'  L2  'fi'
         | 'while'  E  'do'  L  'od'
Syntax rule such as P ::= L and L ::= S do not need separate specification, since these grammar rules simply state that the wp operator for a program P is the same as for its associated statement-list L, and similarly, if a statement-list L is a single statement S, then L has the same axiomatic semantics as S. The remaining four cases are treated in order. To simplify the description we will suppress the use of quotes.

Statement-lists
For lists of statement separated by a semicolon, we have 
     wp( S ; L1, Q ) = wp( S, wp( L1, Q ) )
This states that the weakest precondition of a series of statements is the composition of the weakest preconditions of its parts. For example, 
   wp( x := x – 2; x := x3, x < 0 )
 = wp( x := x – 2, wp( x := x3, x < 0 ) )
 = wp( x := x – 2, x < 0 )
 = ( x < 2 )
Note that since wp works “backward” the positions of S and L1 are not interchanged, as they are in denotational semantics.