• English only

# Differences

This shows you the differences between two versions of the page.

correctness_of_formula_propagation [2007/04/14 17:19]
vkuncak
correctness_of_formula_propagation [2007/04/15 18:40] (current)
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.
+