Review of Fixpoints in Semantics

Transitive Closure as Least Fixedpoint

Recall the definition of transitive closure for a binary relation where .

Lemma: Reflexive transitive closure is the least fixpoint of function , mapping 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 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 • look for solution of , which contains twice, so it expresses recursion
• we can abstract the question of existence of values of recursive functions using fixpoints

If is meaning of and is meaning of assume( c ), the meaning is the fixpoint of function 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

What is the fixpoint of the recursive function 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 , edges and for each edge a command , with initial and final node 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. - the set of values of program variables (not including program counter).

For each program point , we have the set of reachable states .

The set of all reachable states of the program is .

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

The set of reachable states is defined as the least solution of constraints:  where is command associated with edge , and is the relation giving semantics for this command.