ESC/Java

ESC/Java (and more recently ESC/Java2), the "Extended Static Checker for Java," is a <a href="/facts/Programming_tool/wWaFqCFw">programming tool</a> that attempts to find common <a href="/facts/Run-time_error/lCxKsrzB">run-time errors</a> in <a href="/facts/Java_(programming_language)/9ScgFyAL">Java</a> programs at <a href="/facts/Compile_time/yCdI3oqn">compile time</a>. The underlying approach used in ESC/Java is referred to as <a href="/facts/Extended_static_checking/sgYcjRlB">extended static checking</a>, which is a collective name referring to a range of techniques for <a href="/facts/Static_code_analysis/b56nr6QM">statically checking</a> the correctness of various program constraints. For example, that an integer variable is greater-than-zero, or lies between the <a href="/facts/Bounds_checking/vnAjD4Lp">bounds of an array</a>. This technique was pioneered in ESC/Java (and its predecessor, ESC/<a href="/facts/Modula-3/RbblULyn">Modula-3</a>) and can be thought of as an extended form of <a href="/facts/Type_checking/Tz0bAMS9">type checking</a>. Extended static checking usually involves the use of an <a href="/facts/Automated_theorem_proving/vKGvuKFI">automated theorem prover</a> and, in ESC/Java, the Simplify theorem prover was used.
ESC/Java is neither <a href="/facts/Soundness/ndpamd2A">sound</a> nor <a href="/facts/Completeness_(logic)/GzK9zLnu">complete</a>. 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 <a href="/facts/Modular_arithmetic/0wtRa5dU">modular arithmetic</a> and/or <a href="/facts/Thread_(computer_science)/hh8WHyPd">multithreading</a>.
ESC/Java was originally developed at the <a href="/facts/DEC_Systems_Research_Center/0CY4jU3q">Compaq Systems Research Center</a> (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 <a href="/facts/Source_code/o9J6Jv23">source code</a> for ESC/Java and related tools. Recent versions of ESC/Java are based around the <a href="/facts/Java_Modeling_Language/q3RNMJU6">Java Modeling Language</a> (JML). Users can control the amount and kinds of checking by annotating their programs with specially formatted comments or <a href="/facts/Directive_(programming)/RsozxGG0">pragmas</a>.
The <a href="/facts/Radboud_University_Nijmegen/HzHJcIWX">University of Nijmegen</a>'s Security of Systems group released alpha versions of ESC/Java2, an extended version of ESC/Java that processes the <a href="/facts/Java_Modeling_Language/q3RNMJU6">JML</a> specification language through 2004. From 2004 to 2009, ESC/Java2 development was managed by the KindSoftware Research Group at <a href="/facts/University_College_Dublin/RN0ffSeS">University College Dublin</a>, which in 2009 moved to the <a href="/facts/IT_University_of_Copenhagen/6ulkmFUb">IT University of Copenhagen</a>, and in 2012 to the <a href="/facts/Technical_University_of_Denmark/vLv1zoBQ">Technical University of Denmark</a>. Over the years, ESC/Java2 has gained many new features including the ability to reason with multiple <a href="/facts/Automated_theorem_prover/vKGvuKFI">theorem provers</a> and integration with <a href="/facts/Eclipse_(software)/YoqHVjas">Eclipse</a>.
<a href="http://www.openjml.org/">OpenJML</a>, the successor of ESC/Java2, is available for Java 1.8. The source is available at <a href="https://github.com/OpenJML">https://github.com/OpenJML</a>

ESC/Java open-in-new

ESC/Java