JML Runtime Assertion Checking: Improved Error Reporting and Efficiency Using Strong Validity

Abstract. The Java Modeling Language (JML) recently switched to an assertion semantics based on "strong validity" in which an assertion is taken to be valid precisely when it is defined and true. Elsewhere we have shared our positive experiences with the realization and use of this new semantics in the context of ESC/Java2. In this paper, we describe the challenges faced by and the redesign required for the implementation of the new semantics in the JML Runtime Assertion Checker (RAC) compiler. Not only is the new semantics effective at helping developers identify formerly undetected errors in specifications, we also demonstrate how the realization of the new semantics is more efficient--resulting in more compact instrumented code that runs slightly faster. More importantly, under the new semantics, the JML RAC can now compile sizeable JML annotated Java programs (like ESC/Java2) which it was unable to compile before.

• Type: Conference
• Year: 2008
• Where: FM
• Authors: Patrice Chalin, Frédéric Rioux
• Keywords: Assertion Semantics, FM 2008, Formal Methods, Java Modeling Language, JML Runtime Assertion