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
Next revision Both sides next revision
sav07_homework_3 [2007/03/31 19:51]
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 48: Line 39:
  
 **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 ====