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!=0eventually k becomes 0, so z^k becomes 1, and then y = x^n.