Refinement and retrenchment for programming language data types

Abstract

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 respectively 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 ℤ. 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.