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 ?

$\endgroup$
  • $\begingroup$ Could you add if & while clauses to the first and last statements? It's a bit confusing. $\endgroup$ – Sagnik Apr 22 '18 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 '18 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 '18 at 6:20
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.

$\endgroup$

Your Answer

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