1
$\begingroup$

Theoretically, Hoare-Logic let's one prove the correctness of an algorithm, given pre- and post-condition.

However, as far as I've seen it so far, one idealizes his data-types to a mathematical set like $\mathbb{N}$ or $\mathbb{R}$.

So, even though the logic might be sound in Hoare-calculus, the discrepancies between the data types used and the data types modeled can still fail the result (e.g. Overflow for Integers).

Therefore, the question is:
Which additional conditions have to be met (after each step of the algorithm?) to accomodate for the imperfect data types actually used?

$\endgroup$
3
$\begingroup$

No, when using Hoare logic properly, you make sure to account for integer overflow etc. and model the full semantics of the programming language.

It is possible to use Hoare logic along the lines you suggest, but the problem with that is that it invalidates all guarantees you might have hoped for. Since the whole point of Hoare logic is to obtain guarantees, that seems rather counterproductive.

So if you are using Hoare logic for serious verification, you make sure that the Hoare triples accurately represent all elements of the language semantics, including integer overflow (if relevant). For instance, part of the verification task might be to prove that integer overflow cannot happen; if you don't do that, then the Hoare triples need to account for that possibility.

$\endgroup$
  • $\begingroup$ Yet, neither my lecture (okay, it was beginner level) nor the logic book I informed myself further on Hoare-logic ever even mentioned this problem. That's why I wanted more or less a list of what I have to watch out for $\endgroup$ – Sudix Apr 23 '18 at 14:02
  • $\begingroup$ @Sudix, there is no list, because it depends on the underlying programming language. What you need to do is mirror the semantics of the underlying programming language. That might be very easy or very complex, depending on the language's semantics. It's understandable that the lecture didn't mention this when teaching you the concept, because this is a detail that can be distracting when first trying to learn the basic idea of Hoare logic. $\endgroup$ – D.W. Apr 23 '18 at 14:49

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.