Extended static checking: Difference between revisions

Revision as of 15:41, 2 February 2012

Revision as of 17:17, 2 February 2012

Line 1:

'''Extended static checking''' ('''ESC''') is a collective name for a range of techniques for [[static code analysis|statically checking]] the correctness of various program constraints<ref>C. Flanagan, K.R.M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe and R. Stata. "Extended static checking for Java". In ''Proceedings of the Conference on Programming Language Design and Implementation'', pages 234--245, 2002. doi: http://doi.acm.org/10.1145/512529.512558</ref>. ESC can be thought of as an extended form of [[Type checking|type checking]]. As with type checking, ESC is performed automatically at [[compile time]] (i.e. without human intervention). This distinguishes it from more general approaches to the [[formal verification]] 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'' (overestimated errors that aren't 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 aren't targeted by ESC)<ref name=GNESCUWCSC /><ref>Calysto: Scalable and Precise Extended Static Checking, Domagoj Babic and Alan J. Hu. In Proceedings of the International Conference on Software Engineering (ICSE), 2008. doi: http://dx.doi.org/10.1145/1368088.1368118</ref>. ESC can identify a range of errors which are currently outside the scope of a type checker, including [[division by zero]], [[bounds checking|array out of bounds]], [[integer overflow]] and [[Null pointer|null dereferences]].

The techniques used in extended static checking come from various fields of [[Computer Science]], including [[static analysis]], [[symbolic simulation]], [[model checking]], [[abstract interpretation]], [[satisfiability modulo theories|SAT solving]] and [[automated theorem proving]] and [[type checking]]. One characteristic is that ESC is generally performed only at an intraprocedural level (rather than an interprocedural one) beingapplied a modular checkermodularly, which makes programsESC harderbe able to proofscale andas it makes [[Design by contract]] allowed in such program (stillwith some effort modular soundness can be achieved in some cases by making restrictions in program source code<ref name=GNESCUWCSC>{{Cite web

| title = Extended Static Checking

| work = UWTV

Line 8:

}}</ref>). Furthermore, it aims to report errors by exploiting user-supplied specifications, in the form of [[precondition|pre-]] and [[postcondition|post-conditions]], [[loop invariant]]s and [[class invariant]]s.

Extended static checkers typically operate by propagating [[predicate transformer semantics#Strongest postcondition|strongest postconditions]] (resp. [[predicate transformer semantics#Weakest preconditions|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]] 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<ref>An extended Static Checker for Modula-3, K. Rustan M. Leino and Greg Nelson. In Proceedings of the Conference on Compiler Construction, pages 302--305, 1998. doi: http://dx.doi.org/10.1007/BFb0026418</ref> and, later, [[ESC/Java]]. Its roots originate from more simplistic static checking techniques, such as used in [[Lint (software)]] and [[FindBugs]]. A number of other languages have adopted ESC, including [[Spec Sharp|Spec#]] and [[SPARK (programming language)|SPARKada]] and [[VHDL]] VSPEC. However, there is currently no widely used software programming language that provides extended static checking in its base development environment.

== References ==