ESC/Java: Difference between revisions

Revision as of 23:29, 5 July 2025

Revision as of 23:30, 5 July 2025

Line 1:

{{More footnotes|date=body{font:Helvetica,Arial,sans-serif}a{color:#333}a:hover{color:hsl(0,0%,36%)}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. |last2=Leino |first2=K.R.M. |last3=Lillibridge |first3=M. |last4=Nelson |first4=G. |author4-link=Greg Nelson (computer scientist)|last5=Saxe |first5=J. B. |author5-link=James B. Saxe|last6=Stata |first6=R. |author6-link=Raymie Stata|title=Extended static checking for Java |work=Proceedings of the Conference on Programming Language Design and Implementation |pages=234–245 |year=2002 |isbn=1-58113-463-0 |doi=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.