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
sav08:assert_and_error_conditions [2009/03/12 16:17]
vkuncak
sav08:assert_and_error_conditions [2015/04/21 17:30] (current)
Line 28: Line 28:
  
 We assume that the desired properties $P$ satisfy We assume that the desired properties $P$ satisfy
-\[+\begin{equation*}
 \models P \rightarrow OK \models P \rightarrow OK
-\]+\end{equation*}
  
 ===== Desired Rules for Weakest Preconditions ===== ===== Desired Rules for Weakest Preconditions =====
  
 For all $Q$ such that $\models Q \rightarrow OK$, we would like the following to hold: For all $Q$ such that $\models Q \rightarrow OK$, we would like the following to hold:
-\[\begin{array}{l}+\begin{equation*}\begin{array}{l}
   \models wp(c,Q) \rightarrow OK \\   \models wp(c,Q) \rightarrow OK \\
   wp(c1 [] c2,Q) = wp(c1,Q) \land wp(c2,Q) \\   wp(c1 [] c2,Q) = wp(c1,Q) \land wp(c2,Q) \\
Line 43: Line 43:
   wp(assume(F),​Q) = (OK \land (F \rightarrow Q)) \\   wp(assume(F),​Q) = (OK \land (F \rightarrow Q)) \\
   wp(assert(F),​Q) = (F \land Q)   wp(assert(F),​Q) = (F \land Q)
-\end{array}\]+\end{array}\end{equation*}
  
 We assume above that $x$ is not the //error// variable. We assume above that $x$ is not the //error// variable.
  
 Note: we wrote $OK \land ...$ in the weakest precondition of assume, but usually $OK$ is implicit and we do not write it.  We do not need it in other cases because it follows that right hand side implies $OK$. Note: we wrote $OK \land ...$ in the weakest precondition of assume, but usually $OK$ is implicit and we do not write it.  We do not need it in other cases because it follows that right hand side implies $OK$.
 +
  
  
Line 54: Line 55:
 Let OK denote s(error)=0 and OK' denote s'​(error)=0. ​ We define: Let OK denote s(error)=0 and OK' denote s'​(error)=0. ​ We define:
 \begin{eqnarray*} \begin{eqnarray*}
-  R_c(\mbox{havoc(x)}) &=& \{(s,​s'​) \mid OK \rightarrow (OK' \land s'​(y)=s(y)) \} \\+  R_c(\mbox{havoc(x)}) &=& \{(s,​s'​) \mid OK \rightarrow (OK' \land \bigwedge_{y \not\equiv x}\ s'​(y)=s(y)) \} \\
   R_c(\mbox{assert}\ F}) &=& \{(s,​s'​) \mid (OK \land F(s)) \rightarrow s=s' \} \\   R_c(\mbox{assert}\ F}) &=& \{(s,​s'​) \mid (OK \land F(s)) \rightarrow s=s' \} \\
   R_c(\mbox{assume}\ F}) &=& \{(s,​s'​) \mid OK\ \rightarrow\ (F(s) \land s=s') \} \\   R_c(\mbox{assume}\ F}) &=& \{(s,​s'​) \mid OK\ \rightarrow\ (F(s) \land s=s') \} \\