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.