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