This is an old revision of the document!

Correctness of A/G Reasoning

Correctness as Approximation of Relations

Specification $s$ provides a relation that is intended to approximate relation $r$ defining the meaning of procedure, that is, we would like to prove \[

  r \subseteq s

Following Relational Semantics of Procedures, consider one procedure and its associated function \[

  m : {\cal R} \to {\cal 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 \[

   m(s) \subseteq s

\] We claim that $r_* \subseteq s$ where $r_* = \bigcup_{k \ge 0} m^k(\emptyset)$ .

Proof:

Expressing Approximation Using Assume and Assert

Consider a program with only one state variable $x$ .

We express our approximation as \[

 \begin{array}{l}
   assert\, (P(x));\\
   havoc(x); \\
   assume(Q(x))
 \end{array}

So, we would like to show that \[

  r\qquad \subseteq\qquad
 \begin{array}{l}
   (assert\, (P(x));\\
   havoc(x); \\
   assume\, (Q(x)))
 \end{array}

\] is implied by the condition we are checking: \[

 \begin{array}{l}
   (assume\, (P(x));\\
   r; \\
   assert\, (Q(x)))
 \end{array}
 \qquad\subseteq \qquad
 havoc(x)

Shunting rules

For relations $r$ , $s$ that propagate errors (as in Assert and error conditions): \[

   (assume(P(x)); r \subseteq s)\ \ \leftrightarrow\ \ r \subseteq assert(P(x)); s

\] \[

   (r; assert(Q(x)) \subseteq s)\ \ \leftrightarrow\ \ r \subseteq s;assume(Q(x))