Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
correctness_of_formula_propagation [2007/04/14 17:17] vkuncak |
correctness_of_formula_propagation [2007/04/15 18:40] vkuncak |
||
---|---|---|---|
Line 23: | Line 23: | ||
\mbox{fact}_i(w) | \mbox{fact}_i(w) | ||
\end{eqnarray*} | \end{eqnarray*} | ||
- | Let $I$ denote $\mbox{fact}_i(w)$. We have shown that $I$ is preserved across every loop iteration. Note that $sp(I,\mbox{assume}(F);c)) \rightarrow I$ corresponds to | + | Let $I$ denote $\mbox{fact}_i(w)$. We have shown |
+ | \begin{equation*} | ||
+ | sp(I, \mbox{assume}(F);c)) \rightarrow I | ||
+ | \end{equation*} | ||
+ | That is, $I$ is preserved across every loop iteration. Note that $sp(I,\mbox{assume}(F);c)) \rightarrow I$ corresponds to | ||
\begin{equation*} | \begin{equation*} | ||
I \rightarrow wp(I, \mbox{assume}(F);c) | I \rightarrow wp(I, \mbox{assume}(F);c) | ||
Line 57: | 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. | ||
+ |