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?