Collecting Semantics for Example Program

The general form of collecting semantics is:  Here will be except at the entry into our control-flow graph.

// 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 (value of )
• sets of states are sets of integers, (concrete domain)
• for each command , strongest postcondition function Strongest Postondition

Compute or example statements:    Sets of States at Each Program Point

Collecting semantics computes with sets of states at each program point We sometimes write as a shorthand for , for .

In the initial state the value of variable is arbitrary: post Function for the Collecting Semantics

From here we can derive that maps to new value of : The fixpoint condition becomes a system of inequations whereas the postfix point (see Tarski's fixpoint theorem) becomes Computing Fixpoint

To find fixpoint, we compute the sequence for : Thus, all subsequent values remain the same and 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 such that 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: where on a tuple above means taking union of each component separately, so .