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.

  • 1
    $\begingroup$ 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. $\endgroup$ – Steven Nov 9 '19 at 21:09
  • $\begingroup$ @Steven I made some changes to make it more clear and trying to prove the post condition $y = a*c$ will hold. $\endgroup$ – Papaya-Automaton Nov 9 '19 at 21:18
  • $\begingroup$ 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! $\endgroup$ – Daniel Nov 9 '19 at 21:20
  • 1
    $\begingroup$ Can you prove by induction that after the $i$-th iteration $y= a \cdot i$? $\endgroup$ – Steven Nov 9 '19 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.

| cite | improve this answer | |
  • $\begingroup$ 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. $\endgroup$ – Papaya-Automaton Nov 9 '19 at 21:46
  • $\begingroup$ 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. $\endgroup$ – gnasher729 Nov 10 '19 at 0:13

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.