Slide 11.2: Assignment statements
Slide 11.4: While-statements
Home

If-statements 

     S ::= 'if'  E  'then'  L1  'else'  L2  'fi'
Recall that the semantics of the if-statement means that L1 is executed if the value of E>0, and L2 is executed if the value of E≤0. The weakest precondition of this statement is defined as follows: 
   wp( if E then L1 else L2 fi, Q )
 = ( E > 0 → wp( L1, Q ) ) and ( E ≤ 0 → wp( L2, Q ) )
As an example, we compute 
   wp( if x then x := 1 else x := -1 fi, x = 1 )
 = ( x > 0 → wp( x :=  1, x = 1 ) ) and
   ( x ≤ 0 → wp( x := -1, x = 1 ) )
 = ( x > 0 → 1 = 1 ) and ( x ≤ 0 → -1 = 1)
The (P→Q) is the same as (Q or not P). For example, the statement 
  If the river is narrow, then we can cross it quickly.
has the same meaning as 
   The river is not narrow, or we can cross it quickly.
Therefore, we get 
   ( x > 0 → 1 = 1 )
 = ( ( 1 = 1 ) or not ( x > 0 ) )
 = true
   ( x ≤ 0 → -1 = 1 )
 = ( ( -1 = 1 ) or not ( x ≤ 0 ) )
 = ( not ( x ≤ 0 ) )
 = ( x > 0 )
So 
   wp( if x then x := 1 else x := -1 fi, x = 1 )
 = ( x > 0 )