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: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]])
  
 
sav08/correctness_of_a_g_reasoning.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice