# Differences

This shows you the differences between two versions of the page.

 sav08:correctness_of_a_g_reasoning [2008/04/10 13:54]vkuncak sav08:correctness_of_a_g_reasoning [2015/04/21 17:30] (current) Both sides previous revision Previous revision 2008/04/10 13:54 vkuncak 2008/04/10 13:54 vkuncak 2008/04/10 13:51 vkuncak 2008/04/10 13:47 vkuncak 2008/04/10 12:46 vkuncak 2008/04/10 12:44 vkuncak 2008/04/10 12:44 vkuncak 2008/04/10 12:38 vkuncak 2008/04/10 12:35 vkuncak 2008/04/10 12:35 vkuncak 2008/04/10 12:22 vkuncak 2008/04/10 12:21 vkuncak 2008/04/10 12:19 vkuncak 2008/04/10 00:55 vkuncak 2008/04/09 10:36 vkuncak 2008/04/09 00:37 vkuncak created Next revision Previous revision 2008/04/10 13:54 vkuncak 2008/04/10 13:54 vkuncak 2008/04/10 13:51 vkuncak 2008/04/10 13:47 vkuncak 2008/04/10 12:46 vkuncak 2008/04/10 12:44 vkuncak 2008/04/10 12:44 vkuncak 2008/04/10 12:38 vkuncak 2008/04/10 12:35 vkuncak 2008/04/10 12:35 vkuncak 2008/04/10 12:22 vkuncak 2008/04/10 12:21 vkuncak 2008/04/10 12:19 vkuncak 2008/04/10 00:55 vkuncak 2008/04/09 10:36 vkuncak 2008/04/09 00:37 vkuncak created 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]])