# Collecting Semantics for Example Program

The general form of collecting semantics is:

Here will be 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 (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 .