ESC/Java: Difference between revisions

Revision as of 01:22, 7 July 2010

Latest revision as of 02:45, 10 August 2025

(47 intermediate revisions by 30 users not shown)

Line 1:

{{NoMore 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 throughat [[extendedcompile static checkingtime]].<ref>{{cite conference |last1=Flanagan |first1=C. Flanagan,|last2=Leino |first2=K.R.M. Leino,|last3=Lillibridge |first3=M. Lillibridge,|last4=Nelson |first4=G. |author4-link=Greg Nelson, (computer scientist)|last5=Saxe |first5=J. B. Saxe|author5-link=James and RB. Saxe|last6=Stata |first6=R. |author6-link=Raymie "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 it'sits 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 (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]].

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 ''[[pragmaDirective (programming)|pragmas]]s''.

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. SinceFrom 2004 to 2009, ESC/Java2 development has beenwas 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=https://jmlspecs.sourceforge.net/ |title = OpenJML download site on sourceforge}}</ref> The source is available at https://github.com/OpenJML

<ref>{{Cite web|url=https://sourceforge.net/p/jmlspecs/code/HEAD/tree/OpenJML/trunk/OpenJML/|title=Java Modeling Language (JML) / Code / &#91;r9606&#93; /OpenJML/Trunk/OpenJML}}</ref>

== See also ==

*[[Java Modeling Language]] (JML)

== References ==

{{Reflist}}

;Notes

{{refbegin}}

*{{cite conference |last1=Flanagan |first1=C. |last2=Kiniry |first2=K. R. M. |title=Houdini, an Annotation Assistant for ESC/Java |work=FME 2001: Formal Methods for Increasing Software Productivity |series=Lecture Notes in Computer Science |pages=500–517 |year=2001 |volume=2021 |isbn=3-540-41791-5 |doi=10.1007/3-540-45251-6_29}}

*{{cite conference |last1=Cataño |first1=N. |last2=Huisman |first2=M. |title=Formal Specification and Static Checking of Gemplus' Electronic Purse Using ESC/Java |work=FME 2002:Formal Methods—Getting IT Right |series=Lecture Notes in Computer Science |pages=272–289 |year=2002 |volume=2391 |isbn=3-540-43928-5 |doi=10.1007/3-540-45614-7_16}}

*{{cite conference |last1=Cok |first1=D. R. |last2=Kiniry |first2=J. R. |title=ESC/Java2: uniting ESC/Java and JML |work=Proceedings of the 2004 international conference on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices |series=Lecture Notes in Computer Science |pages=108–128 |year=2005 |volume=3362 |isbn=3-540-24287-2 |doi=10.1007/978-3-540-30569-9_6}}

*{{cite conference |last1=Chalin |first1=P. |last2=Kiniry |first2=J. R. |last3=Leavens |first3=G. T. |last4=Poll |first4=E. |title=Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2 |work=Formal Methods for Components and Objects |pages=[https://archive.org/details/formalmethodsfor0000fmco/page/342 342–363] |year=2006 |isbn=3-540-36749-7 |doi=10.1007/3-540-45614-7_16 |url=https://archive.org/details/formalmethodsfor0000fmco/page/342 }}

*{{cite conference |last1=Cok |first1=D. R. |title=Specifying java iterators with JML and Esc/Java2 |work=Proceedings of the 2006 conference on Specification and verification of component-based systems |pages=71–74 |year=2006 |isbn=1-59593-586-X |doi=10.1145/1181195.1181210}}

*{{cite conference |last1=Chalin |first1=P. |title=Early detection of JML specification errors using ESC/Java2 |work=Proceedings of the 2006 conference on Specification and verification of component-based systems |pages=25–32 |year=2006 |isbn=1-59593-586-X |doi=10.1145/1181195.1181201}}

*{{cite conference |last1=Ishikawa |first1=H. |title=An Approach for Refactoring using ESC/Java2: A Simple Case Study |work=Proceedings of the 2009 conference on New Trends in Software Methodologies, Tools and Techniques |pages=61–72 |year=2009 |isbn=978-1-60750-049-0}}

*{{cite conference |last1=Poll |first1=E. |title=Teaching Program Specification and Verification Using JML and ESC/Java2 |work=Proceedings of the 2nd International Conference on Teaching Formal Methods |series=Lecture Notes in Computer Science |pages=92–104 |year=2009 |volume=5846 |isbn=978-3-642-04911-8 |doi=10.1007/978-3-642-04912-5_7 |url=https://www.cs.ru.nl/~erikpoll/papers/tfm2009.pdf}}

*{{cite conference |last1=James |first1=P. R. |last2=Chalin |first2=P. |title=ESC4: a modern caching ESC for Java |work=Proceedings of the 8th international workshop on Specification and verification of component-based systems |pages=19–26 |year=2009 |isbn=978-1-60558-680-9 |doi=10.1145/1596486.1596491}}

{{refend}}

== 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 }}

* [http{{webarchive |url=https://web.archive.org/web/20051208055447/http://research.compaq.com/SRC/esc/ |title=Extended Static Checking for Java] from the|date=December [[Internet8, Archive]]2005}}

* {{usurped|1=[https://web.archive.org/web/20051231203805/http://kindwww.ucdkindsoftware.iecom/products/opensource/ESCJava2/ ESC/Java2 at KindSoftware]}}

* [ftphttps://web.archive.org/web/20070208084515/http://gatekeeper.dec.com:80/pub/DEC/SRC/research-reports/abstracts/src-rr-159.html SRC-RR-159 Extended Static Checking. - David L. Detlefs, K. Rustan M. Leino, Greg Nelson, James B. Saxe]

* [http{{webarchive |url=https://web.archive.org/web/20010228175138/http://research.compaq.com/SRC/esc/escm3/download.html |title=Extended Static Checking Modula-3] from the|date=February [[Internet28, Archive]]2001}}

* {{usurped|1=[https://web.archive.org/web/20071002143846/http://www.researchchannel.org/prog/displayevent.aspx?rID=2761&fID=345 Extended Static Checking]}} Computer Science & Engineering Colloquia. University of Washington. 1999.

{{formalmethods-stub}}

{{DEFAULTSORT:Esc Java}}

[[Category:2002 introductions]]

[[Category:Static2002 code analysissoftware]]

[[Category:Static program analysis tools]]

[[Category:Formal methods tools]]

[[Category:Formal specification languages]]

[[Category:Free computer programming tools]]