Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
sav07_homework_3 [2007/03/31 20:00] vkuncak |
sav07_homework_3 [2007/04/15 17:07] vkuncak |
||
|---|---|---|---|
| Line 16: | 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 23: | Line 24: | ||
| \alpha(c) \sqsubseteq a\ \iff\ c \leq \gamma(a) \qquad (*) | \alpha(c) \sqsubseteq a\ \iff\ c \leq \gamma(a) \qquad (*) | ||
| \end{equation*} | \end{equation*} | ||
| - | for all $c$ and $a$. | + | for all $c$ and $a$ (intuitively, the condition means that $c$ is approximated by $a$). |
| **2.** Show that the condition $(*)$ is equivalent to the conjunction of these two conditions: | **2.** Show that the condition $(*)$ is equivalent to the conjunction of these two conditions: | ||
| Line 38: | 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? |