Review of Fixpoints in Semantics

Transitive Closure as Least Fixedpoint

Recall the definition of transitive closure for $r \subseteq D \times D$ a binary relation

$\begin{equation*} r^* = \bigcup_{n \ge 0} r^n \end{equation*}$

where $r^0 = \Delta_D$ .

Lemma: Reflexive transitive closure is the least fixpoint of function $f(r) = \Delta \cup r$ , mapping $f : D^2 \to D^2$

Meaning of Recursive and Iterative Constructs as Fixpoints of Relations

Consider program with single loop:

while (c) {
  s;
}

Using tail recursion, we could rewrite it as a procedure p such that

p = if (c) then (s;p) else skip

This can be written as

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

where

F(p) = if (c) then (s;p) else skip

How to give semantics to recursive definitions?

eliminate recursive by denoting left-hand side as the result of non-recursive function $F$
look for solution of $p=F(p)$ , which contains $p$ twice, so it expresses recursion
we can abstract the question of existence of values of recursive functions using fixpoints

If $r_s$ is meaning of $s$ and $\Delta_c$ is meaning of assume( c ), the meaning is the fixpoint of function

$\begin{equation*} f(r) = (\Delta_c \circ r_s \circ r) \cup \Delta_{\lnot c} \end{equation*}$

Any program can be reduced to a loop:

introduce program counter and iterate until it reaches exit point
more generally, can write an interpreter that interprets the program

Recall Relational semantics of procedures.

What is the fixpoint of the recursive function $f(x)=1+f(x)$ mapping integers to integers?

we need ordering to ensure existence of fixpoints
relations have a natural subset ordering
relation does not always represent terminating computation

Reachable States and Collecting Semantics

Main question: What values can variables of the program take at different program points?

We can represent programs by control-flow graphs (CFG).

Definition: Control flow-graph is a graph with nodes $V$ , edges $E \subseteq V\times V$ and for each edge $e \in E$ a command $c(e)$ , with initial $init$ and final node $final$

Program points are CFG nodes. Statements are labels on CFG edges.

We look at a particular way of representing and computing sets of reachable states, splitting states by program counter (control-flow graph node): collecting semantics.

$PS$ - the set of values of program variables (not including program counter).

For each program point $p$ , we have the set of reachable states $C(p) \subseteq PS$ .

The set of all reachable states of the program is $\{(p,s) \mid s \in C(p) \}$ .

Let $p_0$ be initial program counter and $I$ the set of values of program variables in $p_0$ .

The set of reachable states is defined as the least solution of constraints:

$\begin{equation*} I \subseteq C(p_0) \end{equation*}$

$\begin{equation*} \bigwedge_{(p_1,p_2) \in E} sp(C(p),r(c(p_1,p_2)))) \subseteq C(p_2) \end{equation*}$

where $c(p_1,p_2)$ is command associated with edge $(p_1,p_2)$ , and $r(c(p_1,p_2))$ is the relation giving semantics for this command.