Abstract Interpretation - Formalization

Formalization

Let L be an ordered set, called a concrete set and let L′ be another ordered set, called an abstract set. These two sets are related to each other by defining total functions that map elements from one to the other.

A function α is called an abstraction function if it maps an element x in the concrete set L to an element α(x) in the abstract set L′. That is, element α(x) in L′ is the abstraction of x in L.

A function γ is called a concretization function if it maps an element x′ in the abstract set L′ to an element γ(x′) in the concrete set L. That is, element γ(x′) in L is a concretization of x′ in L′.

Let L₁, L₂, L′₁ and L′₂ be ordered sets. The concrete semantics f is a monotonic function from L₁ to L₂. A function f′ from L′₁ to L′₂ is said to be a valid abstraction of f if for all x′ in L′₁, (f ∘ γ)(x′) ≤ (γ ∘ f′)(x′).

Program semantics are generally described using fixed points in the presence of loops or recursive procedures. Let us suppose that L is a complete lattice and let f be a monotonic function from L into L. Then, any x′ such that f′(x′) ≤ x′ is an abstraction of the least fixed-point of f, which exists, according to the Knaster–Tarski theorem.

The difficulty is now to obtain such an x′. If L′ is of finite height, or at least verifies the ascending chain condition (all ascending sequences are ultimately stationary), then such an x′ may be obtained as the stationary limit of the ascending sequence x′_n defined by induction as follows: x′₀=⊥ (the least element of L′) and x′_n+1=f′(x′_n).

In other cases, it is still possible to obtain such an x′ through a widening operator ∇: for all x and y, x ∇ y should be greater or equal than both x and y, and for any sequence y′_n, the sequence defined by x′₀=⊥ and x′_n+1=x′_n ∇ y′_n is ultimately stationary. We can then take y′_n=f′(x′_n).

In some cases, it is possible to define abstractions using Galois connections (α, γ) where α is from L to L′ and γ is from L′ to L. This supposes the existence of best abstractions, which is not necessarily the case. For instance, if we abstract sets of couples (x, y) of real numbers by enclosing convex polyhedra, there is no optimal abstraction to the disc defined by x2+y2 ≤ 1.