Slide 11.3: If-statements
Slide 11.5: Proofs of program correctness
Home

While-statements 

     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.