Proof Plan

• Generate the invariant INV and show it is invariant for the loop, that is, show

    { INV and k < b } loop_body { INV }
  

• show

    { PRE } k := a { INV }
  

  which means

    show { INV' } k := a { INV }
     and PRE ==> INV'
  

• show

    INV and ~(k < b) ==> POST
  

• use composition t glue it all together into

    { PRE } program { POST }