Generating the Invariant

Generating the invariant for this example requires a new trick.

Earlier, the suggestion was given to extract ~B from the postcondition of a loop to get a candidate invariant. This simple suggestion is not sufficient here.

For example, taking POST and extracting ~(k!=0) gives (y = x^n and k=0) which is certainly too strong... in particular k=0 is not invariant as the loop executes.

We need to work loop variables into this INV...

so weaken k = 0 to k >= 0, and then try

   k >= 0 and x^n = y * z^k and x!=0 and z!=0