Abstract:

Formalizing Java's Two's-Complement Integral Type in Isabelle/HOL

Nicole Rauch and Burkhart Wolff



We present a formal model of the Java two's-complement integral arithmetics. The model directly formalizes the 
arithmetic operations as given in the Java Language Specification (JLS). The algebraic properties of these 
definitions are derived. Underspecifications and ambiguities in the JLS are pointed out and clarified. The theory 
is formally analyzed in Isabelle/HOL, that is, machine-checked proofs for the ring properties and divisor/
remainder theorems etc. are provided. This work is suited to build the framework for machine-supported 
reasoning over arithmetic formulae in the context of Java source-code verification.