Extended static checking: Difference between revisions

Content deleted Content added

Inline

Latest revision as of 14:29, 29 September 2023

Extended static checking (ESC) is a collective name in computer science 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 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 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).^[2]^[3] ESC can identify a range of errors that 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 program analysis, symbolic simulation, model checking, abstract interpretation, SAT solving and automated theorem proving and type checking. Extended static checking is generally performed only at an intraprocedural, rather than interprocedural, level in order to scale to large programs.^[2] Furthermore, extended static checking 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 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 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^[4] and, later, ESC/Java. Its roots originate from more simplistic static checking techniques, such as static debugging^[5] or lint and FindBugs. A number of other languages have adopted ESC, including Spec# and 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

^ 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
^ ^a ^b "Extended Static Checking". UWTV. Retrieved 2012-02-01.^{[permanent dead link‍]}
^ Babic, Domagoj; Hu, Alan J. (2008). Calysto: Scalable and Precise Extended Static Checking. Proceedings of the International Conference on Software Engineering (ICSE). ACM Press. doi:10.1145/1368088.1368118.
^ Rustan, K.; Leino, M.; Nelson, Greg (1998). "An extended static checker for modula-3". Lecture Notes in Computer Science - International Conference on Compiler Construction. Springer. pp. 302–305. doi:10.1007/bfb0026441. ISBN 978-3-540-64304-3. ISSN 0302-9743.
^ Flanagan, Cormac; Flatt, Matthew; Krishnamurthi, Shriram; Weirich, Stephanie; Felleisen, Matthias (1996). "Catching bugs in the web of program invariants" (PDF). ACM SIGPLAN Notices. 31 (5). Association for Computing Machinery (ACM): 23–32. doi:10.1145/249069.231387. ISSN 0362-1340.

Cormac Flanagan; K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, Raymie Stata (2002). "Extended static checking for Java". Proceedings of the ACM SIGPLAN 2002 conference on Programming language design and implementation. p. 234. doi:10.1145/512529.512558. ISBN 978-1581134636. S2CID 47141042.{{cite book}}: CS1 maint: multiple names: authors list (link)
Babic, Domagoj; Hu, Alan J. (2008). "Calysto". Proceedings of the 13th international conference on Software engineering - ICSE '08. p. 211. doi:10.1145/1368088.1368118. ISBN 9781605580791. S2CID 62868643.
Chess, B.V. (2002). "Improving computer security using extended static checking". Proceedings 2002 IEEE Symposium on Security and Privacy. pp. 160–173. CiteSeerX 10.1.1.15.2090. doi:10.1109/SECPRI.2002.1004369. ISBN 978-0-7695-1543-4. S2CID 12067758.
Rioux, Frédéric; Chalin, Patrice (2006). "Improving the Quality of Web-based Enterprise Applications with Extended Static Checking: A Case Study". Electronic Notes in Theoretical Computer Science. 157 (2): 119–132. doi:10.1016/j.entcs.2005.12.050. ISSN 1571-0661.
James, Perry R.; Chalin, Patrice (2009). "Faster and More Complete Extended Static Checking for the Java Modeling Language". Journal of Automated Reasoning. 44 (1–2): 145–174. CiteSeerX 10.1.1.165.7920. doi:10.1007/s10817-009-9134-9. ISSN 0168-7433. S2CID 14996225.
Xu, Dana N. (2006). "Extended static checking for haskell". Proceedings of the 2006 ACM SIGPLAN workshop on Haskell. p. 48. CiteSeerX 10.1.1.377.3777. doi:10.1145/1159842.1159849. ISBN 978-1595934895. S2CID 1340468.
Leino, K. Rustan M. (2001). "Extended Static Checking: A Ten-Year Perspective". Informatics. Lecture Notes in Computer Science. Vol. 2000. pp. 157–175. doi:10.1007/3-540-44577-3_11. ISBN 978-3-540-41635-7.
Detlefs, David L.; Leino, K. Rustan M.; Nelson, Greg; Saxe, James B. (1998). "Extended Static Checking". Compaq SRC Research Report (159).

[1] 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

[GNESCUWCSC-2] "Extended Static Checking". UWTV. Retrieved 2012-02-01.^{[permanent dead link‍]}

[3] Babic, Domagoj; Hu, Alan J. (2008). Calysto: Scalable and Precise Extended Static Checking. Proceedings of the International Conference on Software Engineering (ICSE). ACM Press. doi:10.1145/1368088.1368118.

[4] Rustan, K.; Leino, M.; Nelson, Greg (1998). "An extended static checker for modula-3". Lecture Notes in Computer Science - International Conference on Compiler Construction. Springer. pp. 302–305. doi:10.1007/bfb0026441. ISBN 978-3-540-64304-3. ISSN 0302-9743.

[5] Flanagan, Cormac; Flatt, Matthew; Krishnamurthi, Shriram; Weirich, Stephanie; Felleisen, Matthias (1996). "Catching bugs in the web of program invariants" (PDF). ACM SIGPLAN Notices. 31 (5). Association for Computing Machinery (ACM): 23–32. doi:10.1145/249069.231387. ISSN 0362-1340.

[1]

[2]

[3]

[4]

[5]

@@ Line 1: / 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]].  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]].
+'''Extended static checking''' ('''ESC''') is a collective name in [[computer science]] 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, [[James B. Saxe|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]]. 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 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).<ref name=GNESCUWCSC /><ref>{{cite conference | last1=Babic | first1=Domagoj | last2=Hu | first2=Alan J. | title=Calysto: Scalable and Precise Extended Static Checking | publisher=ACM Press | conference=Proceedings of the International Conference on Software Engineering (ICSE)| year=2008 | doi=10.1145/1368088.1368118 | page=}}</ref> ESC can identify a range of errors that 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) applied modularly, which makes ESC be able to scale as it makes [[Design by contract]] allowed in such program (with some effort modular soundness can be achieved in some cases by making restrictions in program source code<ref name=GNESCUWCSC>{{Cite web
+The techniques used in extended static checking come from various fields of computer science, including [[static program analysis]], [[symbolic simulation]], [[model checking]], [[abstract interpretation]], [[satisfiability modulo theories|SAT solving]] and [[automated theorem proving]] and [[type checking]]. Extended static checking is generally performed only at an intraprocedural, rather than interprocedural, level in order to scale to large programs.<ref name=GNESCUWCSC>{{Cite web
 | title = Extended Static Checking
 | work = UWTV
 | accessdate = 2012-02-01
 | url = http://stage.uwtv.org/video/player.aspx?mediaid=1577083988
-}}</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.
+}}{{Dead link|date=August 2019 |bot=InternetArchiveBot |fix-attempted=yes }}</ref> Furthermore, extended static checking aims to report errors by exploiting user-supplied [[Formal specification|specification]]s, 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 checkers typically operate by propagating [[predicate transformer semantics#Strongest postcondition|strongest postconditions]] (respectively [[predicate transformer semantics#Weakest preconditions|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]] 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.
+Extended static checking was pioneered in ESC/Modula-3<ref>{{cite book | last1=Rustan | first1=K. | last2=Leino | first2=M. | last3=Nelson | first3=Greg | title=Lecture Notes in Computer Science - International Conference on Compiler Construction| chapter=An extended static checker for modula-3 | publisher=Springer| year=1998 | isbn=978-3-540-64304-3 | issn=0302-9743 | doi=10.1007/bfb0026441|doi-access=free | pages=302–305}}</ref> and, later, [[ESC/Java]]. Its roots originate from more simplistic static checking techniques, such as static debugging<ref>{{cite journal | last1=Flanagan | first1=Cormac | last2=Flatt | first2=Matthew | last3=Krishnamurthi | first3=Shriram | last4=Weirich | first4=Stephanie | last5=Felleisen | first5=Matthias | title=Catching bugs in the web of program invariants |url=http://www.soe.ucsc.edu/~cormac/papers/pldi96.pdf |journal=[[ACM SIGPLAN Notices]] | publisher=Association for Computing Machinery (ACM) | volume=31 | issue=5 | year=1996 | issn=0362-1340 | doi=10.1145/249069.231387 | pages=23–32}}</ref> or [[Lint (software)|lint]] and [[FindBugs]]. A number of other languages have adopted ESC, including 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.
+== See also ==
+*[[Java Modeling Language]] (JML)
 == References ==
+{{reflist}}
-<references/>
 ==Further reading==
-*{{cite journal|last=Flanagan|first=Cormac|coauthors=K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, Raymie Stata|year=2002|title=Extended static checking for Java|journal=Proceedings of the [[Conference on Programming Language Design and Implementation]] (PLDI)|page=234|doi=10.1145/512529.512558|first1=Cormac |last1=Flanagan |first2=K. Rustan M. |last2=Leino |first3=Mark |last3=Lillibridge |first4=Greg |last4=Nelson |first5=James B. |last5=Saxe |first6=Raymie |last6=Stata}}
+*{{cite book |author1=Cormac Flanagan |author2=K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, Raymie Stata|title=Proceedings of the ACM SIGPLAN 2002 conference on Programming language design and implementation |chapter=Extended static checking for Java |year=2002|page=234|doi=10.1145/512529.512558|isbn=978-1581134636|s2cid=47141042 }}
-*{{cite journal|last1=Babic|first1=Domagoj|first2=Alan J. |last2=Hu|year=2008|title=Calysto: Scalable and Precise Extended Static Checking|journal=Proceedings of the International Conference on Software Engineering (ICSE)|page=211|doi=10.1145/1368088.1368118}}
+*{{cite book|last1=Babic|first1=Domagoj|first2=Alan J. |last2=Hu|title=Proceedings of the 13th international conference on Software engineering - ICSE '08 |chapter=Calysto |year=2008|page=211|doi=10.1145/1368088.1368118|isbn=9781605580791|s2cid=62868643 }}
-*{{cite journal|last=Chess|first=B.V.|year=2002|title=Improving computer security using extended static checking|journal=Proceedings of IEEE Symposium on Security and Privacy|pages=160–173|doi=10.1109/SECPRI.2002.1004369}}
+*{{cite book|last=Chess|first=B.V.|title=Proceedings 2002 IEEE Symposium on Security and Privacy |year=2002|chapter=Improving computer security using extended static checking|pages=160–173|doi=10.1109/SECPRI.2002.1004369|isbn=978-0-7695-1543-4|citeseerx=10.1.1.15.2090|s2cid=12067758 }}
-*{{cite journal|last1=Rioux|first1=Frédéric|first2=Patrice |last2=Chalin|year=2006|title=Improving the Quality of Web-based Enterprise Applications with Extended Static Checking: A Case Study|journal=Electronic Notes in Theoretical Computer Science|volume=157|issue=2|pages=119–132|issn=15710661|doi=10.1016/j.entcs.2005.12.050}}
+*{{cite journal|last1=Rioux|first1=Frédéric|first2=Patrice |last2=Chalin|year=2006|title=Improving the Quality of Web-based Enterprise Applications with Extended Static Checking: A Case Study|journal=Electronic Notes in Theoretical Computer Science|volume=157|issue=2|pages=119–132|issn=1571-0661|doi=10.1016/j.entcs.2005.12.050|doi-access=free}}
-*{{cite journal|last1=James|first1=Perry R.|first2=Patrice |last2=Chalin|year=2009|title=Faster and More Complete Extended Static Checking for the Java Modeling Language|journal=Journal of Automated Reasoning|volume=44|issue=1–2|pages=145–174|issn=0168-7433|doi=10.1007/s10817-009-9134-9}}
+*{{cite journal|last1=James|first1=Perry R.|first2=Patrice |last2=Chalin|year=2009|title=Faster and More Complete Extended Static Checking for the Java Modeling Language|journal=Journal of Automated Reasoning|volume=44|issue=1–2|pages=145–174|issn=0168-7433|doi=10.1007/s10817-009-9134-9|citeseerx=10.1.1.165.7920|s2cid=14996225 }}
-*{{cite journal|last=Xu|first=Dana N.|year=2006|title=Extended static checking for haskell|journal=Proceedings of the ACM workshop on Haskell|page=48|doi=10.1145/1159842.1159849}}
+*{{cite book|last=Xu|first=Dana N.|title=Proceedings of the 2006 ACM SIGPLAN workshop on Haskell |year=2006|chapter=Extended static checking for haskell|page=48|doi=10.1145/1159842.1159849|isbn=978-1595934895|citeseerx=10.1.1.377.3777|s2cid=1340468 }}
-*{{cite journal|last=Leino|first=K. Rustan M.|title=Extended Static Checking: A Ten-Year Perspective|journal=Informatics|volume=2000|pages=157–175|doi=10.1007/3-540-44577-3_11|year=2001}}
+*{{cite book|last=Leino|first=K. Rustan M.|title=Informatics |chapter=Extended Static Checking: A Ten-Year Perspective|volume=2000|pages=157–175|doi=10.1007/3-540-44577-3_11|year=2001|series=Lecture Notes in Computer Science|isbn=978-3-540-41635-7}}
 *{{cite journal|year=1998|title=Extended Static Checking|journal=Compaq SRC Research Report|issue=159|first1=David L. |last1=Detlefs |first2=K. Rustan M. |last2=Leino |first3=Greg |last3=Nelson |first4=James B. |last4=Saxe}}