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 [2010/03/08 13:48]
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.
Line 55: 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 \bigwedge_{{y \not\equiv x} 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') \} \\