Jump to content

ESC/Java

Add links
From Wikipedia, the free encyclopedia
This is an old revision of this page, as edited by Redjamjar (talk | contribs) at 21:03, 6 July 2010. The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.

ESC/Java (and more recently ESC/Java2), the "Extended Static Checker for Java," is a programming tool that attempts to find common run-time errors in Java programs through extended static checking[1]. This is a collective name referring to a range of techniques for statically checking the correctness of various program constraints. For example, that an integer variable is greater-than-zero, or lies between the bounds of an array. This technique was pioneered in ESC/Java (and it's 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 prover and, in ESC/Java, the Simplify theorem prover was used.

ESC/Java is neither sound nor complete. This is in 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 false-negatives). Examples in the latter category include errors arising from modular arithmetic and/or multithreading.

ESC/Java was originally developed at the 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 pragmas.

The University of Nijmegen's Security of Systems group released alpha versions of ESC/Java2, an extended version of ESC/Java that processes the JML specification language through 2004. Since 2004, ESC/Java2 development has been managed by the KindSoftware Research Group at University College Dublin. Over the years, ESC/Java2 has gained many new features including the ability to reason with multiple theorem provers and integration with Eclipse.

References

  1. ^ C. Flanagan, K.R.M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe and R. Stata. "Extended static checking for Java". In Proceedings of the Conference on Programming Language Design and Implementation, pages 234--245, 2002. doi: http://doi.acm.org/10.1145/512529.512558
Stub icon

This formal methods-related article is a stub. You can help Wikipedia by expanding it.

Retrieved from "https://en.wikipedia.org/w/index.php?title=ESC/Java&oldid=372098599"