LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision 		Previous revision
sav07_homework_3 [2007/03/31 19:51]
vkuncak 		sav07_homework_3 [2007/04/15 17:07]
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.
- 
- 
- 
- 
- 
- 
  
  
Line 32: 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 47: 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?
- +
- +
-==== 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 ====+