Contributions to the JML project: Safe arithmetic and non-null-by-default

The MultiJava Compiler (MJC) is an extension to the Java programming language that adds open classes and symmetric multiple dispatch. The Java Modeling Language (JML) is a Behavioral Interface Specification Language (BISL) that can be used to specify both simple DBC and full behavioral interface specifications. The JML toolset is based on MJC and contains tools such as the JML (type) checker and the JML Runtime Assertion Checker (RAC). JMLb, is a new version of JML that supports arbitrary precision integers and safe-arithmetic. In this thesis we present the implementation of (bytecode level) support for safe-math integral arithmetic in MJC as well as a performance evaluation of this new version of MJC, in comparison with other Java compilers. Another main enhancement presented in this thesis is the implementation of a non-null statistics gathering tool in the JML checker. An overview of the desugaring process for various kinds of JML method specifications is given. In addition, rules for judging non-null usage are described by presenting examples of different scenarios.