We present an approach to integrating the refinement relation between
infinite integer types (used in specification languages) and finite
integer types (used in programming languages) into software
verification calculi.  Since integer types in programming languages
have finite ranges, in general they are not a correct data refinement
of the mathematical integers usually used in specification
languages. Ensuring the correctness of such a refinement requires
generating and verifying additional proof obligations. We tackle this
problem considering Java and UML/OCL as example. We present a
sequent calculus for Java integer arithmetic with integrated
generation of refinement proof obligations.  Thus, there is no
explicit refinement relation, such that the arising complications
remain (as far as possible) hidden from the user. Our approach has
been implemented as part of the KeY system.