S ::= 'while' E 'do' L 'od'
The while-statement executes as long as E>0.
As in other formal semantic methods, the semantics of the while-loop present particular problems.
We must give an inductive definition based on the number of times the loop executes.
Let Hi(while E do L od, Q) be the statement that the loop executes i times and terminates in a state satisfying Q.
Then clearly
H0( while E do L od, Q )
= E ≤ 0 and Q
and
H1( while E do L od, Q )
= E > 0 and wp( L, Q and E ≤ 0 )
= E > 0 and wp( L, H0( while E do L od, Q ) )
Continuing in this fashion we have in general that
Hi+1( while E do L od, Q )
= E > 0 and wp( L, Hi( while E do L od, Q ) )
Now we define
wp( while E do L od, Q )
= there exists an i such that Hi( while E do L od, Q )
Note that this definition of the semantics of the while requires the while-loop to terminate.
Thus, a nonterminating loop always has false as its weakest precondition; that is, it can never make a postcondition true.
For example,
wp( while 1 do L od, Q ) = false, for all L and Q
The semantics we have just given for loops has the drawback that it is very difficult to use in the main application area of axiomatic semantics, namely, the proof of correctness of programs.