Improving JML: For a safer and more effective language

An unusually high number of published JML specifications are invalid or inconsistent, including cases from the security critical area of smart card applications. We claim that these specification errors are due to a mismatch between user expectations and the current JML semantics of expressions over numeric types. At the heart of the problem is JML's language design decision to assign to arithmetic operators the same semantics as in Java. Consequently, JML arithmetic is bounded in precision and more importantly loss of precision occurs stealthily. After a short discussion of JML language design goals and objectives, we introduce JMLa, an adaptation of JML supporting primitive arbitrary precision numeric types. To support our claim that the identified specification errors are due to JML's divergence from user expectations, we demonstrate that the invalidities and inconsistencies disappear under JMLa semantics with either no, or minor syntactic changes to the specifications. Other advantages of JMLa are illustrated including safety-how it allows an automated static checker like ESC/Java to detect more specification and implementation errors. We also briefly illustrate how these issues are applicable to other assertion-based languages like Eiffel.