Example 2: Proof Plan

OUTLINE OF PROOF

 { PRE: x > 3 }

    if ( x < 25 ) then x := 2 * x

 { POST: x >= 8 }

1. show { PRE and x < 25 } x := 2*x { POST }
2. show PRE and ~(x < 25) ==> POST
3. conclude { PRE } if ... then ... { POST }