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?

$\endgroup$
  • $\begingroup$ Try z = xy0 -xy $\endgroup$ – Dmitri Chubarov Nov 23 '17 at 7:37
  • $\begingroup$ @Dmitry Make an answer? $\endgroup$ – Yuval Filmus Nov 24 '17 at 19:06

Your Answer

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

Browse other questions tagged or ask your own question.