ESC/Java: Difference between revisions

Revision as of 20:45, 6 July 2010

Revision as of 20:47, 6 July 2010

Line 2:

'''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 by [[Static code analysis|static analysis]] of the program text<ref>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</ref>. 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 checking|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 ''[[pragma]]s''.