Given the program:

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

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?

  • $\begingroup$ Try z = xy0 -xy $\endgroup$ Nov 23, 2017 at 7:37
  • $\begingroup$ @Dmitry Make an answer? $\endgroup$ Nov 24, 2017 at 19:06


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.