Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Last revision Both sides next revision | ||
sav07_homework_3 [2007/03/31 19:58] vkuncak |
sav07_homework_3 [2007/04/02 09:37] vkuncak |
||
---|---|---|---|
Line 1: | Line 1: | ||
- | (Draft only!) | ||
- | |||
==== Forward and backward propagation ==== | ==== Forward and backward propagation ==== | ||
Line 18: | Line 16: | ||
\end{equation*} | \end{equation*} | ||
where $r^{-1}$ denotes the inverse of relation $r$. In other words, computing weakest preconditions corresponds to propagating possible errors backwards. | where $r^{-1}$ denotes the inverse of relation $r$. In other words, computing weakest preconditions corresponds to propagating possible errors backwards. | ||
+ | |||
==== Galois Connection ==== | ==== Galois Connection ==== | ||
Line 40: | Line 39: | ||
* $\gamma$ is an [[wk>injective function]] | * $\gamma$ is an [[wk>injective function]] | ||
- | **4.** State the condition for $c=\gamma(\alpha(c))$ to hold for all $c$. When $C$ is the set of concrete states and $A$ is a domain of static analysis, is it more reasonable to expect that $c=\gamma(\alpha(c))$ or $\alpha(\gamma(a)) = a$ to be satisfied, and why? | + | **4.** State the condition for $c=\gamma(\alpha(c))$ to hold for all $c$. When $C$ is the set of sets of concrete states and $A$ is a domain of static analysis, is it more reasonable to expect that $c=\gamma(\alpha(c))$ or $\alpha(\gamma(a)) = a$ to be satisfied, and why? |