Wikipedia

ESC/Java

This is an old revision of this page, as edited by Redjamjar (talk | contribs) at 20:45, 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 by static analysis of the program text[1]. ESC/Java sacrifices soundness and completeness in order to reduce the number of false positives (errors reported to the programmer which, in fact, do not exist). The idea is that this makes the tool more likely to be used in practice, since the programmer is not inundated with large volumes of errors and/or warnings.

The underlying technique used in ESC/Java is known as extended static checking. This 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 never 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 system#type checking][type checking]]. Extended static checking usually involves the use of an [[automated theorem proving][automated theorem prover]] and, in ESC/Java, Simplify was used.

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.

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.

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
 

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=372095063"