ESC/Java

From Wikipedia, the free encyclopedia

This article includes a list ofgeneral references, butit lacks sufficient correspondinginline citations. Please help toimprove this article byintroducing more precise citations.(March 2010) (Learn how and when to remove this message)

ESC/Java (and more recentlyESC/Java2), the "Extended Static Checker for Java," is aprogramming tool that attempts to find commonrun-time errors inJava programs atcompile time.^[1] The underlying approach used in ESC/Java is referred to asextended static checking, which is a collective name referring to a range of techniques forstatically checking the correctness of various program constraints. For example, that an integer variable is greater-than-zero, or lies between thebounds 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 oftype checking. Extended static checking usually involves the use of anautomated theorem prover and, in ESC/Java, the Simplify theorem prover was used.

ESC/Java is neithersound norcomplete. 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 asfalse-positives); secondly, there are incorrect programs it will consider to be correct (known asfalse-negatives). Examples in the latter category include errors arising frommodular arithmetic and/ormultithreading.

ESC/Java was originally developed at theCompaq 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 thesource code for ESC/Java and related tools. Recent versions of ESC/Java are based around theJava Modeling Language (JML). Users can control the amount and kinds of checking by annotating their programs with specially formatted comments orpragmas.

TheUniversity of Nijmegen'sSecurity of Systems group released alpha versions of ESC/Java2, an extended version of ESC/Java that processes theJML specification language through 2004. From 2004 to 2009, ESC/Java2 development was managed by the KindSoftware Research Group atUniversity College Dublin, which in 2009 moved to theIT University of Copenhagen, and in 2012 to theTechnical University of Denmark. Over the years, ESC/Java2 has gained many new features including the ability to reason with multipletheorem provers and integration withEclipse.

OpenJML, the successor of ESC/Java2, is available for Java 1.8.^[2] The source is available athttps://github.com/OpenJML

^[3]

References

[edit]

^Flanagan, C.; Leino, K.R.M.; Lillibridge, M.;Nelson, G.;Saxe, J. B.;Stata, R. (2002).Extended static checking for Java.Proceedings of the Conference on Programming Language Design and Implementation. pp. 234–245.doi:10.1145/512529.512558.ISBN 1-58113-463-0.
^"OpenJML download site on sourceforge".
^"Java Modeling Language (JML) / Code / [r9606] /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:10.1007/3-540-45251-6_29.ISBN 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:10.1007/3-540-45614-7_16.ISBN 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:10.1007/978-3-540-30569-9_6.ISBN 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.Formal Methods for Components and Objects. pp. 342–363.doi:10.1007/3-540-45614-7_16.ISBN 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:10.1145/1181195.1181210.ISBN 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:10.1145/1181195.1181201.ISBN 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 978-1-60750-049-0.
Poll, E. (2009).Teaching Program Specification and Verification Using JML and ESC/Java2(PDF).Proceedings of the 2nd International Conference on Teaching Formal Methods. Lecture Notes in Computer Science. Vol. 5846. pp. 92–104.doi:10.1007/978-3-642-04912-5_7.ISBN 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:10.1145/1596486.1596491.ISBN 978-1-60558-680-9.