Termination and Efficiency of Abstract Interpretation Analysis

Definition: A chain of length is a sequence such that

where means, as usual,

Definition: A partial order has a finite height if it has a chain of length and every chain is of length at most .

A finite lattice is of finite height

Example: The constant propagation lattice is an infinite lattice of height 2. One example chain of length 2 is

Here the function is given by

• when

The ordering is given by iff

Example: If a state of a (one-variable) program is given by an integer, then a concrete lattice element is a set of integers. This lattice has infinite height. There is a chain

for every .

Convergence in Lattices of Finite Heignth

Consider a finite-height lattice of height and function

What is the maximum length of sequence ?

Give an effectively computable expression for .

Computing the Height when Combining Lattices

Let denote the height of the lattice .

Product

Given lattices and , consider product lattice with set and potwise order

iff

What is the height of the product lattice?

Exponent

Given lattice and set , consider the lattice defined by

iff .

What is the height of the exponent lattice?

Answer: height of times the cardinality of .