|
'''Extended Staticstatic Checkingchecking''' ('''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 system#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 completenesssoundness, in that it aims to dramatically reduce the number of ''false positives'' (reportedoverestimated errors that are not real errors, inthat factis, notESC errorsover strictness) at the cost of introducing some ''false negatives'' (real errorsESC whichunderestimation error, but that need no programmer's attention, or are not reportedtargeted 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, Domagoj| Babicpublisher=ACM andPress Alan J. Hu. In| conference=Proceedings of the International Conference on Software Engineering (ICSE),| year=2008. doi:| http://dx.doi.org/=10.1145/1368088.1368118 | page=}}</ref>. ESC can identify a range of errors whichthat are currently outside the scope of a type checker, including [[division by zero]], [[bounds checking|array out of bounds]], [[integer overflow]] and [[pointer (computing)#Null pointer|null dereferences]].
The techniques used in extended static checking come from various fields of [[Computercomputer Science]]science, including [[static program analysis]], [[symbolic simulation]], [[model checking]], [[abstract interpretation]], [[satisfiability modulo theories|SAT solving]] and [[automated theorem proving]]. and One[[type characteristicchecking]]. isExtended thatstatic ESCchecking 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,level in theorder formto ofscale [[precondition|pre-]]to andlarge [[postcondition|post-conditions]],programs.<ref [[loopname=GNESCUWCSC>{{Cite invariant|loop invariants]] and [[class invariant|class invariants]].web
| title = Extended Static Checking
| work = UWTV
| accessdate = 2012-02-01
| url = http://stage.uwtv.org/video/player.aspx?mediaid=1577083988
| archive-url = https://archive.today/20130416030925/http://stage.uwtv.org/video/player.aspx?mediaid=1577083988
| url-status = dead
| archive-date = April 16, 2013
}}</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.respectively [[predicate transformer semantics#Weakest preconditions|weakest preconditions]]) intraprocedurally through a method starting from the precondition (resp.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 Staticstatic Checkingchecking was pioneered in ESC/Modula-3<ref>An{{cite extendedbook Static| Checkerlast1=Rustan for Modula-3,| first1=K. Rustan| last2=Leino | first2=M. Leino| andlast3=Nelson | first3=Greg Nelson.| title=Lecture InNotes Proceedingsin ofComputer theScience - International Conference on Compiler Construction,| pageschapter=An 302-extended static checker for modula-305,3 | publisher=Springer| year=1998. doi:| isbn=978-3-540-64304-3 | issn=0302-9743 | http://dx.doi.org/=10.1007/BFb0026418bfb0026441|doi-access=free | pages=302–305}}</ref> and, later, [[ESC/Java]]. Its roots originate from more simplistic static checking techniques, such as usedstatic 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 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.
== See also ==
*[[Java Modeling Language]] (JML)
== References ==
{{reflist}}
<references/>
==Further reading==
*{{cite journalbook |last=Flanagan|firstauthor1=Cormac Flanagan |coauthorsauthor2=K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, Raymie Stata|year=2002|title=ExtendedProceedings staticof checkingthe forACM Java|journal=ProceedingsSIGPLAN of the2002 [[Conferenceconference on Programming Languagelanguage Designdesign and Implementation]]implementation (PLDI)|chapter=Extended static checking for Java |year=2002|page=234|doi=10.1145/512529.512558|first1isbn=Cormac 978-1581134636|last1s2cid=Flanagan47141042 |first2=K. Rustan M. |last2=Leino |first3=Mark |last3=Lillibridge |first4=Greg |last4=Nelson |first5=James B. |last5=Saxe |first6=Raymie |last6=Stata}}
*{{cite journalbook|last1=Babic|first1=Domagoj|first2=Alan J. |last2=Hu|year=2008|title=Calysto: Scalable and Precise Extended Static Checking|journal=Proceedings of the International13th Conferenceinternational conference on Software Engineeringengineering - (ICSE) '08 |chapter=Calysto |year=2008|page=211|doi=10.1145/1368088.1368118|isbn=9781605580791|s2cid=62868643 }}
*{{cite journalbook|last=Chess|first=B.V.|title=Proceedings 2002 IEEE Symposium on Security and Privacy |year=2002|titlechapter=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|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=157106611571-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-21–2|pages=145–174|issn=0168-7433|doi=10.1007/s10817-009-9134-9|citeseerx=10.1.1.165.7920|s2cid=14996225 }}
*{{cite journalbook|last=Xu|first=Dana N.|year=2006|title=Extended static checking for haskell|journal=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 journalbook|last=Leino|first=K. Rustan M.|title=Informatics |chapter=Extended Static Checking: A Ten-Year Perspective|journal=Informatics|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}}
{{DEFAULTSORT:Extended Static Checking}}
{{formalmethods-stub}}
[[Category:Static codeprogram analysis tools]] ▼
▲[[Category:Static code analysis]]
[[Category:Formal methods]]
| 