1
$\begingroup$

Given the program:

{y=y0 ^ y>=0}
    z=0;
    while (y>0){
        z=z+x;        (1)
        y=y-1;
    }
{z=x*y0}

I am having trouble finding the invariant, I've tried:

  • z=xy-xy
  • z<=xy
  • z=0xy

with/without the precondition as the invariant, but none of my attempts can be used to prove the post-condition. Any help would be greated appreciated!

Moreover, if the code at (1) is changed to z=z*x;, how should I modify my invariant?

Improve this question
$\endgroup$
2
  • $\begingroup$ Try z = xy0 -xy $\endgroup$
    – Dima Chubarov
    Nov 23, 2017 at 7:37
  • $\begingroup$ @Dmitry Make an answer? $\endgroup$
    – Yuval Filmus
    Nov 24, 2017 at 19:06

0

Reset to default

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.