CONDITIONAL STATEMENT: AN EXAMPLE

 The cond is {x < 0} and we have two cases:

 (Case 1) cond is true. We have:
  x = -x
  { x >= 0 } (Post-condition)
 By backward substitution we obtain:
  { -x >= 0 }
 Therefore,
  { x =<  0 } (clause 1)

 (Case 2) cond is false. We have:
  x = x
  { x >= 0} (Post-condition)
 By backward substitution we obtain:
  { x >= 0} (clause 2)

 By combining the two clauses we obtain the
 Pre-condition, which is {x =< 0} or {x >= 0 }
 Therefore pre-condition is  { true }