# 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 Both sides previous revision Previous revision 2007/04/15 18:40 vkuncak 2007/04/14 17:19 vkuncak 2007/04/14 17:17 vkuncak 2007/04/14 17:09 vkuncak 2007/04/14 17:08 vkuncak 2007/04/14 17:08 vkuncak 2007/04/14 17:06 vkuncak 2007/04/14 17:05 vkuncak 2007/04/14 17:00 vkuncak 2007/04/14 16:59 vkuncak 2007/04/14 16:55 vkuncak 2007/04/14 16:54 vkuncak 2007/04/14 16:53 vkuncak 2007/04/14 16:33 vkuncak 2007/04/14 15:59 vkuncak created 2007/04/15 18:40 vkuncak 2007/04/14 17:19 vkuncak 2007/04/14 17:17 vkuncak 2007/04/14 17:09 vkuncak 2007/04/14 17:08 vkuncak 2007/04/14 17:08 vkuncak 2007/04/14 17:06 vkuncak 2007/04/14 17:05 vkuncak 2007/04/14 17:00 vkuncak 2007/04/14 16:59 vkuncak 2007/04/14 16:55 vkuncak 2007/04/14 16:54 vkuncak 2007/04/14 16:53 vkuncak 2007/04/14 16:33 vkuncak 2007/04/14 15:59 vkuncak created 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. +