Collecting Semantics for Example Program

The general form of collecting semantics is:

$\begin{equation*} F : (V \to 2^S) \to (V \to 2^S) \end{equation*}$

$\begin{equation*} F(g)(v') = g_{init}(v') \cup \bigcup_{(v,v') \in E} sp(g(v),r(v,v')) \end{equation*}$

Here $g_{init}(v')$ will be $\emptyset$ except at the entry into our control-flow graph.

Example Program with One Variable

// v0
x := 0;
// v1
while (x < 10) {
  // v2
  x := x + 3;
}
// v3

Concrete Domain: Sets of States

Because there is only one variable:

state is an element of $\mathbb{Z}$ (value of $x$ )
sets of states are sets of integers, $C = 2^\mathbb{Z}$ (concrete domain)
for each command $K$ , strongest postcondition function $sp(\cdot,K) : C \to C$

Strongest Postondition

Compute $sp$ or example statements:

$\begin{equation*} sp(P, x:=0) = \{ 0 \} \end{equation*}$

$\begin{equation*} sp(P, x:=x+3) = \{ x+3 \mid x \in P \} \end{equation*}$

$\begin{equation*} sp(P, assume(x<10)) = \{ x \mid x \in P \land x < 10 \} \end{equation*}$

$\begin{equation*} sp(P, assume(\lnot (x < 10)) = \{ x \mid x \in P \land x \ge 10 \} \end{equation*}$

Sets of States at Each Program Point

Collecting semantics computes with sets of states at each program point

$\begin{equation*} g : \{ v_0, v_1, v_2, v_3 \} \to C \end{equation*}$

We sometimes write $g_i$ as a shorthand for $g(v_i)$ , for $i \in \{0,1,2,3\}$ .

In the initial state the value of variable is arbitrary: $I = \mathbb{Z}$

post Function for the Collecting Semantics

From here we can derive $F$ that maps $g$ to new value of $g$ :

$\begin{equation*} \begin{array}{l} F(g_0,g_1,g_2,g_3) = \\ \begin{array}[t]{l} (\mathbb{Z}, \\ sp(g_0, x:=0) \cup sp(g_2, x:=x+3),\\ sp(g_1, assume(x < 10)), \\ sp(g_1, assume(\lnot(x<10)))) \end{array} \end{array} \end{equation*}$

The fixpoint condition $F(g) = g$ becomes a system of inequations

$\begin{equation*} \begin{array}[t]{l} g_0 = \mathbb{Z} \\ g_1 = sp(g_0, x:=0) \cup sp(g_2, x:=x+3)\\ g_2 = sp(g_1, assume(x < 10)) \\ g_3 = sp(g_1, assume(\lnot(x<10)))) \end{array} \end{equation*}$

whereas the postfix point (see Tarski's fixpoint theorem) becomes

$\begin{equation*} \begin{array}[t]{l} \mathbb{Z} \subseteq g_0 \\ sp(g_0, x:=0) \cup sp(g_2, x:=x+3) \subseteq g_1 \\ sp(g_1, assume(x < 10)) \subseteq g_2 \\ sp(g_1, assume(\lnot(x<10))) \subseteq g_3 \end{array} \end{equation*}$

Computing Fixpoint

To find fixpoint, we compute the sequence $F^n(\emptyset,\emptyset,\emptyset,\emptyset)$ for $n \ge 0$ :

$\begin{equation*} \begin{array}{l} (\emptyset,\emptyset,\emptyset,\emptyset) \\ (\mathbb{Z},\emptyset,\emptyset,\emptyset) \\ (\mathbb{Z},\{0\},\emptyset,\emptyset) \\ (\mathbb{Z},\{0\},\{0\},\emptyset) \\ (\mathbb{Z},\{0,3\},\{0\},\emptyset) \\ (\mathbb{Z},\{0,3\},\{0,3\},\emptyset) \\ (\mathbb{Z},\{0,3,6\},\{0,3\},\emptyset) \\ (\mathbb{Z},\{0,3,6\},\{0,3,6\},\emptyset) \\ (\mathbb{Z},\{0,3,6,9\},\{0,3,6,9\},\emptyset) \\ (\mathbb{Z},\{0,3,6,9,12\},\{0,3,6,9\},\emptyset) \\ (\mathbb{Z},\{0,3,6,9,12\},\{0,3,6,9\},\{12\}) \\ (\mathbb{Z},\{0,3,6,9,12\},\{0,3,6,9\},\{12\}) \\ \end{array} \end{equation*}$

Thus, all subsequent values remain the same and $(\mathbb{Z},\{0,3,6,9,12\},\{0,3,6,9\},\{12\})$ is the fixpoint of collecting semantics equations. In general we may need infinitely many iterations to converge.

Question: Suppose that we have a program that terminates for every possible initial state. Can we always find a finite constant $n$ such that

$\begin{equation*} F^n(\emptyset,\ldots,\emptyset)=F^{n+1}(\emptyset,\ldots,\emptyset) \end{equation*}$

i.e. the sequence such as the one above is guaranteed to stabilize?

Example: Assume an arbitrary initial value and consider the loop. Compute a sequence of sets of states at the point after the increment statement in the loop, following the equations for collecting semantics.

if (y > 0) {
  x = 0
  while (x < y) {
    x = x + 1
  }
}

What always works from omega continuity:

$\begin{equation*} lfp(F) = \bigcup_{n \ge 0} F^n(\emptyset,\ldots,\emptyset) \end{equation*}$

where $\bigcup$ on a tuple above means taking union of each component separately, so $(A,B) \cup (A',B') = (A \cup A', B \cup B')$ .