Hoare-Logic: Requirements for imperfect data types

Question

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?

Answer 1

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.