ESC/Java: Difference between revisions

Revision as of 21:12, 7 February 2014

Revision as of 13:50, 16 February 2014

Line 4:

<!-- End of AfD message, feel free to edit beyond this point -->

{{More footnotes|date=March 2010}}

'''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 at [[compile time]].<ref>{{cite conference |last1=Flanagan |first1=C. Flanagan,|last2=Leino |first2=K.R.M. Leino,|last3=Lillibridge |first3=M. Lillibridge,|last4=Nelson |first4=G. Nelson,|last5=Saxe |first6=J. B. Saxe and|last6=Stata |first5=R. Stata. "|title=Extended static checking for Java". In ''|work=Proceedings of the Conference on Programming Language Design and Implementation'', |pages=234–245 234|year=2002 |isbn=1-58113-245, 2002. 463-0 |doi: http://doi.acm.org/=10.1145/512529.512558}}</ref> The underlying approach used in ESC/Java is referred to as [[extended static checking]], which is 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 its predecessor, ESC/Modula-3) and can be thought of as an extended form of [[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 was 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 as ''false-negatives''). Examples in the latter category include errors arising from [[modular arithmetic]] and/or [[Thread (computer science)|multithreading]].