Refinement is a well-established and accepted technique for the
systematic development of correct software systems. However, for the
step from already refined specification to implementation, a correct
refinement is often not possible because the data types used in the
specification resp. the implementation language differ.  In this
paper, we discuss this problem and its consequences, using the integer
data types of Java as an example, which do not correctly refine the
mathematical integers Z. We present a solution, which can be seen as a
generalisation of refinement and a variant of retrenchment. It has
successfully been implemented as part of the KeY software verification
system.