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 )