Extended static checking (ESC) is a collective name in

computer science Computer science is the study of computation, automation, and information. Computer science spans theoretical disciplines (such as algorithms, theory of computation, information theory, and automation) to practical disciplines (includin ...

for a range of techniques for statically checking the correctness of various program constraints. ESC can be thought of as an extended form of

type checking In computer programming, a type system is a logical system comprising a set of rules that assigns a property called a type to every "term" (a word, phrase, or other set of symbols). Usually the terms are various constructs of a computer program ...

. As with type checking, ESC is performed automatically at

compile time In computer science, compile time (or compile-time) describes the time window during which a computer program is compiled. The term is used as an adjective to describe concepts related to the context of program compilation, as opposed to concept ...

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

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 met ...

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 which are currently outside the scope of a type checker, including

division by zero In mathematics, division by zero is division where the divisor (denominator) is zero. Such a division can be formally expressed as \tfrac, where is the dividend (numerator). In ordinary arithmetic, the expression has no meaning, as there is ...

, array out of bounds,

integer overflow In computer programming, an integer overflow occurs when an arithmetic operation attempts to create a numeric value that is outside of the range that can be represented with a given number of digits – either higher than the maximum or lower t ...

and null dereferences. The techniques used in extended static checking come from various fields of computer science, including

static program analysis In computer science, static program analysis (or static analysis) is the analysis of computer programs performed without executing them, in contrast with dynamic program analysis, which is performed on programs during their execution. The term ...

symbolic simulation In computer science, a simulation is a computation of the execution of some appropriately modelled state-transition system. Typically this process models the complete state of the system at individual points in a discrete linear time frame, comp ...

model checking In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification (also known as correctness). This is typically associated with hardware or software system ...

, abstract interpretation, SAT solving and

automated theorem proving Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was ...

and

. 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 specifications, in the form of pre- and post-conditions,

loop invariant In computer science, a loop invariant is a property of a program loop that is true before (and after) each iteration. It is a logical assertion, sometimes checked within the code by an assertion call. Knowing its invariant(s) is essential in ...

s and

class invariant In computer programming, specifically object-oriented programming, a class invariant (or type invariant) is an invariant used for constraining objects of a class. Methods of the class should preserve the invariant. The class invariant constr ...

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 In mathematics, a divisor of an integer n, also called a factor of n, is an integer m that may be multiplied by some integer to produce n. In this case, one also says that n is a multiple of m. An integer n is divisible or evenly divisible by ...

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 excluded third) 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,

ESC/Java 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 at compile time. The underlying approach used in ESC/Java is referred to as exten ...

. Its roots originate from more simplistic static checking techniques, such as static debugging or

Lint (software) Lint, or a linter, is a static code analysis tool used to flag programming errors, bugs, stylistic errors and suspicious constructs. The term originates from a Unix utility that examined C language source code. History Stephen C. Johnson, a com ...

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

VHDL The VHSIC Hardware Description Language (VHDL) is a hardware description language (HDL) that can model the behavior and structure of digital systems at multiple levels of abstraction, ranging from the system level down to that of logic gat ...

VSPEC. However, there is currently no widely used software programming language that provides extended static checking in its base development environment.

See also

References

Further reading