# 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

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:

Denoting the right-hand side by , we can write the above as

Thus, the meaning of the procedure is the fixpoint of function given by

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

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

## 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

where the function is given by:

We define lattice structure on by

Note that:

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

#### Remark

is the least fixpoint of , so by Tarski's Fixpoint Theorem, it is also the least such that . Thus, implies .