Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
sav07_homework_3 [2007/03/31 19:45] vkuncak |
sav07_homework_3 [2007/03/31 20:00] 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 41: | Line 34: | ||
**3.** Let $\alpha$ and $\gamma$ satisfy the condition of Galois connection. Show that the following three conditions are equivalent: | **3.** Let $\alpha$ and $\gamma$ satisfy the condition of Galois connection. Show that the following three conditions are equivalent: | ||
- | * $c = \gamma(\alpha(c))$ for all $c$ | + | * $\alpha(\gamma(a)) = a$ for all $a$ |
- | * $\gamma$ is a [[wk>surjective function]] | + | * $\alpha$ is a [[wk>surjective function]] |
- | * $\alpha$ is an [[wk>injective function]] | + | * $\gamma$ is an [[wk>injective function]] |
- | + | ||
- | ==== Weakest preconditions and relations ==== | + | |
- | + | ||
- | Consider a guarded command language with one variable, denoted x, and constructs | + | |
- | + | ||
- | assume F | + | |
- | assert F | + | |
- | havoc(x) | + | |
- | c1 [] c2 | + | |
- | c1 ; c2 | + | |
- | + | ||
- | Assume that F can only mention x as the only variable, which takes values from some set $S$. Program states in our language will be pairs $(x,ok)$ where $x \in S$ and $ok$ is a boolean value that indicates whether an error has occurred. Therefore, a state is an element of $\mbox{PS} = S \times \{\mbox{true},\mbox{false}\}$. | + | |
- | + | ||
- | Your task is to define, for each command $c$, the meaning $R(c) \subseteq \mbox{PS}^2$. | + | |
- | + | ||
- | Using the standard definition of $wp$, | + | |
- | \begin{equation*} | + | |
- | wp(c,Q) = \{ s_1 \mid \forall s_2. (s_1,s_2) \in R(c) \rightarrow s_2 \in Q \} | + | |
- | \end{equation*} | + | |
- | + | ||
- | Your goal is to come up with the definition of $R(c)$ such that wp satisfies the following **expected conditions:** | + | |
- | + | ||
- | wp(Q, assume F) = {(x,ok)|F(x) -> (x,ok)∈Q} | + | |
- | wp(Q, assert F) = {(x,ok)|F(x) & (x,ok)∈Q} | + | |
- | wp(Q, havoc(x)) = {(x,ok)|∀x'.(x',ok) ∈ Q} | + | |
- | wp(Q, c1 [] c2) = wp(Q,c1) ∩ wp(Q,c2) | + | |
- | wp(Q, c1 ; c2) = wp(wp(Q,c2),c1) | + | |
- | + | ||
- | These conditions correspond to our rules for propagating formulas using wp. | + | |
- | + | ||
- | As a hint, you should be able to define | + | |
- | + | ||
- | R(c1 [] c2) = R(c1) ∪ R(c2) | + | |
- | R(c1 ; c2) = R(c1) o R(c2) | + | |
- | + | ||
- | Your remaining task is to define the meaning of assert, assume, and havoc such that all the **expected conditions** above hold. | + | |
- | + | ||
- | Verify your solution by computing | + | |
- | + | ||
- | R(assert(false); assume(false)) | + | |
- | + | ||
- | and | + | |
- | + | ||
- | wp(PS, assert(false);assume(false)). | + | |
- | + | ||
- | where PS is the set of all program states. | + | |
- | + | ||
- | + | ||
- | ==== Resolution Example ==== | + | **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? |