Extended Static Checking (ESC) is a collective name for a range of techniques for statically checking

Static code analysis

Static program analysis is the analysis of computer software that is performed without actually executing programs built from that software In most cases the analysis is performed on some version of the source code and in the other cases some form of the object code...

 the correctness of various program constraints. ESC can be thought of as an extended form of type checking. As with type checking, ESC is performed automatically at compile time

Compile time

In computer science, compile time refers to either the operations performed by a compiler , programming language requirements that must be met by source code for it to be successfully compiled , or properties of the program that can be reasoned about at compile time.The operations performed at...

 (i.e. without human intervention). This distinguishes it from more general approaches to the formal verification

Formal verification

In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics .- Usage :Formal verification can be...

 of software, which typically rely on human-generated proofs. Furthermore, it promotes practicality over completeness, in that it aims to dramatically reduce the number of false positives (reported errors that are, in fact, not errors) at the cost of introducing some false negatives (real errors which are not reported). ESC can identify a range of errors which are currently outside the scope of a type checker, including division by zero

Division by zero

In mathematics, division by zero is division where the divisor is zero. Such a division can be formally expressed as a / 0 where a is the dividend . Whether this expression can be assigned a well-defined value depends upon the mathematical setting...

, array out of bounds

Bounds checking

In computer programming, bounds checking is any method of detecting whether a variable is within some bounds before its use. It is particularly relevant to a variable used as an index into an array to ensure its value lies within the bounds of the array...

, integer overflow

Integer overflow

In computer programming, an integer overflow occurs when an arithmetic operation attempts to create a numeric value that is too large to be represented within the available storage space. For instance, adding 1 to the largest value that can be represented constitutes an integer overflow...

 and null dereferences.

The techniques used in extended static checking come from various fields of Computer Science

Computer science

Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...

, including static analysis

Static analysis

Static analysis, static projection, and static scoring are terms for simplified analysis wherein the effect of an immediate change to a system is calculated without respect to the longer term response of the system to that change...

, model checking

Model checking

In computer science, model checking refers to the following problem:Given a model of a system, test automatically whether this model meets a given specification....

, abstract interpretation

Abstract interpretation

In computer science, abstract interpretation is a theory of sound approximation of the semantics of computer programs, based on monotonic functions over ordered sets, especially lattices. It can be viewed as a partial execution of a computer program which gains information about its semantics In...

, SAT solving

Satisfiability Modulo Theories

In computer science, the Satisfiability Modulo Theories problem is a decision problem for logical formulas with respect to combinations of background theories expressed in classical first-order logic with equality...

 and automated theorem proving

Automated theorem proving

Automated theorem proving or automated deduction, currently the most well-developed subfield of automated reasoning , is the proving of mathematical theorems by a computer program.- Decidability of the problem :...

. One characteristic is that ESC is generally performed only at an intraprocedural level (rather than an interprocedural one). Furthermore, it aims to report errors by exploiting user-supplied specifications, in the form of pre-

Precondition

In computer programming, a precondition is a condition or predicate that must always be true just prior to the execution of some section of code or before an operation in a formal specification....

 and post-conditions

Postcondition

In computer programming, a postcondition is a condition or predicate that must always be true just after the execution of some section of code or after an operation in a formal specification. Postconditions are sometimes tested using assertions within the code itself...

, loop invariant

Loop invariant

In computer science, a loop invariant is an invariant used to prove properties of loops. Informally, a loop invariant is a statement of the conditions that should be true on entry into a loop and that are guaranteed to remain true on every iteration of the loop...

s and class invariant

Class invariant

In computer programming, specifically object-oriented programming, a class invariant is an invariant used to constrain objects of a class. Methods of the class should preserve the invariant. The class invariant constrains the state stored in the object....

s.

Extended static checkers typically operate by propagating strongest postconditions (resp. weakest preconditions) intraprocedurally through a method starting from the precondition (resp. 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 divisor

Divisor

In mathematics, a divisor of an integer n, also called a factor of n, is an integer which divides n without leaving a remainder.-Explanation:...

 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 correct in order for a method to pass extended static checking. Typically, some form of automated theorem prover is used to discharge verification conditions.

Extended Static Checking was pioneered in ESC/Modula-3 and, later, ESC/Java

ESC/Java

ESC/Java , the "Extended Static Checker for Java," is a programming tool that attempts to find common run-time errors in Java programs at compile time...

. Its roots originate from more simplistic static checking techniques, such as used in Lint (software) and FindBugs

FindBugs

FindBugs is an open source program created by Bill Pugh and David Hovemeyer which looks for bugs in Java code. It uses static analysis to identify hundreds of different potential types of errors in Java programs. FindBugs operates on Java bytecode, rather than source code. The software is...

. A number of other languages have adopted ESC, including Spec#

Spec sharp

Spec# is a programming language with specification language features that extends the capabilities of the C# programming language with Eiffel-like contracts, including object invariants, preconditions and postconditions. Like ESC/Java, it includes a static checking tool based on a theorem prover...

 and SPARKada. However, there is currently no widely used programming language that provides extended static checking.