Reasoning about Procedures by Inlining Contracts

Suppose we have a program where each procedure has a contract. We prove program correctness in two steps:

replace each procedure call with procedure contract (if there are parameters, instantiate them)
for each procedure, show that the resulting body satisfies the contract

It is clear that this reasoning is correct for non-recursive procedures.

We will show that it is also correct for mutually recursive procedures.

Example of Inlining Contracts

In this code,

proc even() 
requires x >= 0
ensures (wasEven == (old(x) % 2 == 0))
{
  if (x==0) {
    wasEven = true;
  } else {
    x = x - 1;
    odd();
  }
}
proc odd()
requires x >= 0
ensures (wasEven == (old(x) % 2 != 0))
{
  if (x==0) {
    wasEven = false;
  } else {
    x = x - 1;
    even();
  }
}

After inlining contracts we obtain:

proc even() 
requires x >= 0
ensures (wasEven == (old(x) % 2 == 0))
{
  if (x==0) {
    wasEven = true;
  } else {
    x = x - 1;
    x0 = x;
    assert(x >= 0);
    havoc x, wasEven;
    assume(wasEven == (x0 % 2 != 0));
  }
}
proc odd()
requires x >= 0
ensures (wasEven == (old(x) % 2 != 0))
{
  if (x==0) {
    wasEven = false;
  } else {
    x = x - 1;
    x0 = x;
    assert(x >= 0);
    havoc x, wasEven;
    assume(wasEven == (x0 % 2 == 0));
  }
}

In the resulting code there are no more procedure calls. We verify for each procedure that it conforms to the pre/post condition. We do so by assuming 'requires' and asserting 'ensures'. We also need to save the initial state to be able to refer to it in the postcondition. For 'even' procedure, we need to show that the following code does not lead to errors:

oldx = x;
assume(x >= 0);
if (x==0) {
  wasEven = true;
} else {
  x = x - 1;
  x0 = x;
  assert(x >= 0);
  havoc x, wasEven;
  assume(wasEven == (x0 % 2 != 0));
}
assert((wasEven == (oldx % 2 == 0));

Correctness of Inlining Contracts

Suppose we have two mutually recursive procedures, as in the previous example. We can give their semantics as the least solution $(r'_1,r'_2)$ of the system of equations on relations:

$\begin{equation*} r_1 = body_1(r_1,r_2) \end{equation*}$

$\begin{equation*} r_2 = body_2(r_1,r_2) \end{equation*}$

That is, it is the least fixpoint of function

$\begin{equation*} G(r_1,r_2) = (body_1(r_1,r_2), body_2(r_1,r_2)) \end{equation*}$

Suppose $r_1$ has the contract (specification) $s_1$ and $r_2$ has contract $s_2$ . Inlining contract into first procedure we obtain $body_1(s_1,s_2)$ . The technique that we propose therefore corresponds to proving:

$\begin{equation*} body_1(s_1,s_2) \subseteq s_1 \end{equation*}$

$\begin{equation*} body_2(s_1,s_2) \subseteq s_2 \end{equation*}$

In other words, it shows $G(s_1,s_2) \sqsubseteq (s_1,s_2)$ . This means that the specification $(s_1,s_2)$ is a postfix point of $G$ . By Tarski's Fixpoint Theorem, the least fixpoint is the least postfix point as well, so

$\begin{equation*} (r'_1, r'_2) \sqsubseteq (s_1,s_2) \end{equation*}$

that is $r'_1 \subseteq s_1$ and $r'_2 \subseteq s_2$ . Therefore, the meaning of each procedure satisfies its specification, which shows that this approach is correct.

Shunting rules

We say that relation $r$ respects errors if for an error state $e$ we have $(e,x) \in r$ for all states $x$ .

For relations $r$ , $s$ that respect errors, we have

$\begin{equation*} 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) \end{equation*}$

For more, see the semantics of Assert and error conditions.

Proofs:

using relations
using weakest preconditions (see homework in SAV'07)

Verifying that Body Conforms to Contract

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

We express our approximation as

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

We show that

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

is implied by

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

To check the final condition, because $x$ describes the entire state, all we need to check is that the transformed program

$\begin{equation*} (assume\, (P(x));\\ r; \\ assert\, (Q(x))) \end{equation*}$

cannot result in assertion violations.

Note: we can also directly check the relation subset condition, by computing formula for relation body and showing that it implies the formula for the contract.