# 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

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.

• So, would y = (c-x) * a be a valid invariant since it holds before the first iteration and after an iteration, and also true after the last iteration. – Papaya Automata Nov 9 at 21:46
• Yes. And because it is true after the last iteration where x = 0, we have y = (c-x)*a = (c-0)*a = c*a after the last iteration. – gnasher729 Nov 10 at 0:13