Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | |||
|
correctness_of_formula_propagation [2007/04/14 17:19] vkuncak |
correctness_of_formula_propagation [2007/04/15 18:40] vkuncak |
||
|---|---|---|---|
| Line 61: | Line 61: | ||
| With this transformation we can represent arbitrary control-flow graphs, and then we need to worry only about one loop. Moreover, we can support control-flow constructs such as goto and break. | With this transformation we can represent arbitrary control-flow graphs, and then we need to worry only about one loop. Moreover, we can support control-flow constructs such as goto and break. | ||
| + | |||
| + | **Note:** It does not matter how we obtained $\mbox{fact}_i(v)$ as long as, for the control flow graph $(V,E)$, we can find some values $\mbox{fact}(v)$ for each node $v \in V$, such that for each $(v,c,u) \in E$ we have | ||
| + | \begin{equation*} | ||
| + | sp(\mbox{fact}(u),c) \rightarrow \mbox{fact}(v) | ||
| + | \end{equation*} | ||
| + | |||
| + | In particular, we could have guessed a loop invariant using some heuristics, or postupated invariant as a formula with some unknowns and then tried to solve for these unknowns. | ||
| + | |||