Software Verification with Integrated Data Type Refinement 
for Integer Arithmetic

Bernhard Beckert and Steffen Schlager

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.