where D? = N [ f?g.
In most cases we are only interested in determining some properties of the
semantics of a system speci ed by a set A of abstract objects. Formally, an
abstract interpretation2 for a concrete domain C is a pair (A; ) where A is
partially ordered by A (the approximation ordering ) and : C ! A maps every
semantic property to the strongest (smallest) abstract property it enjoys. An
1 For easiness of presentation, we do not consider here higher-order functions.
2 The abstract interpretation framework here used is the one presented in [
> (str if f (?) = ?, otherwise.
Clearly, str (JprogK) = str since prog describes a strict function. 1.1
Collecting Semantics
In most cases abstract interpretations are de ned starting from a so-called
collecting semantics. According to [
For example, consider the collecting semantics CS1 for the concrete domain
C = D? ! D? de ned in [
CS1 (f ) = X 2 P(D?):f (X), where f (X) is the image of f through X. It turns out that strictness may be derived from CS1. Actually, we have that: { { str (f ) str (f ) CS1 (f?g) > is always true, hence it is equivalent to CS1 (f ) X:D?; str means that f is a strict function, which is equivalent to f?g, i.e., CS1 (f ) str by de ning str =
X: (X
D? if X f?g, otherwise.
However, not all the abstractions may be recovered from CS1. Consider the
property of absence. We say that a function is absent if it ignores its arguments.
This gives origin to the absence abstract interpretation [
> (abs if 8x 2 D?: f (x) = f (?),
otherwise.
It turns out that absence cannot be recovered from CS1, since there is no element
in the abstract domain of CS1 which exactly corresponds to the set of all the
absent functions. However, more precise collecting semantics may be used to
derive abs, such as CS2 [
We now formalize the notion of precision which arises from the previous considerations and characterize the collecting semantics using the category theory3. We recall that a Galois connection (Gc) is a pair of maps h ; i : A B such that (a) b , a (b). Given a set C, we de ne the category AI(C) whose objects are abstract interpretations and whose morphisms from (A; A) to (B; B) are Galois connections h ; i : A B such that B = A. Identity and composition of arrows work as in the category of Galois connections. This de nition of the category of abstract interpretations naturally arises from the practical uses of abstract interpretation and represents a strengthening of the notion of derivability between abstractions, since the existence of a morphism h ; i : A B implies that B is derivable from A. The following proposition shows that there is a Gc from CS2 to CS1 but not from CS1 to CS2, which re ects our intuition that CS2 is strictly more precise than CS1, and that CS1 is a suitable collecting semantics for strictness but not for the absence property.
Proposition 1. The following properties hold: { there is no Gc h 12; 12i : CS1 { there is a Gc h 21; 21i : CS2 { there is a Gc h 1str ; 1str i : CS1
CS2 such that CS2 = CS1 such that CS1 =
Str such that str = When an abstract interpretation (A; A) is designed starting from the collecting semantics (S; S ), it means that (A; A) is derivable from (S; S ), hence there is a map from (S; S ) to (A; A) in our category AI(C). In addition, it would be preferable to have a canonical way of deriving one from the other. This leads to the notion of initial object in a category: if (S; S ) is initial for a given full subcategory D of AI(C), it means that all the abstract interpretations in D may be reduced to (S; S ) in a unique canonical way.
Given a collecting semantics (S; S ), we are interested in characterizing the
maximal full subcategory D of AI(C) such that (S; S ) is initial for D. Such
subcategories immediately induce a taxonomy on program analysis which precisely
characterizes the program properties suitable for a given collecting semantics.
3 Since the very beginning of the abstract interpretation theory, there have been work
on categorical approaches to abstract interpretation (see, for instance, [
We rst show that CS2 is initial for all the abstract interpretations which have enough joins, and that this is the largest class of abstract interpretations which enjoys this property.
De nition 2 (Having enough joins). We say that the abstract interpretation (A; A) has enough joins when WA X exists for each X which is a subset of the image of A.
Obviously, if A is a complete join-semilattice, than (A; A) has enough joins. Theorem 3. The full subcategory of all the abstract interpretations which have enough joins is the largest class of abstractions for which the collecting semantics CS2 is initial.
The maximality of the class of abstract interpretations which have enough joins allows us to completely characterize the analyses which reduce to the collecting semantics CS2. We now show that the collecting semantics CS1 is initial for a large class of abstract interpretations, which can be constructively characterized. De nition 4 (Mix of functions). We say that a function g : D? ! D? is a mix of the set of functions F D? ! D? i for each x 2 D? there exists f 2 F such that g(x) = f (x).
De nition 5 (Mixable interpretations). Let (A; A) be an abstract interpretation such that A has enough joins. We call (A; A) mixable if, for any set of functions F D? ! D?, whenever g is a mix of functions in F , we have A(g) W A(f ).
f2F
An interpretation is mixable when deciding whether (f ) a may be done by looking at the values of f for a single element of the domain at a time. This observation is formalized by the following lemma.
Lemma 6. Let (A; A) be a mixable interpretation. Then D? 9f 0 s.t. f 0(x) = f (x) ^ A(f 0) a.
A(f ) a () 8x 2 This lemma can be exploited to characterize mixable abstract interpretations: { the strictness abstract interpretation is mixable, since we only need to check the single value of f (?) in order to decide whether a function is strict; { the absence abstract interpretation is not mixable, since we need to compare the values computed by f for di erent arguments; { the totality abstract interpretation, which decides whether a function is total, i.e., for all x 2 D? n f?g we have that f (x) 6= ? is mixable, since we just need to see the value of f for (many) single arguments, without the need of comparing them.
We now show that all the mixable interpretations may be designed starting from the collecting semantics CS1.
Theorem 7. The full subcategory of all the mixable abstract interpretations is the largest class of abstractions for which the collecting semantics CS1 is initial.
Static analyses formalized in the abstract interpretation framework are de ned
starting from a collecting semantics, which is a fundamental choice in the design
of any abstract interpretation, but few works in the literature systematically
study collecting semantics. [