Sciweavers

Share
FM
2008
Springer

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

9 years 9 months ago
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.
Patrice Chalin, Frédéric Rioux
Added 26 Oct 2010
Updated 26 Oct 2010
Type Conference
Year 2008
Where FM
Authors Patrice Chalin, Frédéric Rioux
Comments (0)
books