Loop Body Plan

• prove "true" path in if-then-else

    { INV and k!=0 and odd(k) } 
        k, y := k - 1, y * z 
    { INV }
  

• prove "false" path in if-then-else

    { INV and k!=0 and ~odd(k) } 
        k, z := k/2, z * z 
    { INV }
  

• conclude

    {INV and k!=0} if odd(k) then... else... {INV}
  

  by if-then-else inference rule

• conclude

    {INV} while k!= 0 if-then-else {INV and k=0}
  

  by while-loop inference rule