1
$\begingroup$ 
(x >= 0 && y >= 0) 
q = 0;
r = x;
while ( r >=y ) { 
  r = r - y;
  q = q + 1;
}
(x = q*y +r) && (r >= 0) && (r < y)

For this what if y = 0 ?

If y = 0, then r stays at r inside the while loop, which makes r >= y true always. So it doesn't seem to terminate.

So I think, for pre-condition, doesn't it have to be (y > 0) to make sure this program terminates ?

Improve this question
$\endgroup$
3
  • $\begingroup$ Could you add if & while clauses to the first and last statements? It's a bit confusing. $\endgroup$
    – Sagnik
    Apr 22, 2018 at 5:58
  • $\begingroup$ If $y=0$ then the loop never terminates. Depending on your semantics of Hoare triples, either this is OK (the loop never terminates, so the postcondition is never falsified) or not (your precondition must ensure that the code terminates). But it just seems like a typo for $y>0$. $\endgroup$
    – Yuval Filmus
    Apr 22, 2018 at 6:07
  • 1
    $\begingroup$ To clarify: Are these partial correctness assertions (typically written with {}) or total correctness assertions (typically written with [])? If they are partial correctness assertions, they don't require the loop terminates; they only describe what needs to happen when it does determine. $\endgroup$
    – Curtis F
    Apr 22, 2018 at 6:20

1 Answer 1

Reset to default
1
$\begingroup$

As mentioned in the comments, it depends on whether you care about partial correctness or total correctness.

Partial correctness requires that, if the program starts from any state satisfying the preconditions, and if the program terminates in a final state, then such final state satisfies the postcondition.

Total correctness requires that, if the program starts from any state satisfying the preconditions, then the program terminates in a final state, which satisfies the postcondition.

Only total correctness requires termination, partial correctness does not.

The Hoare logic rules for program statements are roughly the same, except for while loops. In partial correctness, the while rule requires to find a suitable invariant property. In total correctness, the rule requires both the invariant property and the variant: this is a strictly decreasing, natural valued function of the state (roughly, providing an upper bound on the number of loops).

If your rules have no variant, but only deal with the invariant, they are meant to be used to prove partial correctness, only.

Improve this answer
$\endgroup$

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.