0
$\begingroup$

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.

Improve this question
$\endgroup$
4
  • 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, 2019 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$
    – KetDog
    Nov 9, 2019 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, 2019 at 21:20
  • 1
    $\begingroup$ Can you prove by induction that after the $i$-th iteration $y= a \cdot i$? $\endgroup$
    – Steven
    Nov 9, 2019 at 21:20

1 Answer 1

Reset to default
3
$\begingroup$

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.

Improve this answer
$\endgroup$
2
  • $\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$
    – KetDog
    Nov 9, 2019 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, 2019 at 0:13

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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