Early detection of JML specification errors using ESC/Java2
- 10 November 2006
- proceedings article
- Published by Association for Computing Machinery (ACM)
Abstract
The earlier errors are found, the less costly they are to fix. This also holds true of errors in specifications. While research into Static Program Verification (SPV) in general, and Extended Static Checking (ESC) in particular, has made great strides in recent years, there is little support for detecting errors in specifications beyond ordinary type checking. This paper reports on recent enhancements that we have made to ESC/Java2, enabling it to report errors in JML specifications due to (method or Java operator) precondition violations and this, at a level of diagnostics that is on par with its ability to report such errors in program code. The enhancements also now make it possible for ESC/Java2 to report errors in specifications for which no corresponding source is available. Applying this new feature to, e.g., the JML specifications of classes in java.*, reveals over 50 errors, including inconsistencies. We describe the adjustment to the assertion semantics necessary to make this possible, and we provide an account of the (rather small) design changes needed to realize the enhancements.Keywords
This publication has 12 references indexed in Scilit:
- Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2Published by Springer Nature ,2006
- How the design of JML accommodates both runtime assertion checking and formal verificationScience of Computer Programming, 2005
- ESC/Java2: Uniting ESC/Java and JMLPublished by Springer Nature ,2005
- The KRAKATOA tool for certificationof JAVA/JAVACARD programs annotated in JMLThe Journal of Logic and Algebraic Programming, 2004
- Extended static checking for JavaPublished by Association for Computing Machinery (ACM) ,2002
- Non-deterministic expressions and predicate transformersInformation Processing Letters, 1997
- Avoiding the undefined by underspecificationPublished by Springer Nature ,1995
- A typed logic of partial functions reconstructed classicallyActa Informatica, 1994
- Two over three: a two-valued logic for software specification and validation over a three-valued predicate calculusJournal of Applied Non-Classical Logics, 1993
- Applying 'design by contract'Computer, 1992