Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Last revision Both sides next revision | ||
|
sav07_lecture_7 [2007/04/18 03:01] philippe.suter |
sav07_lecture_7 [2009/03/24 23:18] vkuncak |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| ====== Lecture 7: Formulas as a unifying domain for static analysis ====== | ====== Lecture 7: Formulas as a unifying domain for static analysis ====== | ||
| + | |||
| Line 54: | Line 55: | ||
| Analysis stops when $\forall v. \mbox{fact}_{i+1}(v) \rightarrow \mbox{fact}_i(v)$. That is, no new states are generated by strongest postcondition (we have reached a fix point - formula not trivial). | Analysis stops when $\forall v. \mbox{fact}_{i+1}(v) \rightarrow \mbox{fact}_i(v)$. That is, no new states are generated by strongest postcondition (we have reached a fix point - formula not trivial). | ||
| - | __Note__: If you end up with a situation where $\exists$ a state $v$ for which $\mbox{fact}(v) = true$, then the analysis is useless. In this case, you may want to refine $A$ (and hence also change the function $N$). Sometimes, this can be done automatically. | + | __Note__: If you end up with a situation where $\exists$ a state $v$ for which $\mbox{fact}(v) = true$, then the analysis gives no useful information about state $v$. In this case, you may want to refine $A$ (and hence also change the function $N$). Sometimes, this can be done automatically. |
| ===== Examples ===== | ===== Examples ===== | ||