Relational Semantics of Procedures

Let $S$ be the set of states and ${\cal R}$ denote $2^{S\times S}$ , the set of all relations on $S$ .

In Relational Semantics for a language without procedures we had semantic function that maps programs to relations

$\begin{equation*} r_c : C \to {\cal R} \end{equation*}$

so $r_c(c_1)$ was the relation corresponding to the command $c_1$ , and we denote it by $[\![c_1]\!]$ .

How can we define semantics for program with recursive procedures?

We consider first the case of procedures without parameters; adding parameters is straightforward.

One Recursive Procedure

We first illustrate the semantics for one recursive procedure. The definition only relies on the Lattices structure, so it generalizes to recursive definitions with multiple procedures, and recursive definitions in general.

Example: Consider the following procedure that, if $x,y$ are positive, moves the content of x into y.

  var x,y;
  proc move() {
     if (x > 0) {
       x = x - 1;
       move();
       y = y + 1;
     }
  }

or, expressed using non-deterministic choice and assume:

  var x,y;
  proc move() {
     ( assume(x>0);
       x = x - 1;
       move();
       y = y + 1;
     ) 
     [] (assume (!(x>0))
  }

Suppose we have relation $r_{move}$ describing the meaning of the procedure. By Relational Semantics, this procedure should behave similarly as the meanings of commands, so we should have the following equation:

$\begin{equation*} r_{move} = ([\![assume(x>0)]\!]\ \circ\ [\![x=x-1]\!]\ \circ\ r_{move}\ \circ\ [\![y=y+1]\!])\ \bigcup\ [\![assume(!(x>0))]\!] \end{equation*}$

Denoting the right-hand side by $F(r_{move})$ , we can write the above as

$\begin{equation*} r_{move} = F(r_{move}) \end{equation*}$

Thus, the meaning of the procedure is the fixpoint of function $F : {\cal R} \to {\cal R}$ given by

$\begin{equation*} F(t) = ([\![assume(x>0)]\!]\ \circ\ [\![x=x-1]\!]\ \circ\ t\ \circ\ [\![y=y+1]\!])\ \bigcup\ [\![assume(!(x>0))]\!] \end{equation*}$

Note that $F$ is monotonic in its argument, because the operators $\circ$ , $\cup$ are monotonic:

$r_1 \subseteq r_2\ \rightarrow\ (r_1 \circ s) \subseteq (r_2 \circ s)$
$r_1 \subseteq r_2\ \rightarrow\ (s \circ r_1) \subseteq (s \circ r_2)$
$r_1 \subseteq r_2\ \rightarrow\ r_1 \cup s \subseteq r_2 \cup s$

Similarly, the function is $\omega$ -continuous (see Tarski's Fixpoint Theorem). Thus, it has the least fixpoint, and this fixpoint is given by

$\begin{equation*} r_{move} = \bigcup_{n \ge 0} F^n(\emptyset) \end{equation*}$

In fact, $F^n(\emptyset)$ represents the result of inlining the recursive procedure $n$ times. Therefore, if $s_0$ is the initial state such that the computation in the procedure terminates within $n$ steps, then $(s_0,s) \in F^n(\emptyset)$ iff $(s_0,s) \in r_{move}$ .

In this example, we have

$\begin{equation*} r_{move} = \{((x,y),(x',y').\ (x > 0 \land x'=0 \land y'=x+y) \lor (x \le 0 \land x'=x \land y'=y) \} \end{equation*}$

Multiple Mutually Recursive Procedures

Example: Consider the following example. The idea is that after execution of the procedure even(), the boolean variable wasEven shows whether the initial value of x was even.

var x : int
var wasEven : bool

proc even() {
  if (x==0) {
    wasEven = true;
  } else {
    x = x - 1;
    odd();
  }
}
proc odd() {
  if (x==0) {
    wasEven = false;
  } else {
    x = x - 1;
    even();
  }
}

We can write the bodies as follows:

even() =
   (assume(x==0); wasEven = true)
   []
   (assume(x!=0); x = x - 1; odd())

odd() = 
   (assume(x==0); wasEven = false)
   []
   (assume(x!=0); x = x - 1; even())

Now, we turn mutually recursive definition into a simple recursive definition by taking the pair of the meaning of odd and even. We need to find relations $r_{even}$ , $r_{odd}$ such that

$\begin{equation*} (r_{even},r_{odd}) = G(r_{even},r_{odd}) \end{equation*}$

where the function $G : {\cal R}^2 \to {\cal R}^2$ is given by:

$\begin{equation*} G(E,O) = \begin{array}[t]{@{}l@{}} \bigg( ([\![assume(x==0)]\!] \circ [\![wasEven=true]\!]) \cup ([\![assume(x!=0)]\!] \circ [\![x=x-1]\!] \circ O)\ , \\ ([\![assume(x==0)]\!] \circ [\![wasEven=false]\!]) \cup ([\![assume(x!=0)]\!] \circ [\![x=x-1]\!] \circ E) \bigg) \end{array} \end{equation*}$

We define lattice structure on ${\cal R}^2$ by

$\begin{equation*} (r_1,r_2) \sqsubseteq (r'_1,r'_2) \ \mbox{ iff } \ (r_1 \subseteq r'_1) \land (r_2 \subseteq r'_2) \end{equation*}$

$\begin{equation*} (r_1,r_2) \sqcup (r'_1,r'_2) = (r_1 \cup r'_1, r_2 \cup r'_2) \end{equation*}$

Note that:

$\begin{equation*} G(\emptyset,\emptyset) = ([\![assume(x==0)]\!] \circ [\![wasEven=true]\!], [\![assume(x==0)]\!] \circ [\![wasEven=false]\!]) \end{equation*}$

$\begin{equation*} G(G(\emptyset,\emptyset)) = \begin{array}[t]{@{}l@{}} \bigg( ([\![assume(x==0)]\!] \circ [\![wasEven=true]\!]) \cup ([\![assume(x!=0)]\!] \circ [\![x=x-1]\!] \circ G(\emptyset,\emptyset).\_2)\ , \\ ([\![assume(x==0)]\!] \circ [\![wasEven=false]\!]) \cup ([\![assume(x!=0)]\!] \circ [\![x=x-1]\!] \circ G(\emptyset,\emptyset).\_1) \bigg) \end{array} \end{equation*}$

where $p.\_1$ and $p.\_2$ denote first, respectively, second, element of the pair $p$ .

The results extend to any number of call sites and any number of mutually recursive procedures, we just consider a function $G : {\cal R}^d \to {\cal R}^d$ where $d$ is the number of procedures; this mapping describes how, given one approximation of procedure semantics, compute a better approximation that is correct for longer executions.

We define $\sqsubseteq$ and $\sqcup$ analogous to $\subseteq$ and $\cup$ (indeed, the domain ${\cal R}^d$ , that is $(2^{S\times S})^d$ , is isomorphic to $2^{S\times S \times \{1,2,\ldots,d\}}$ ).

The meaning of all procedures is then the tuple $p_* \in {\cal R}^n$ given by $\bigsqcup\limits_{n \ge 0} G^n(\emptyset,\ldots,\emptyset)$ .

Example

In the example above, we can prove that

$\begin{equation*} r_{even} = \{((x,wasEven),(x',wasEven').\ x \ge 0 \land x' = 0 \land (wasEven' \leftrightarrow ((x \mod 2) = 0)) \end{equation*}$

$\begin{equation*} r_{odd} = \{((x,wasEven),(x',wasEven').\ x \ge 0 \land x' = 0 \land (wasEven' \leftrightarrow ((x \mod 2) \ne 0)) \end{equation*}$

Remark

$p_*$ is the least fixpoint of $G$ , so by Tarski's Fixpoint Theorem, it is also the least $p$ such that $G(p) \sqsubseteq p$ . Thus, $G(p) \sqsubseteq p$ implies $p_* \sqsubseteq p$ .