Content deleted Content added
Timtempleton (talk | contribs) added important context |
Rescuing 0 sources and tagging 1 as dead. #IABot (v2.0beta15) |
||
Line 6:
| accessdate = 2012-02-01
| url = http://stage.uwtv.org/video/player.aspx?mediaid=1577083988
}}{{Dead link|date=August 2019 |bot=InternetArchiveBot |fix-attempted=yes }}</ref> Furthermore, extended static checking 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.
| |||