How to find loop invariant?

Question

I was doing exercise about program verification, and I had some difficulties in finding this loop invariant:

y = 0;
while (y != x) {
    y = y + 1;
}

the precondition is x>=0 and the postcondition is x=y

In the loop there is just one variable so I couldn't think any possible relation that is preserved throughout the program. One weak invariant so far is (y>= 0 && y<=x). So what is the suitable loop invariant for this program?

Answer 1

Let me give you a hint: loop invariants must be expressed in terms of each iteration i. That is, it must be something like "P is true before the execution of every iteration i". The invariant you've come up with is not expressed as a function of i. Try modifying it a little bit and I think you'll find a more suitable loop invariant.

If you get stuck, I recommend you check out the book title "Discrete Mathematics with Applications", by Susanna Epp; it has a chapter on loop invariants and the book is very gentle for beginners.