Extended static checking (ESC) is a collective name in
computer science
Computer science is the study of computation, information, and automation. Computer science spans Theoretical computer science, theoretical disciplines (such as algorithms, theory of computation, and information theory) to Applied science, ...
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'' (for example, integer, floating point, string) to every '' term'' (a word, phrase, or other set of symbols). Usu ...
. 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 language's statements are converted into binary instructions for the processor to execute. The term is used as an adjective to describe concepts relat ...
(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 a system with respect to a certain formal specification or property, using formal methods of mathematics.
Formal ver ...
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
division by zero
In mathematics, division by zero, division (mathematics), division where the divisor (denominator) is 0, zero, is a unique and problematic special case. Using fraction notation, the general example can be written as \tfrac a0, where a is the di ...
,
array out of bounds,
integer overflow
In computer programming, an integer overflow occurs when an arithmetic operation on integers 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 maximu ...
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 (also known as static analysis or static simulation) is the analysis of computer programs performed without executing them, in contrast with dynamic program analysis, which is performed on programs duri ...
,
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, compu ...
,
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 syst ...
,
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 pro ...
,
SAT solving
In computer science and formal methods, a SAT solver is a computer program which aims to solve the Boolean satisfiability problem (SAT). On input a formula over Boolean data type, Boolean variables, such as "(''x'' or ''y'') and (''x'' or not ''y'' ...
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 a majo ...
and
type checking
In computer programming, a type system is a logical system comprising a set of rules that assigns a property called a ''type'' (for example, integer, floating point, string) to every '' term'' (a word, phrase, or other set of symbols). Usu ...
. 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
specification
A specification often refers to a set of documented requirements to be satisfied by a material, design, product, or service. A specification is often a type of technical standard.
There are different types of technical or engineering specificati ...
s, 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 with a code assertion. Knowing its invariant(s) is essential in understanding th ...
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 constra ...
s.
Extended static checkers typically operate by propagating
strongest postconditions (respectively
weakest preconditions) 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
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 divisibl ...
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. Its roots originate from more simplistic static checking techniques, such as static debugging
or
lint and
FindBugs. A number of other languages have adopted ESC, including Spec# and
SPARKada and
VHDL
VHDL (Very High Speed Integrated Circuit Program, VHSIC Hardware Description Language) is a hardware description language that can model the behavior and structure of Digital electronics, digital systems at multiple levels of abstraction, ran ...
VSPEC. However, there is currently no widely used software programming language that provides extended static checking in its base development environment.
See also
*
Java Modeling Language (JML)
References
Further reading
*
*
*
*
*
*
*
*
{{DEFAULTSORT:Extended Static Checking
Static program analysis tools
Formal methods