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:correctness_of_a_g_reasoning [2008/04/10 13:54]
vkuncak
sav08:correctness_of_a_g_reasoning [2015/04/21 17:30] (current)
Line 4: Line 4:
  
 Specification $s$ provides a relation that is intended to approximate relation $r$ defining the meaning of procedure, that is, we would like to prove Specification $s$ provides a relation that is intended to approximate relation $r$ defining the meaning of procedure, that is, we would like to prove
-\[+\begin{equation*}
     r \subseteq s     r \subseteq s
-\]+\end{equation*}
  
 Following [[Relational Semantics of Procedures]],​ consider one procedure and its associated function Following [[Relational Semantics of Procedures]],​ consider one procedure and its associated function
-\[+\begin{equation*}
     m : {\cal R} \to {\cal R}     m : {\cal R} \to {\cal R}
-\]+\end{equation*}
 and its fixed point $r_*$. and its fixed point $r_*$.
  
 The idea of approach based on specifications is to prove that, if we assume that procedure calls satisfy the specification,​ then we can prove the specification for the procedure we are verifying. ​ In other words, specifications provide a relation $s$ such that The idea of approach based on specifications is to prove that, if we assume that procedure calls satisfy the specification,​ then we can prove the specification for the procedure we are verifying. ​ In other words, specifications provide a relation $s$ such that
-\[+\begin{equation*}
      m(s) \subseteq s      m(s) \subseteq s
-\]+\end{equation*}
 We claim that $r_* \subseteq s$ where $r_* = \bigcup_{k \ge 0} m^k(\emptyset)$. We claim that $r_* \subseteq s$ where $r_* = \bigcup_{k \ge 0} m^k(\emptyset)$.
  
Line 33: Line 33:
  
 We express our approximation as  We express our approximation as 
-\[+\begin{equation*}
    ​\begin{array}{l}    ​\begin{array}{l}
      ​assert\,​ (P(x));\\      ​assert\,​ (P(x));\\
Line 39: Line 39:
      ​assume(Q(x))      ​assume(Q(x))
    ​\end{array}  ​    ​\end{array}  ​
-\]+\end{equation*}
  
 So, we would like to show that So, we would like to show that
-\[+\begin{equation*}
     r\qquad \subseteq\qquad     r\qquad \subseteq\qquad
    ​\begin{array}{l}    ​\begin{array}{l}
Line 49: Line 49:
      ​assume\,​ (Q(x)))      ​assume\,​ (Q(x)))
    ​\end{array}  ​    ​\end{array}  ​
-\]+\end{equation*}
 is implied by the condition we are checking: is implied by the condition we are checking:
-\[+\begin{equation*}
    ​\begin{array}{l}    ​\begin{array}{l}
      ​(assume\,​ (P(x));\\      ​(assume\,​ (P(x));\\
Line 59: Line 59:
    ​\qquad\subseteq \qquad    ​\qquad\subseteq \qquad
    ​havoc(x)    ​havoc(x)
-\]+\end{equation*}
  
 ===== Shunting rules ===== ===== Shunting rules =====
Line 66: Line 66:
  
 For relations $r$, $s$ that respect errors, we have For relations $r$, $s$ that respect errors, we have
-\[+\begin{equation*}
      ​assume(P) \mathop{;} r \subseteq s\ \ \leftrightarrow\ \ r \subseteq assert(P) \mathop{;} s      ​assume(P) \mathop{;} r \subseteq s\ \ \leftrightarrow\ \ r \subseteq assert(P) \mathop{;} s
-\] +\end{equation*} 
-\[+\begin{equation*}
      r \mathop{;} assert(Q) \subseteq s\ \ \leftrightarrow\ \ r \subseteq s \mathop{;} assume(Q)      r \mathop{;} assert(Q) \subseteq s\ \ \leftrightarrow\ \ r \subseteq s \mathop{;} assume(Q)
-\]+\end{equation*}
  
 Proofs: Proofs:
   * using relations   * using relations
-  * using weakest preconditions (see [[sav07_homework_4#​rules_for_guarded_commands|homework in SAV'​07]])+  * using weakest preconditions (see [[:sav07_homework_4#​rules_for_guarded_commands|homework in SAV'​07]])