2
$\begingroup$

I am trying to find the weakest precondition and invariant of this while loop. I have read and am trying to understand the concept of calculating preconditions based on postconditions. I was wondering if someone could explain it to me.

while i < j do 
    i = i + 1;
    j = j - 1;
end 

{i = j or i = j + 1}
$\endgroup$
  • $\begingroup$ Loop invariant here is i<j., As you can clearly see. $\endgroup$ – Mr. Sigma. Feb 16 '17 at 7:21
  • 2
    $\begingroup$ @Seeker I doubt that $i<J$ is strong enough as a loop invariant to reach the desired post-condition. $\endgroup$ – Martin Berger Feb 16 '17 at 10:39
  • $\begingroup$ @Martin Don't you think Compliment of what inside {} is loop invariant here? Right? $\endgroup$ – Mr. Sigma. Feb 16 '17 at 10:46
  • $\begingroup$ @Seeker I'm not sure what you mean. $\endgroup$ – Martin Berger Feb 16 '17 at 11:55
  • 1
    $\begingroup$ @Johnny Hmmm, try this with i = 2 and j = 0 ... $\endgroup$ – Martin Berger Mar 2 '17 at 9:59

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.