# ESC/Java

> Mediated Wiki article. Canonical URL: https://mediated.wiki/source/ESC%2FJava
> Markdown URL: https://mediated.wiki/source/ESC%2FJava.md
> Source: https://en.wikipedia.org/wiki/ESC%2FJava
> Source revision: 1314788198
> License: Creative Commons Attribution-ShareAlike 4.0 International (https://creativecommons.org/licenses/by-sa/4.0/)

This article includes a list of general references, but it lacks sufficient corresponding inline citations. Please help to improve this article by introducing more precise citations. (March 2010) (Learn how and when to remove this message)

**ESC/Java** (and more recently **ESC/Java2**), the "Extended Static Checker for Java," is a [programming tool](/source/Programming_tool) that attempts to find common [run-time errors](/source/Run-time_error) in [Java](/source/Java_(programming_language)) programs at [compile time](/source/Compile_time).[1] The underlying approach used in ESC/Java is referred to as [extended static checking](/source/Extended_static_checking), which is a collective name referring to a range of techniques for [statically checking](/source/Static_code_analysis) the correctness of various program constraints. For example, that an integer variable is greater-than-zero, or lies between the [bounds of an array](/source/Bounds_checking). This technique was pioneered in ESC/Java (and its predecessor, ESC/[Modula-3](/source/Modula-3)) and can be thought of as an extended form of [type checking](/source/Type_checking). Extended static checking usually involves the use of an [automated theorem prover](/source/Automated_theorem_proving) and, in ESC/Java, the Simplify theorem prover was used.

ESC/Java is neither [sound](/source/Soundness) nor [complete](/source/Completeness_(logic)). 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](/source/Modular_arithmetic) and/or [multithreading](/source/Thread_(computer_science)).

ESC/Java was originally developed at the [Compaq Systems Research Center](/source/DEC_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](/source/Source_code) for ESC/Java and related tools. Recent versions of ESC/Java are based around the [Java Modeling Language](/source/Java_Modeling_Language) (JML). Users can control the amount and kinds of checking by annotating their programs with specially formatted comments or *[pragmas](/source/Directive_(programming))*.

The [University of Nijmegen](/source/Radboud_University_Nijmegen)'s *Security of Systems* group released alpha versions of ESC/Java2, an extended version of ESC/Java that processes the [JML](/source/Java_Modeling_Language) specification language through 2004. From 2004 to 2009, ESC/Java2 development was managed by the KindSoftware Research Group at [University College Dublin](/source/University_College_Dublin), which in 2009 moved to the [IT University of Copenhagen](/source/IT_University_of_Copenhagen), and in 2012 to the [Technical University of Denmark](/source/Technical_University_of_Denmark). Over the years, ESC/Java2 has gained many new features including the ability to reason with multiple [theorem provers](/source/Automated_theorem_prover) and integration with [Eclipse](/source/Eclipse_(software)).

[OpenJML](https://www.openjml.org/), the successor of ESC/Java2, is available for Java 1.8.[2] The source is available at [https://github.com/OpenJML](https://github.com/OpenJML)

[3]

## See also

- [Java Modeling Language](/source/Java_Modeling_Language) (JML)

## References

1. **[^](#cite_ref-1)** Flanagan, C.; Leino, K.R.M.; Lillibridge, M.; [Nelson, G.](/source/Greg_Nelson_(computer_scientist)); [Saxe, J. B.](/source/James_B._Saxe); [Stata, R.](/source/Raymie_Stata) (2002). *Extended static checking for Java*. *Proceedings of the Conference on Programming Language Design and Implementation*. pp. 234–245. [doi](/source/Doi_(identifier)):[10.1145/512529.512558](https://doi.org/10.1145%2F512529.512558). [ISBN](/source/ISBN_(identifier)) [1-58113-463-0](https://en.wikipedia.org/wiki/Special:BookSources/1-58113-463-0).

1. **[^](#cite_ref-2)** ["OpenJML download site on sourceforge"](https://jmlspecs.sourceforge.net/).

1. **[^](#cite_ref-3)** ["Java Modeling Language (JML) / Code / \[r9606\] /OpenJML/Trunk/OpenJML"](https://sourceforge.net/p/jmlspecs/code/HEAD/tree/OpenJML/trunk/OpenJML/).

**Notes**

- Flanagan, C.; Kiniry, K. R. M. (2001). *Houdini, an Annotation Assistant for ESC/Java*. *FME 2001: Formal Methods for Increasing Software Productivity*. Lecture Notes in Computer Science. Vol. 2021. pp. 500–517. [doi](/source/Doi_(identifier)):[10.1007/3-540-45251-6_29](https://doi.org/10.1007%2F3-540-45251-6_29). [ISBN](/source/ISBN_(identifier)) [3-540-41791-5](https://en.wikipedia.org/wiki/Special:BookSources/3-540-41791-5).

- Cataño, N.; Huisman, M. (2002). *Formal Specification and Static Checking of Gemplus' Electronic Purse Using ESC/Java*. *FME 2002:Formal Methods—Getting IT Right*. Lecture Notes in Computer Science. Vol. 2391. pp. 272–289. [doi](/source/Doi_(identifier)):[10.1007/3-540-45614-7_16](https://doi.org/10.1007%2F3-540-45614-7_16). [ISBN](/source/ISBN_(identifier)) [3-540-43928-5](https://en.wikipedia.org/wiki/Special:BookSources/3-540-43928-5).

- Cok, D. R.; Kiniry, J. R. (2005). *ESC/Java2: uniting ESC/Java and JML*. *Proceedings of the 2004 international conference on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices*. Lecture Notes in Computer Science. Vol. 3362. pp. 108–128. [doi](/source/Doi_(identifier)):[10.1007/978-3-540-30569-9_6](https://doi.org/10.1007%2F978-3-540-30569-9_6). [ISBN](/source/ISBN_(identifier)) [3-540-24287-2](https://en.wikipedia.org/wiki/Special:BookSources/3-540-24287-2).

- Chalin, P.; Kiniry, J. R.; Leavens, G. T.; Poll, E. (2006). [*Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2*](https://archive.org/details/formalmethodsfor0000fmco/page/342). *Formal Methods for Components and Objects*. pp. [342–363](https://archive.org/details/formalmethodsfor0000fmco/page/342). [doi](/source/Doi_(identifier)):[10.1007/3-540-45614-7_16](https://doi.org/10.1007%2F3-540-45614-7_16). [ISBN](/source/ISBN_(identifier)) [3-540-36749-7](https://en.wikipedia.org/wiki/Special:BookSources/3-540-36749-7).

- Cok, D. R. (2006). *Specifying java iterators with JML and Esc/Java2*. *Proceedings of the 2006 conference on Specification and verification of component-based systems*. pp. 71–74. [doi](/source/Doi_(identifier)):[10.1145/1181195.1181210](https://doi.org/10.1145%2F1181195.1181210). [ISBN](/source/ISBN_(identifier)) [1-59593-586-X](https://en.wikipedia.org/wiki/Special:BookSources/1-59593-586-X).

- Chalin, P. (2006). *Early detection of JML specification errors using ESC/Java2*. *Proceedings of the 2006 conference on Specification and verification of component-based systems*. pp. 25–32. [doi](/source/Doi_(identifier)):[10.1145/1181195.1181201](https://doi.org/10.1145%2F1181195.1181201). [ISBN](/source/ISBN_(identifier)) [1-59593-586-X](https://en.wikipedia.org/wiki/Special:BookSources/1-59593-586-X).

- Ishikawa, H. (2009). *An Approach for Refactoring using ESC/Java2: A Simple Case Study*. *Proceedings of the 2009 conference on New Trends in Software Methodologies, Tools and Techniques*. pp. 61–72. [ISBN](/source/ISBN_(identifier)) [978-1-60750-049-0](https://en.wikipedia.org/wiki/Special:BookSources/978-1-60750-049-0).

- Poll, E. (2009). [*Teaching Program Specification and Verification Using JML and ESC/Java2*](https://www.cs.ru.nl/~erikpoll/papers/tfm2009.pdf) (PDF). *Proceedings of the 2nd International Conference on Teaching Formal Methods*. Lecture Notes in Computer Science. Vol. 5846. pp. 92–104. [doi](/source/Doi_(identifier)):[10.1007/978-3-642-04912-5_7](https://doi.org/10.1007%2F978-3-642-04912-5_7). [ISBN](/source/ISBN_(identifier)) [978-3-642-04911-8](https://en.wikipedia.org/wiki/Special:BookSources/978-3-642-04911-8).

- James, P. R.; Chalin, P. (2009). *ESC4: a modern caching ESC for Java*. *Proceedings of the 8th international workshop on Specification and verification of component-based systems*. pp. 19–26. [doi](/source/Doi_(identifier)):[10.1145/1596486.1596491](https://doi.org/10.1145%2F1596486.1596491). [ISBN](/source/ISBN_(identifier)) [978-1-60558-680-9](https://en.wikipedia.org/wiki/Special:BookSources/978-1-60558-680-9).

## External links

- [Java Programming Toolkit Source Release](http://www.hpl.hp.com/downloads/crl/jtk/)[*[permanent dead link](https://en.wikipedia.org/wiki/Wikipedia:Link_rot)*]

- [Extended Static Checking for Java](https://web.archive.org/web/20051208055447/http://research.compaq.com/SRC/esc/) at the [Wayback Machine](/source/Wayback_Machine) (archived December 8, 2005)

- [ESC/Java2 at KindSoftware](https://web.archive.org/web/20051231203805/http://www.kindsoftware.com/products/opensource/ESCJava2/)

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

- [Extended Static Checking Modula-3](https://web.archive.org/web/20010228175138/http://research.compaq.com/SRC/esc/escm3/download.html) at the [Wayback Machine](/source/Wayback_Machine) (archived February 28, 2001)

- [Extended Static Checking](https://web.archive.org/web/20071002143846/http://www.researchchannel.org/prog/displayevent.aspx?rID=2761) Computer Science & Engineering Colloquia. University of Washington. 1999.

---
Adapted from the Wikipedia article [ESC/Java](https://en.wikipedia.org/wiki/ESC%2FJava) by Wikipedia contributors ([contributor history](https://en.wikipedia.org/wiki/ESC%2FJava?action=history)). Available under [Creative Commons Attribution-ShareAlike 4.0 International](https://creativecommons.org/licenses/by-sa/4.0/). Changes may have been made.