Extended static checking: Difference between revisions

Revision as of 21:08, 10 July 2010

Revision as of 21:09, 10 July 2010

Line 3:

The techniques used in extended static checking come from various fields of [[Computer Science]], including [[static analysis]], [[model checking]], [[abstract interpretation]], [[satisfiability modulo theories|SAT solving]] and [[automated theorem proving]]. One characteristic is that ESC is generally performed only at an intraprocedural level (rather than an [[interprocedural optimization|interprocedural]] one). Furthermore, it aims to report errors by exploiting user-supplied specifications, in the form of [[precondition|pre-]] and [[postcondition|post-conditions]], [[loop invariant|loop invariants]] and [[class invariant|class invariants]].

Extended static checkers typically operate by propagating [[predicate transformer semantics#Strongest postcondition|strongstrongest postconditions]] (resp. [[predicate transformer semantics#Weakest precondition|weakweakest 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 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<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]]. However, there is currently no widely used programming language that provides extended static checking.