# I cannot find an invariant for the following program

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.

• The question is unclear to me. Could you try explaining better what you're trying to achieve? You say "I can intuitively tell that this program is partially correct", but we don't know what the problem is supposed to do. Also, you should probably revise the formatting of your code. – Steven Nov 9 at 21:09
• @Steven I made some changes to make it more clear and trying to prove the post condition $y = a*c$ will hold. – Papaya Automata Nov 9 at 21:18
• A variable cannot be an invariant. Only a statement can. A good idea is to write down the values of your variables after the first, second ... Last iteration. Maybe you spot a pattern! – Daniel Nov 9 at 21:20
• Can you prove by induction that after the $i$-th iteration $y= a \cdot i$? – Steven Nov 9 at 21:20