Lab for Automated Reasoning and Analysis 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') \} \\
 
sav08/assert_and_error_conditions.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice