Extended static checking: Difference between revisions
mNo edit summary |
mNo edit summary |
||
Line 5: | Line 5: | ||
Extended static checkers typically operate by propagating [[predicate transformer semantics#Strongest postcondition|strong postconditions]] (resp. [[predicate transformer semantics#Weakest precondition|weak 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 checkers typically operate by propagating [[predicate transformer semantics#Strongest postcondition|strong postconditions]] (resp. [[predicate transformer semantics#Weakest precondition|weak 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 [[ |
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 the approach, including [[Spec Sharp|Spec#]] and [[SPARK (programming language)|SPARKada]]. However, there is currently no widely used programming language that provides extended static checking. |
||
Revision as of 23:23, 9 July 2010
Extended Static Checking (ESC) is a collective name for a range of techniques for statically checking the correctness of various program constraints[1]. ESC can be thought of as an extended form of type checking. As with type checking, ESC is performed at 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 (reported errors that are, in fact, not errors) at the cost of introducing some false negatives (real errors which are not reported)[2]. ESC can identify a range of errors which are currently outside the scope of a type checker, including division by zero, array out of bounds, integer overflow and null dereferences.
The techniques used in extended static checking come from various fields of Computer Science, including static analysis, model checking, abstract interpretation, SAT solving and automated theorem proving. One key characteristic is that ESC 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- and post-conditions, loop invariants and class invariants.
Extended static checkers typically operate by propagating strong postconditions (resp. weak 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[3] 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 the approach, including Spec# and SPARKada. However, there is currently no widely used programming language that provides extended static checking.
Notes
- ^ 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
- ^ 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
- ^ 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
References
- Extended Static Checking for Java, Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe and Raymie Stata. In Proceedings of the Conference on Programming Language Design and Implementation (PLDI), 2002. doi: http://dx.doi.org/10.1145/512529.512558
- 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
- Improving Computer Security using Extended Static Checking, B. V. Chess. In Proceedings of IEEE Symposium on Security and Privacy, 2002. doi: http://dx.doi.org/10.1109/SECPRI.2002.1004369
- Improving the Quality of Web-based Enterprise Applications with Extended Static Checking: A Case Study, Frédéric Rioux and Patrice Chalin. Electronic Notes in Theoretical Computer Science, 157(2):119–132, 2006. doi: http://dx.doi.org/10.1016/j.entcs.2005.12.050
- Faster and More Complete Extended Static Checking for the Java Modelling Language, Perry R. James, Patrice Chalin. In Journal of Automated Reasoning, 44(1-2):145–174, 2009. doi: http://dx.doi.org/10.1007/s10817-009-9134-9
- Extended Static Checking for Haskell, Dana N. Xu. In Proceedings of the ACM workshop on Haskell, 2006. doi: http://dx.doi.org/10.1145/1159842.1159849
- Extended Static Checking: a Ten-Year Perspective, K Rustan Leino. Informatics, 2001. doi: http://dx.doi.org/10.1007/3-540-44577-3_11
- Extended Static Checking, David L. Detlefs, K. Rustan M. Leino, Greg Nelson, James B. Saxe. Compaq SRC Research Report 159, 1998.