• English only

# Differences

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

Link to this comparison view

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