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 Both sides next revision
sav07_homework_3 [2007/03/31 19:48]
vkuncak
sav07_homework_3 [2007/03/31 19:51]
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.
 +
  
  
Line 46: Line 47:
   * $\gamma$ is an [[wk>​injective function]]   * $\gamma$ is an [[wk>​injective function]]
  
-**4.** State the condition for $c=\gamma(\alpha(c))$ to hold.+**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 ==== ==== Weakest preconditions and relations ====