Extended static checking

Extended static checking (ESC) is a collective name in <a href="/facts/Computer_science/lN3pEyPz">computer science</a> for a range of techniques for <a href="/facts/Static_code_analysis/b56nr6QM">statically checking</a> the correctness of various program constraints. ESC can be thought of as an extended form of <a href="/facts/Type_checking/Tz0bAMS9">type checking</a>. As with type checking, ESC is performed automatically at <a href="/facts/Compile_time/yCdI3oqn">compile time</a> (i.e. without human intervention). This distinguishes it from more general approaches to the <a href="/facts/Formal_verification/BYD4GnJR">formal verification</a> of software, which typically rely on human-generated proofs. Furthermore, it promotes practicality over soundness, in that it aims to dramatically reduce the number of false positives (overestimated errors that are not real errors, that is, ESC over strictness) at the cost of introducing some false negatives (real ESC underestimation error, but that need no programmer's attention, or are not targeted by ESC). ESC can identify a range of errors that are currently outside the scope of a type checker, including <a href="/facts/Division_by_zero/wXK7t2Ge">division by zero</a>, <a href="/facts/Bounds_checking/vnAjD4Lp">array out of bounds</a>, <a href="/facts/Integer_overflow/sVNnSolT">integer overflow</a> and <a href="/facts/Null_pointer/66zwVEfL">null dereferences</a>.
The techniques used in extended static checking come from various fields of computer science, including <a href="/facts/Static_program_analysis/b56nr6QM">static program analysis</a>, <a href="/facts/Symbolic_simulation/xmMhJP4N">symbolic simulation</a>, <a href="/facts/Model_checking/FwvKMlw9">model checking</a>, <a href="/facts/Abstract_interpretation/cj6wjzu1">abstract interpretation</a>, <a href="/facts/Satisfiability_modulo_theories/10mBFLFB">SAT solving</a> and <a href="/facts/Automated_theorem_proving/vKGvuKFI">automated theorem proving</a> and <a href="/facts/Type_checking/Tz0bAMS9">type checking</a>. Extended static checking is generally performed only at an intraprocedural, rather than interprocedural, level in order to scale to large programs. Furthermore, extended static checking aims to report errors by exploiting user-supplied <a href="/facts/Formal_specification/4q2oDkvS">specifications</a>, in the form of <a href="/facts/Precondition/dWbBdG2e">pre-</a> and <a href="/facts/Postcondition/4tF1Havd">post-conditions</a>, <a href="/facts/Loop_invariant/fIbNgcsI">loop invariants</a> and <a href="/facts/Class_invariant/PqDFHgQy">class invariants</a>.
Extended static checkers typically operate by propagating <a href="/facts/Predicate_transformer_semantics/bxK9TNh7">strongest postconditions</a> (respectively <a href="/facts/Predicate_transformer_semantics/bxK9TNh7">weakest preconditions</a>) intraprocedurally through a method starting from the precondition (respectively postcondition). At each point during this process an intermediate condition is generated that captures what is known at that program point. This is combined with the necessary conditions of the program statement at that point to form a verification condition. An example of this is a statement involving a division, whose necessary condition is that the <a href="/facts/Divisor/DKNa2GvC">divisor</a> be non-zero. The verification condition arising from this effectively states: given the intermediate condition at this point, it must follow that the divisor is non-zero. All verification conditions must be shown to be false (hence correct by means of <a href="/facts/Excluded_third/tDhbugCN">excluded third</a>) in order for a method to pass extended static checking (or "unable to find more errors"). Typically, some form of automated theorem prover is used to discharge verification conditions.
Extended static checking was pioneered in ESC/Modula-3 and, later, <a href="/facts/ESC/Java/xmkTq8NF">ESC/Java</a>. Its roots originate from more simplistic static checking techniques, such as static debugging or <a href="/facts/Lint_(software)/Yjg4pfM5">lint</a> and <a href="/facts/FindBugs/XpckAPDp">FindBugs</a>. A number of other languages have adopted ESC, including Spec# and <a href="/facts/SPARK_(programming_language)/rQB6QTvf">SPARKada</a> and <a href="/facts/VHDL/H6Exdjfs">VHDL</a> VSPEC. However, there is currently no widely used software programming language that provides extended static checking in its base development environment.

Extended static checking open-in-new

Extended static checking