ESC/Java: Difference between revisions

Revision as of 01:20, 7 July 2010

Revision as of 01:21, 7 July 2010

Line 2:

'''ESC/Java''' (and more recently '''ESC/Java2'''), the "Extended Static Checker for Java," is a [[programming tool]] that attempts to find common [[run-time error]]s in [[Java (programming language)|Java]] programs through [[extended static checking]]<ref>C. Flanagan, K.R.M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe and R. Stata. "Extended static checking for Java". In ''Proceedings of the Conference on Programming Language Design and Implementation'', pages 234--245, 2002. doi: http://doi.acm.org/10.1145/512529.512558</ref> --- a collective name referring to a range of techniques for [[static code analysis|statically checking]] the correctness of various program constraints. For example, that an integer variable is greater-than-zero, or lies between the [[bounds checking|bounds of an array]]. This technique was pioneered in ESC/Java (and it's predecessor, ESC/Modula-3) and can be thought of as an extended form of [[type system#Type Checking|type checking]]. Extended static checking usually involves the use of an [[automated theorem proving|automated theorem prover]] and, in ESC/Java, the Simplify theorem prover was used.

ESC/Java is neither [[soundness|sound]] nor [[completeness|complete]]. This iswas intentional and aims to reduce the number of errors and/or warnings reported to the programmer, in order to make the tool more useful in practice. However, it does mean that: firstly, there are programs that ESC/Java will erroneously consider to be incorrect (known as false-positives); secondly, there are incorrect programs it will consider to be correct (known false-negatives). Examples in the latter category include errors arising from [[modular arithmetic]] and/or [[multithreading]].

ESC/Java was originally developed at the [[DEC Systems Research Center|Compaq Systems Research Center]] (SRC). SRC launched the project in 1997, after work on their original extended static checker, ESC/Modula-3, ended in 1996. In 2002, SRC released the [[source code]] for ESC/Java and related tools. Recent versions of ESC/Java are based around the [[Java Modeling Language]] (JML). Users can control the amount and kinds of checking by annotating their programs with specially formatted comments or ''[[pragma]]s''.