Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | Next revision Both sides next revision | ||
sav07_homework_3 [2007/03/31 19:51] vkuncak |
sav07_homework_3 [2007/03/31 19:58] vkuncak |
||
---|---|---|---|
Line 18: | Line 18: | ||
\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 48: | Line 41: | ||
**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 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? | ||
- | |||
- | |||
- | ==== 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 ==== | ||