usingESCJava2.PDF

Early Detection of JML Specification Errors using ESC/Java2 Patrice Chalin Dept. of Computer Science and Software Engineering, Dependable Software Research Group, Concordia University 1455 de Maisonneuve Blvd. West, Montréal Québec, Canada, H3G 1M8 chalin@cse.concordia.ca ABSTRACT that an error is detected, the less costly it will be to correct. This The earlier errors are found, the less costly they are to fix. This has motivated considerable research in the area of Static Program also holds true of errors in specifications. While research into Verification (SPV) so that today, a variety of approaches and tools Static Program Verification (SPV) in general, and Extended Static are becoming available to developers. In fact, developers can Checking (ESC) in particular, has made great strides in recent already make routine use of tools that effectively eliminate certain years, there is little support for detecting errors in specifications classes of error. One promising technological approach to SPV is beyond ordinary type checking. This paper reports on recent en- Extended Static Checking (ESC) [11]. ESC tools, like ESC/Java2 hancements that we have made to ESC/Java2, enabling it to report [7] and Spec#’s Boogie [8], offer fully automated checking of errors in JML specifications due to (method or Java operator) code against specifications. Despite the fact that automation is precondition violations and this, at a level of diagnostics that is on achieved at the expense of completeness and/or soundness, in par with its ab