This is an old revision of the document!
Relational Semantics of Procedures
Let be the set of states and
denote
, the set of all relations on
.
In Relational Semantics for a language without procedures we had semantic function that maps programs to relations \[
r_c : C \to {\cal R}
\]
so was the relation corresponding to the command
, and we denote it by
.
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 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 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:
\[
r_{move} = ([\![assume(x>0)]\!]\ \circ\ [\![x=x-1]\!]\ \circ\ r_{move}\ \circ\ [\![y=y+1]\!])\ \bigcup\ [\![assume(!(x>0))]\!]
\]
Denoting the right-hand side by , we can write the above as
\[
r_{move} = F(r_{move})
\]
Thus, the meaning of the procedure is the fixpoint of function given by
\[
F(t) = ([\![assume(x>0)]\!]\ \circ\ [\![x=x-1]\!]\ \circ\ t\ \circ\ [\![y=y+1]\!])\ \bigcup\ [\![assume(!(x>0))]\!]
\]
Note that is monotonic in its argument, because the operators
,
are monotonic:
Similarly, the function is -continuous (see Tarski's Fixpoint Theorem). Thus, it has the least fixpoint, and this fixpoint is given by
\[
r_{move} = \bigcup_{n \ge 0} F^n(\emptyset)
\]
In fact, represents the result of inlining the recursive procedure
times. Therefore, if
is the initial state such
that the computation in the procedure terminates within
steps, then
iff
.
In this example, we have \[
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) \}
\]
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 ,
such that
\[
(r_{even},r_{odd}) = G(r_{even},r_{odd})
\]
where the function is given by:
\[
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} \]
We define lattice structure on by
\[
(r_1,r_2) \sqsubseteq (r'_1,r'_2) \ \mbox{ iff } \ (r_1 \subseteq r'_1) \land (r_2 \subseteq r'_2)
\] \[
(r_1,r_2) \sqcup (r'_1,r'_2) = (r_1 \cup r'_1, r_2 \cup r'_2)
\] Note that: \[
G(\emptyset,\emptyset) = ([\![assume(x==0)]\!] \circ [\![wasEven=true]\!], [\![assume(x==0)]\!] \circ [\![wasEven=false]\!])
\] \[
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}
\]
where and
denote first, respectively, second, element of the pair
.
The results extend to any number of call sites and any number of mutually recursive procedures, we just consider a function where
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 and
analogous to
and
(indeed, the domain
, that is
, is isomorphic to
).
The meaning of all procedures is then the tuple given by
.
Example
In the example above, we can prove that \[
r_{even} = \{((x,wasEven),(x',wasEven').\ x \ge 0 \land x' = 0 \land (wasEven' \leftrightarrow (x \mod 2 = 0))
\] \[
r_{odd} = \{((x,wasEven),(x',wasEven').\ x \ge 0 \land x' = 0 \land (wasEven' \leftrightarrow (x \mod 2 \ne 0))
\]
Remark
is the least fixpoint of
, so by Tarski's Fixpoint Theorem, it is also the least
such that
. Thus,
implies
.