Content deleted Content added
Citation bot (talk | contribs) Add: volume, series. | Use this bot. Report bugs. | Suggested by Dominic3203 | Category:Free computer programming tools | #UCB_Category 19/31 |
m Undid revision 1305049123 by Bender the Bot (talk) bot error fixed |
||
| (7 intermediate revisions by 6 users not shown) | |||
Line 1:
{{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. |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.
ESC/Java is neither [[soundness|sound]] nor [[completeness (logic)|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]].
Line 8:
The [[Radboud University Nijmegen|University of Nijmegen]]'s ''Security of Systems'' group released alpha versions of ESC/Java2, an extended version of ESC/Java that processes the [[Java Modeling Language|JML]] specification language through 2004. From 2004 to 2009, ESC/Java2 development was managed by the KindSoftware Research Group at [[University College Dublin]], which in 2009 moved to the [[IT University of Copenhagen]], and in 2012 to the [[Technical University of Denmark]]. Over the years, ESC/Java2 has gained many new features including the ability to reason with multiple [[Automated theorem prover|theorem prover]]s and integration with [[Eclipse (software)|Eclipse]].
[http://www.openjml.org/ OpenJML], the successor of ESC/Java2, is available for Java 1.8.<ref>{{cite web |url=
<ref>{{Cite web|url=https://sourceforge.net/p/jmlspecs/code/HEAD/tree/OpenJML/trunk/OpenJML/|title=Java Modeling Language (JML) / Code / [r9606] /OpenJML/Trunk/OpenJML}}</ref>
Line 31:
== External links ==
* [http://www.hpl.hp.com/downloads/crl/jtk/ Java Programming Toolkit Source Release]{{Dead link|date=July 2025 |bot=InternetArchiveBot |fix-attempted=yes }}
* {{webarchive |url=https://web.archive.org/web/20051208055447/http://research.compaq.com/SRC/esc/ |title=Extended Static Checking for Java |date=December 8, 2005}}
* {{usurped|1=[https://web.archive.org/web/20051231203805/http://www.kindsoftware.com/products/opensource/ESCJava2/ ESC/Java2 at KindSoftware]}}
* [
* {{webarchive |url=https://web.archive.org/web/20010228175138/http://research.compaq.com/SRC/esc/escm3/download.html |title=Extended Static Checking Modula-3 |date=February 28, 2001}}
* {{usurped|1=[https://web.archive.org/web/20071002143846/http://www.researchchannel.org/prog/displayevent.aspx?rID=2761 Extended Static Checking]}} Computer Science & Engineering Colloquia. University of Washington. 1999.
{{DEFAULTSORT:Esc Java}}
| |||