I cannot find an invariant for the following program

Question

I have the following:

(|$y=0; x=c$|) while(x > 0){y=y+a; x=x-1;} (|$y= a*c$|)

This seems like a fairly simple program and I can intuitively tell that the post condition $y=a*c$ is true when the loop terminates, but I cannot a find a good invariant. Of course, I think I can say the variable $a$ is an invariant, but I don't think that it would prove the partial correctness of this program.

Any help is greatly appreciated.

Answer 1

Figure out what the value of y is, depending on x, a, and c. Prove that your formula is correct before the first iteration, and prove that if it is true before an iteration then it is also true after the iteration.