{ INV and k!=0 and odd(k) } k, y := k - 1, y * z { INV }
{ INV and k!=0 and ~odd(k) } k, z := k/2, z * z { INV }
{INV and k!=0} if odd(k) then... else... {INV}by if-then-else inference rule
{INV} while k!= 0 if-then-else {INV and k=0}by while-loop inference rule