Complementation in Abstract Interpretation

AGOSTINO CORTESI Università di Venezia GILBERTO FILÉ Università di Padova ROBERTO GIACOBAZZI Università di Pisa CATUSCIA PALAMIDESSI Università di Genova and FRANCESCO RANZATO Università di Padova

Reduced product of abstract domains is a rather well-known operation for domain composition in abstract interpretation. In this article, we study its inverse operation, introducing a notion of domain complementation in abstract interpretation. Complementation provides a systematic way to design new abstract domains, and it allows to systematically decompose domains. Also, such an operation allows to simplify domain verification problems, and it yields space-saving representations for complex domains. We show that the complement exists in most cases, and we apply complementation to three well-known abstract domains, notably to Cousot and Cousot’s interval domain for integer variable analysis, to Cousot and Cousot’s domain for comportment analysis of functional languages, and to the domain Sharing for aliasing analysis of logic languages.

Categories and Subject Descriptors: D.3.1 [Programming Languages]: Formal Definitions and Theory—semantics; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs—logics of programs

General Terms: Languages, Theory Additional Key Words and Phrases: Abstract domain, abstract interpretation, closure operator, complementation, functional and logic programming, program analysis

The work of R. Giacobazzi has been partly supported by the EEC-HCM individual grant: “Semantic Definitions, Abstract Interpretation and Constraint Reasoning,” n. ERBCHBICT930822. The work of A. Cortesi and G. Filé has been partly supported by “MURST-NRP: Modelli della Computazione e dei Linguaggi di Programmazione.” A preliminary version of this article appeared in Proceedings of the 2nd International Static Analysis Symposium (SAS ’95 ), Glasgow, September 1995. Authors’ addresses: A. Cortesi, Università di Venezia, Dipartimento di Matematica Applicata e Informatica, Via Torino 155, 30173 Mestre-Venezia, Italy; email: cortesi@moo.dsi.unive.it; G. Filé and F. Ranzato, Università di Padova, Dipartimento di Matematica Pura ed Applicata, Via Belzoni 7, 35131 Padova, Italy; email: {gilberto; franz}@math.unipd.it; R. Giacobazzi, Università di Pisa, Dipartimento di Informatica, Corso Italia 40, 56125 Pisa, Italy; email: giaco@di.unipi.it; C. Palamidessi, Università di Genova, Dipartimento di Informatica e Scienze dell’Informazione, Via Dodecaneso 35, 16146 Genova, Italy; email: catuscia@disi.unige.it. Permission to make digital/hard copy of all or part of this material without fee is granted provided that the copies are not made or distributed for profit or commercial advantage, the ACM copyright/server notice, the title of the publication, and its date appear, and notice is given that copying is by permission of the Association for Computing Machinery, Inc. (ACM). To copy otherwise, to republish, to post on servers, or to redistribute to lists requires prior specific permission and/or a fee.

ACM Transactions on Programming Languages and Systems, Vol. 19, No. 1, January 1997, Pages 7–47.

8 · Cortesi et al.

1. INTRODUCTION

Abstract interpretation is a general theory, introduced by Cousot and Cousot [1977; 1979], for describing the relationship among semantics of programming languages at different levels of abstraction. In this framework, program analysis is defined as nonstandard program semantics, obtained from the standard one by substituting its domain of computation, called concrete, (and the basic operations on it) with an abstract domain (and corresponding abstract operations). The concrete and the abstract domains are always complete lattices, where the ordering relations describe the relative precision of the denotations, the top elements representing no information. For example, assume that the concrete domain is the powerset ℘(ZZ) of integer numbers. This may be the case whenever we perform a static analysis on variables assuming integer values. Possible abstract domains are depicted in the picture below. The interpretation of their elements is straightforward: for instance, 0+ represents the set of nonnegative integers whereas − represents the set of negative integers.

• • • + 0+ ZZA^{+}  • • • −0 ZZA^{−}  [figure: •; •; •; •; •; •; •; −; −0; ∅; 0; ZZ; 0+; +; Sign]

The relation of abstraction between abstract domains is traditionally formalized in terms of Galois insertions (cf. Cousot and Cousot [1977]). A domain D is an abstraction of C, if there exists a monotone abstraction function α : C → D, which is part of a Galois insertion. This happens whenever α is surjective, i.e., all the elements of D are approximations of elements in C, and if c ∈ C is such an element, then α(c) ∈ D is the least (unique) element in D which corresponds to an object in C approximating the meaning of c. This correspondence is defined in terms of an adjoint function γ : D → C, providing a representation in C for the elements of D. The relation between domains established by a Galois insertion ensures that the abstract domain contains only the best (viz., most precise) approximations of the elements of the concrete one. This is the case of A^{+} and Sign in the example above. In this case, −0 ∈ Sign is abstracted into ZZ of A^{+}, which corresponds to the least set in A^{+} containing nonpositive numbers, while 0 ∈ Sign is approximated by 0+ ∈ A^{+}, which corresponds to the least set in A^{+} containing 0.

Already in their early works Cousot and Cousot [1977; 1979], have pointed out the importance of incrementally designing abstract domains. Richer domains can be obtained by combining simpler ones or by lifting them by systematically adding new information. The first kind of operations are known as domain combinators, while the latter ones are known as domain completions. Both operations are devoted to enhance the expressive power of domains and have been called domain refinements (cf. Filé et al. [1996]). All these domain operations provide high-level facilities to tune the analysis in accuracy and cost. Among these operations for domain refinement, reduced product [Cousot and Cousot 1979] is probably the most common and widely known one. It has been included as an important tool for design aid

ACM Transactions on Programming Languages and Systems, Vol. 19, No. 1, January 1997.

Complementation in Abstract Interpretation · 9

in many modern systems for program analysis, like for instance in System Z [Yi and Harrison 1993]. In Codish et al. [1995] the cost/precision tradeoff between using two separate abstract domains and using their reduced product has been experimentally evaluated for the analysis of logic programs in the system PLAI.

Reduced product corresponds to cartesian product of domains, where equivalent tuples are identified, viz., reduced. Let us use the abstract domains introduced above in order to illustrate reduced product. The reduced product of A^{+} and A^{−} is Sign. Observe that Sign has two new elements with respect to A^{+} and A^{−}: 0 and ∅. These elements are obtained by combining, by conjunction, which is set intersection of the corresponding sets of integers, respectively, 0+ with −0 and + with −. In this example, reduction is necessary only for identifying distinct pairs of elements denoting ∅, as, for instance, the pairs ⟨+, −⟩ and ⟨+, −0⟩.

The Problem: Domain Decomposition in Abstract Interpretation. A natural question that arises in this setting is whether it is possible to define the inverse of reduced product, namely an operation which, starting from any two domains C and D, with D more abstract than C, gives as result the most abstract domain C ∼ D, whose reduced product with D is exactly C. Recall that in the setting of abstract interpretation a domain D is more abstract than C, if C contains all the information of D, by simplifying: D ⊆ C, up to isomorphic representation of domain objects. In the example above, for instance, A^{+} is more abstract than Sign.

Because of the peculiar structure of domains in abstract interpretation, the above problem cannot be solved by simply considering the set-theoretic complement C \D of D into C. This is because the result would not be in general an abstract domain. In our example, for instance, Sign \ A^{+} = {−0, −, 0, ∅} is not an abstract domain: in particular, Sign \ A^{+} does not contain any correct (with respect to the standard meaning of signs as sets of integers) denotation representing no information at all, namely denoting the set of all integers. In contrast, it is easy to verify that the domains A^{−} and Sign above, and the domains A^{−∅}, A^{−0}, A^{(−0)+}, and A^{±0} depicted below, are all and only those abstractions of Sign which, once combined with A^{+} by reduced product, give Sign back.

[figure: • • • • ∅ −0 ZZA^{−∅}; •; •; •; •; •; ∅; 0; −; −0; ZZ; A^{−0}; •; •; •; •; •; −; −0; ∅; ZZ; +; A^{(−0)+}; •; •; •; •; •; •; −; −0; ∅; 0; ZZ; 0+; A^{±0}]

It is worth noting that A^{−} is contained in (viz., more abstract than) all these domains. Hence, in this sense, A^{−} = Sign ∼ A^{+}. The main question is therefore whether for any two domains C and D as above, the domain C ∼ D always exists. A positive answer to this question would fill one gap of abstract interpretation theory, providing a methodology for systematic domain decomposition. This is important for several reasons. First, it can be useful for designing new abstract domains and for minimizing their space requirement, yielding compact representations for complex domains as tuples of simpler (i.e., more abstract) factors. This can be particularly interesting for those domains that were not originally designed through composition, which is the case for most of the abstract domains used in

ACM Transactions on Programming Languages and Systems, Vol. 19, No. 1, January 1997.

practical analyses. Furthermore, decomposing domains allows to decompose also their verification. In fact, instead of proving some property for a complex domain, it may be convenient to verify it for the simpler components of a decomposition of this domain. Clearly, this is a viable technique only provided that the considered property is preserved under reduced product. Finally, domain decomposition helps to understand the internal structure of complex domains, which, as already observed, are in most cases defined as a whole and not by composition of elementary domains. Such an operation would allow to show for instance that Sign∼A^{+} = A^{−} and Sign ∼ A^{−} = A^{+}, and thus that ⟨A^{+}, A^{−}⟩ provides a minimal way of decomposing Sign, in the sense that no component can be simplified without changing the other one.

The Idea: Pseudocomplementation for Domain Decomposition. In order to solve the problem of inverting reduced product in a general setting, i.e., for any domain in abstract interpretation, we need a formal framework, where properties of abstract domains can be studied independently from the representation of their objects. In fact, the definition of abstraction in terms of Galois insertions suffers from being dependent on the way domain objects are represented.

The closure operator approach to abstract interpretation provides a very useful mathematical framework for studying abstract domains and in particular the above operation for domain decomposition. The equivalence between Galois insertions and closure operators is well known in lattice theory (cf. Birkhoff [1967]). Cousot and Couost [1979] applied this equivalence, observing that every abstraction of a concrete domain C can be associated with an (upper) closure operator on C, and the operation of reduced product between abstract domains can be interpreted as the corresponding lattice-theoretic operation of greatest lower bound ⊓ on the complete lattice uco(C) of all (upper) closure operators on C. Closure operators play here the role of approximating operations. The intuition behind this construction is simple. A closure operator ρ : C → C is a function which is monotonic, idempotent (i.e., ρ(ρ(c)) = ρ(c)), and extensive (i.e., ρ(c) ≥ c). Monotonicity ensures that the abstraction monotonically approximates domain objects. Idempotence ensures that the approximation is performed all at once, while extensivity captures the situation where the approximation of an object c contains all the information in c. Closure operators capture therefore the essence of the process of abstraction. Moreover, they have the advantage of simplicity, e.g., one single function, and specify abstractions independently from isomorphic representation of domain objects. Hence, they provide precisely the right high-level setting which is needed when reasoning about properties of abstract domains. For example, it is easy to verify that A^{+} and A^{−} correspond, up to object names, to the image of Sign under the following closure operators:

ρ_{A^{+}}(x) = \{ \begin{matrix}x & if x ∈ \{+, 0+, ZZ\} \\ 0+ & if x = 0 \\ + & if x = ∅ \\ ZZ & if x ∈ \{−, −0\}; \end{matrix} ρ_{A^{−}}(x) = \{ \begin{matrix}x & if x ∈ \{−, −0, ZZ\} \\ −0 & if x = 0 \\ − & if x = ∅ \\ ZZ & if x ∈ \{+, 0+\}. \end{matrix}

The lattice of abstract interpretations of a domain C is therefore isomorphic to the lattice uco(C) of closure operators on C. The bottom element in uco(C) cor-

ACM Transactions on Programming Languages and Systems, Vol. 19, No. 1, January 1997.

responds to the identical abstraction, which leaves C unchanged, while the top element corresponds to the straightforward abstraction, which forgets about the whole structure of C, mapping C into its top element. In this setting, asking whether C ∼ D exists for any C and D (with D abstracting C) is equivalent to ask whether uco(C) is pseudocomplemented. Being a pseudocomplement of D in uco(C) for a domain (closure operator) C ∼ D means that whenever there exists another domain X, such that D ⊓ X = C, then X is always more concrete than C ∼ D. Therefore, in the context of abstract interpretation, the lattice-theoretic notion of pseudocomplementation [Birkhoff 1967] captures precisely the intended meaning of inverting reduced product. In the example above, it is easy to see that A^{+} ⊓ A^{−} = Sign, and for any domain X such that A^{+} ⊓ X = Sign, e.g., X = A^{−0}, X contains Sign∼A^{+} = A^{−}.

The attentive reader may wonder why we have defined the operation ∼ as the pseudocomplement instead of the complement, which would additionally require that the least upper bound of C ∼ D and D in uco(C) is the top element. This is the case in our example, where the most abstract domain (viz., the top closure) {ZZ} is the only common abstraction of A^{+} and A^{−}. Although some closure (domain) may have accidentally a complement, this is not true in general, i.e., for any closure. This would clearly correspond to requiring that uco(C) is complemented, but Dwinger [1954] and, successively, Morgado [1962] proved that uco(C) is complemented if and only if C is a complete well-ordered chain. This condition is clearly too restrictive to be applied in static analysis and abstract interpretation of programming languages, because concrete and abstract domains for semantics and analysis in general are not complete chains. On the contrary, the requirement that uco(C) is pseudocomplemented can be met in most cases of interest. In fact, recently, Giacobazzi et al. [1996] have given a sufficient condition for uco(C) to be pseudocomplemented. In the present article, we point out that this condition is satisfied by most of the known concrete and abstract domains for semantics and analysis of programming languages.

Structure of the Article. On the basis of the result in Giacobazzi et al. [1996], we define the operation of pseudocomplementation of abstract domains. For the sake of simplicity, this operation will be simply called complementation. We study the basic properties of complementation for abstract domain decomposition, and we provide a constructive iterative characterization of complements. We introduce the notion of minimal decomposition for an abstract domain, and we provide an iterative method to construct minimal decompositions, i.e., decompositions of domains involving the most abstract factors. The usefulness of complementation for domain decomposition is illustrated by means of several examples. First, we consider some general properties of domains which can be verified compositionally on the simpler factors of their decompositions. Then, we apply domain decomposition to specific well-known domains for program analysis. Cousot and Cousot’s [1976; 1977] domain for integer interval analysis of programs with integer variables provides the first simple, but useful, example for explaining some subtle technical points of the complementation. More complex examples of the use of complementation for domain decomposition are given by considering a domain for aliasing analysis in logic programming, notably Sharing, introduced by Jacobs and Langen [1989; 1992],

ACM Transactions on Programming Languages and Systems, Vol. 19, No. 1, January 1997.

and Cousot and Cousot’s [1994] domain for comportment analysis for higher-order functional languages.

The domain for comportment analysis was originally obtained by disjunctive completion of a simpler domain of basic comportments for functions. We prove that the domain of basic comportments can be decomposed by complementation as reduced product of Mycroft’s [1980; 1981] domains for termination and strictness analysis. This provides a reduction of the lattice-structure of comportments as well as an intuitive interpretation of comportment analysis as the space of relations between the domains for termination and strictness. For the sake of simplicity, the domain of comportment analysis is considered for the case of functional basic types only.

We use complementation for decomposing Sharing into a component expressing the ability of Sharing to compute ground dependency information and a component expressing the remaining information of Sharing. Cortesi et al. [1992] proved that the information for ground dependency analysis of Sharing is expressed by a more abstract domain, which we show to coincide with the domain Def for ground dependency analysis. Def was introduced by Marriott and Søndergaard [1993], as an adaptation of Dart’s [1988; 1991] work on groundness in deductive databases. As expectable, the complement of Def relative to Sharing, called Sharing^{+}, captures precisely variable aliasing and no ground dependency information. It is worth mentioning that Sharing^{+} corresponds to a simple and elegant closure operator on Sharing.

The rest of the article is organized as follows. Section 2 contains some preliminaries about lattice theory and abstract interpretation. Section 3 introduces the notion of complementation of abstract domains and studies its properties. In this section, we also give the constructive fixpoint characterization of complementation of closure operators, which is the basis for an iterative construction of complements of abstract domains. Section 4 gives systematic ways to decompose domains and exemplifies how the notion of complementation actually works. In Section 5 we give some examples of domain properties which can be verified on the simpler factors of their decompositions. Section 6 presents complements of some abstractions of Cousot and Cousot’s integer interval domain. Section 7 provides decompositions of Cousot and Cousot’s domain for comportment analysis. Section 8 describes the application of the complement to the domain Sharing. Section 9 concludes.

2. PRELIMINARIES

Throughout the article, we will assume familiarity with the basic notions of lattice theory (e.g., see Birkhoff [1967], Davey and Priestley [1990], and Grätzer [1978]) and abstract interpretation [Cousot and Cousot 1977; 1979]. Now, we briefly introduce some notation and recall some well-known notions.

2.1 Mathematical Notation

Let C and D be sets. The powerset of C is denoted by ℘(C), and the cardinality of C by |C|. The set-difference between C and D is denoted by C \ D. If f is a function defined on C and D ⊆ C then f(D) = {f(x) | x ∈ D}. By g ∘ f we denote the composition of the functions f and g, i.e., ∀x. (g ∘ f)(x) = g(f(x)). The set D equipped with a partial order ⪯ is denoted by ⟨D, ⪯⟩. If D is a poset, we usually

ACM Transactions on Programming Languages and Systems, Vol. 19, No. 1, January 1997.

denote by ⪯_{D} the corresponding partial order. A complete lattice D with partial order ⪯, greatest lower bound (glb) ∧, least upper bound (lub) ∨, top element ⊤ = ∧∅ = ∨D, and bottom element ⊥ = ∨∅ = ∧D is denoted by ⟨D, ⪯, ∧, ∨, ⊤, ⊥⟩. When D is a lattice, ∨_{D}, ∧_{D}, ⊤_{D}, and ⊥_{D} denote the corresponding basic operators and elements. In the following, we will often abuse notation by denoting lattices with their poset notation. We use C ≅ D to denote that the ordered structures C and D are isomorphic.

2.2 Galois Connections and Closure Operators

We recall the notions of Galois connection and insertion and closure operator, which are fundamental in the standard theory of abstract interpretation [Cousot and Cousot 1977; 1979]. If C and D are posets, and α : C → D, γ : D → C are monotonic functions such that ∀c ∈ C. c ⪯_{C} γ(α(c)) and ∀d ∈ D. α(γ(d)) ⪯_{D} d, then we call the quadruple (γ, D, C, α) a Galois connection (G.c.) between C and D. If in addition ∀d ∈ D. α(γ(d)) = d, then we call (γ, D, C, α) a Galois insertion (G.i.) of D in C. We also recall that the above definition of G.c. is equivalent to that of adjunction: (γ, D, C, α) is an adjunction if ∀c ∈ C.∀d ∈ D. α(c) ⪯_{D} d ⇔ c ⪯_{C} γ(d). Abstract interpretations are traditionally specified in terms of Galois insertions. Any G.c. may be lifted to a G.i. identifying in an equivalence class those values of the abstract domain with the same concrete meaning. This process is known as reduction of the abstract domain. In the setting of abstract interpretation, C and D are called, respectively, the concrete and the abstract domain, and they are assumed to be complete lattices, whereas α and γ are called the abstraction and the concretization maps, respectively. Also, D is called an abstraction (or abstract interpretation) of C, and C a concretization of D. Furthermore, if C is not an abstraction of D, then we say that D is a strict abstraction of C. Note that, if (γ, D, C, α) is a G.i., then the concretization and abstraction mappings, γ and α, are 1-1 and onto, respectively. In this case, each value of the abstract domain D is useful in the representation of the concrete domain C, as all the elements of D represent distinct members of C.

An (upper) closure operator, or simply a closure, on the poset ⟨L, ⪯⟩ is a monotonic, idempotent, and extensive (viz., ∀x ∈ L. x ⪯ ρ(x)) operator ρ : L → L. If ⟨L, ⪯, ∧, ∨, ⊤, ⊥⟩ is a complete lattice then each closure operator ρ is uniquely determined by the set of its fixpoints, which is its image ρ(L). A set X ⊆ L is the set of fixpoints of a closure operator iff X is a Moore-family of L, i.e., ⊤ ∈ X and X is meet-closed (viz., for any Y ⊆ X, ∧Y ∈ X). Furthermore, the set of fixpoints ρ(L) is a complete lattice with respect to the order of L, but, in general, it is not a complete sublattice of L, since the lub in ρ(L) might be different from that in L. Hence, in the following, a closure operator ρ will often denote the set of its fixpoints ρ(L). Being a set, the set of fixpoints of a closure is often denoted with capital Latin letters. Denoting closures by sets will be particularly convenient when closure operators will denote domains. In the following, we will keep Greek letters only as denotations for closures in lattice-theoretic notions and results and will use capital Latin ones to emphasize their role as domains. However, viewing closures as functions is also important in abstract interpretation, because they define the abstraction function. Hence, in the following, we will keep this soft ambiguity by using both notations and will leave to the reader to distinguish their use as func-

ACM Transactions on Programming Languages and Systems, Vol. 19, No. 1, January 1997.

tions or sets, according to the context. Ward [1942, Theorem 4.2] proved that if L is a complete lattice, then ⟨uco(L), ⊑, ⊓, ⊔, λx.⊤, λx.x⟩ is a complete lattice, where for every ρ, η ∈ uco(L), {ρ_{i}}_{i∈I} ⊆ uco(L), and x ∈ L:

—ρ ⊑ η iff ∀x ∈ L. ρ(x) ⪯ η(x), or, equivalently, ρ ⊑ η iff η(L) ⊆ ρ(L); —(⊓_{i∈I}ρ_{i})(x) = ∧_{i∈I}ρ_{i}(x); —(⊔_{i∈I}ρ_{i})(x) = x ⇔ ∀i ∈ I. ρ_{i}(x) = x; —λx.⊤ is the top element, whereas λx.x is the bottom element.

2.3 Abstract Interpretation and Closure Operators: Reduced Product Revisited

A key point in abstract interpretation theory [Cousot and Cousot 1979] is the equivalence between the Galois insertion and closure operator approach to the design of abstract domains. Usually, the Galois insertion approach is the most used. In this case, D is an abstraction of C if there exist α and γ such that (γ, D, C, α) is a Galois insertion. It is well known since Cousot and Cousot [1979] that the real essence of an abstract domain lies with the closure operator associated with the corresponding G.i. Actually, an abstract domain is just a “computer representation” of its logical meaning, namely its image in the concrete domain. In fact, using a different but lattice-theoretic isomorphic domain changes nothing in the abstract reasoning. This logical meaning of an abstract domain is exactly captured by the associated closure operator on the concrete domain. More formally, on one hand, if (γ, D, C, α) is a G.i. then the closure associated with D is the operator ρ = γ ∘ α on C. On the other hand, if ρ is a closure on C and ι : ρ(C) → D is an isomorphism of complete lattices (with inverse ι^{−1}) then (ι^{−1}, D, C, ι ∘ ρ) is a G.i. By the above equivalence, it is not restrictive, and often more convenient, to use the closure operator approach to reason about abstract properties up to isomorphic representations of abstract domains. Thus, in the rest of the article, we will feel free to use this approach most of the time, and whenever we will say that D is an abstraction of C (or C a concretization of D), we will mean that D ≅ ρ(C) for some closure ρ ∈ uco(C). It is well known [Cousot and Cousot 1979] that the order relation on uco(C) corresponds to the order by means of which abstract domains are compared with regard to their precision of representation. More formally, if ρ_{i} ∈ uco(C) and D_{i} ≅ ρ_{i}(C) (i = 1, 2), D_{1} is more precise than D_{2} iff ρ_{1} ⊑ ρ_{2} (i.e., ρ_{2}(C) ⊆ ρ_{1}(C)). Since, clearly, D_{1} is more precise than D_{2} iff there exists ρ ∈ uco(D_{1}) such that D_{2} ≅ ρ(D_{1}); then we can equivalently write D_{1} ⊑ D_{2}. Therefore, to compare domains with regard to their precision, we will only speak about abstractions between them and will use ⊑ to relate both nonhomogeneous domains, i.e., domains which are not Moore-families of the same concrete domain, and homogeneous domains, i.e., closure operators on a concrete domain. Further, because we will be independent from object representations in domains, we will often use the equality symbol = between domains instead of the more rigorous symbol of isomorphism ≅.

In view of this equivalence, the lub and glb on uco(C) get a clear meaning. Suppose {ρ_{i}}_{i∈I} ⊆ uco(C) and D_{i} ≅ ρ_{i}(C) for each i ∈ I. Any domain D isomorphic to the least upper bound (⊔_{i∈I}ρ_{i})(C) is the most concrete among the domains which are abstractions of all the D_{i}, i.e., D is the least common abstraction of all the D_{i}. The interpretation of the glb operation on uco(C) is twofold. First, any

ACM Transactions on Programming Languages and Systems, Vol. 19, No. 1, January 1997.

domain D isomorphic to the greatest lower bound (⊓_{i∈I}ρ_{i})(C) is (isomorphic to) the well-known reduced product [Cousot and Cousot 1979] of all the domains D_{i}. Further, the glb D, and hence reduced product, is the most abstract among the domains (abstracting C) which are more concrete than every D_{i}. Thus, we will denote reduced product of abstract domains by the glb symbol ⊓.

3. (PSEUDO)COMPLEMENTS OF ABSTRACT DOMAINS

A consequence of the isomorphism between the lattice of abstract interpretations of a concrete domain C and the corresponding lattice of closure operators uco(C) is that it is not possible, in general, to define the lattice-theoretic complement of abstract domains, i.e., for any domain D such that C ⊑ D, a domain D̄ such that D ⊓ D̄ = C and D ⊔ D̄ = {⊤_{C}}. This follows from results by Dwinger [1954] and Morgado [1962], saying that uco(C) is complemented (or a Boolean algebra) iff C is a complete well-ordered chain. A similar condition, on arbitrary complete chains, is also necessary and sufficient for uco(C) to be distributive [Dwinger 1954]. Both these conditions are clearly too restrictive for abstract interpretation of programming languages. The following example shows this problem in a simple finite lattice.

Example 3.1. Consider the following finite lattice C.

[figure: •; •; •; •; b; ⊤; a; ⊥]

The closure operators (or equivalently abstract interpretations) on C are the following:

ρ_{1} = {⊤}, ρ_{2} = {⊤, a}, ρ_{3} = {⊤, ⊥}, ρ_{4} = {⊤, b},
ρ_{5} = {⊤, a, ⊥}, ρ_{6} = {⊤, b, ⊥}, ρ_{7} = {⊤, a, b, ⊥}.

They form the lattice uco(C) depicted below.

[figure: •; •; •; •; •; •; •; ρ_{1}; ρ_{2}; ρ_{3}; ρ_{4}; ρ_{5}; ρ_{6}; ρ_{7}]

It is immediate to observe that uco(C) is not complemented. For instance, ρ_{3} does not have the complement in uco(C).

The idea of this article is to use a different and somehow weaker notion of complementation in uco(C) as a systematic approach for domain complementation in abstract interpretation. Indeed, while in general uco(C) is not complemented, it is always pseudocomplemented, as proved in Giacobazzi et al. [1996]. We recall the lattice-theoretic notion of pseudocomplement.

ACM Transactions on Programming Languages and Systems, Vol. 19, No. 1, January 1997.

Definition 3.2. Let ⟨L, ⪯, ∧, ⊥⟩ be a meet semilattice with bottom. The pseudocomplement of x ∈ L, if it exists, is the (unique) element x^{∗} ∈ L such that x ∧ x^{∗} = ⊥ and ∀y ∈ L. (x ∧ y = ⊥) ⇒ (y ⪯ x^{∗}). If every x ∈ L has the pseudocomplement, we say that L is pseudocomplemented.

Pseudocomplement is in this sense weaker than complement because, in general, if L is a lattice, the least upper bound between x and x^{∗} is not the top element of L. It is worth noting that if the pseudocomplement of x ∈ L exists then it is unique, and in a complete lattice L, it is always defined as (cf. Grätzer [1978])

x^{∗} = ∨{y ∈ L | x ∧ y = ⊥}.  (†)

Example 3.3. Consider the lattice uco(C) of closure operators of Example 3.1. It is easy to verify the following pseudocomplements for the elements in uco(C): ρ_{1}^{∗} = ρ_{7}, ρ_{2}^{∗} = ρ_{4}, ρ_{3}^{∗} = ρ_{7}, ρ_{4}^{∗} = ρ_{2}, ρ_{5}^{∗} = ρ_{4}, ρ_{6}^{∗} = ρ_{2}, and ρ_{7}^{∗} = ρ_{1}.

In the following, we assume that L is a complete lattice.

Definition 3.4. L is meet-continuous if, for any chain C ⊆ L and for each x ∈ L, x ∧ (∨C) = ∨_{y∈C}(x ∧ y).

Remark 3.5. It is worth noting that meet-continuity is strictly weaker than the well-known complete inf-distributivity property (viz., ∀x ∈ L.∀Y ⊆ L. x ∧ (∨Y) = ∨_{y∈Y} (x ∧ y)). For instance, any lattice satisfying the ascending chain condition is obviously meet-continuous, but not necessarily complete inf-distributive (which for a finite lattice amounts to be distributive). Moreover complete Heyting algebras, continuous, algebraic, arithmetic, completely distributive, and Boolean complete lattices are always meet-continuous [Gierz et al. 1980, p. 96].

This notion of meet-continuity is central in the following result.

Theorem 3.6 [Giacobazzi et al. 1996]. If L is meet-continuous then uco(L) is pseudocomplemented.

By the above remark, the following corollary is immediate.

Corollary 3.7. If L either satisfies the ascending chain condition, or it is a complete Heyting algebra, or continuous, or algebraic, or arithmetic, or completely distributive, or a Boolean lattice, then uco(L) is pseudocomplemented.

Therefore, it is possible to define a weaker notion of domain complementation for abstract interpretation, which is precisely pseudocomplementation. In this case, the abstract domain to factorize plays the role of L.

Suppose D is an abstraction of the complete lattice C, and assume that C is meet-continuous. Exploiting Theorem 3.6 we can give the following definition of the complement of abstract domains.

Definition 3.8. The complement of D relative to (or in) C is the complete lattice C ∼D given by the set of fixpoints of the pseudocomplement D^{∗} (in uco(C)) of D.

It is immediate to observe that if C ⊑ D then C ⊑ C ∼ D. Therefore, the complement C ∼D is an abstraction of C. By equation (†), the pseudocomplement of D is expressible as

D^{∗} = ⊔{E ∈ uco(C) | D ⊓ E = C}.

ACM Transactions on Programming Languages and Systems, Vol. 19, No. 1, January 1997.

This equality makes clear the meaning of the complement: C ∼ D is the most abstract among the domains (abstracting C and) such that their reduced product with D yields C. The following picture shows the relation between the different domains involved in complementation.

[figure: •; •; •; •; •; {⊤}; C ∼D; (C ∼D) ⊔ D; D; (C ∼D) ⊓ D = C; ⋮; abstract]

Moreover, C may be thought of either as a concrete domain or as an abstract domain. In both cases, the complement C ∼ D intuitively captures what program properties representable by the domain C are ignored and left out by its abstraction D, allowing to understand more in depth how the abstraction process led from C to D. By Definition 3.8, we fix in C the representation of the complement C ∼ D, being C ∼ D a closure on C. Hence, C ∼ D is often intended as a subset of C. Obviously, any other lattice isomorphic to C ∼D can be considered in all respects as the complement. From now on, whenever we will speak about complements, we will suppose that the conditions for their existence hold.

The following technical result is recalled from Cousot [1978, Theorem 4.2.0.4.7] and provides a simple way to generalize domain complementation to arbitrary abstractions in the lattice of abstract interpretations of a given domain. For the sake of completeness, we present a sketch of the proof.

Proposition 3.9 [Cousot 1978]. Let L be a complete lattice and η ∈ uco(L). Then, uco(η) ≅ ↑η = {ρ ∈ uco(L) | η ⊑ ρ}.

Proof Sketch. Let L be a complete lattice and η ∈ uco(L). Since η is a complete lattice, uco(η) is also a complete lattice. Clearly, the principal filter ↑η of uco(L) is a complete (sub)lattice too, and uco(η) and ↑ η are isomorphic complete lattices. Indeed, the isomorphism is given by the mappings Ψ : uco(η) →↑ η such that Ψ(μ) = μ ∘ η, and Φ :↑η → uco(η) such that ∀x ∈ η. Φ(ρ)(x) = ρ(x).

By this result, we can apply Theorem 3.6 to arbitrary pairs of elements in the lattice of abstract interpretations. In general, if C is a concrete domain, D an abstraction of C (i.e., D ∈ uco(C)), and E an abstraction of D (i.e., E ∈ uco(D)), then while the computation of D ∼ E requires that D is meet-continuous, the domain C can be merely a complete lattice. The complement D ∼E is given in this case by the set of fixpoints of the pseudocomplement E^{∗} = ⊔{X ∈ uco(D) | E ⊓ X = D}, which is a closure operator on D. Proposition 3.9 says that uco(D) and {X ∈ uco(C) | D ⊑ X} are isomorphic complete lattices. Hence, the complement D ∼ E can be equivalently obtained as a pseudocomplement on the more concrete domain C, using the isomorphism of Proposition 3.9. In fact, if, by the isomorphism of Proposition 3.9, we view E as a closure on C (viz., E = E ∘ D ∈ uco(C)), then E^{∗} = ⊔{X ∈ uco(C) | (E ∘ D) ⊓ X = D}, which corresponds precisely to the expected intuitive meaning of D ∼E as closure on C.

ACM Transactions on Programming Languages and Systems, Vol. 19, No. 1, January 1997.

Meet-continuity of the concrete domain of reference plays a central role in the existence of the complement (cf. Theorem 3.6). Giacobazzi et al. [1996] observed that meet-continuity is preserved by continuous closures (η ∈ uco(L) is continuous if for any chain C ⊆ L, η(∨C) = ∨η(C)).

Proposition 3.10 [Giacobazzi et al. 1996]. If L is meet-continuous, and η ∈ uco(L) is continuous, then η(L) is meet-continuous.

Therefore, this result provides a sufficient condition on the closure defining an abstract domain D in order to verify the meet-continuity of D.

The following algebraic properties of the complement operation∼on abstract domains can be easily derived from similar properties of pseudocomplemented lattices (see Birkhoff [1967], Frink [1962], Grätzer [1978], and Varlet [1963]). Note that (j) includes one of De Morgan’s laws.

Proposition 3.11. Let C be a meet-continuous lattice, C ⊑ D, E, and C ⊑ D_{i} for each i ∈ I. Define ⊤ as the most abstract interpretation of C. Then,

(a) D ⊑ C ∼(C ∼D);
(b) (D ⊑ E) ⇒ (C ∼E) ⊑ (C ∼D);
(c) (C ∼D) = C ∼(C ∼(C ∼D));
(d) (D ⊑ (C ∼E) and D ⊑ E) ⇔ (D = C);
(e) ((C ∼D) ⊏ (C ∼E)) ⇔ (C ∼(C ∼E) ⊏ C ∼(C ∼D));
(f) (C ∼D = ⊤) ⇔ (D = C);
(g) C ∼⊤ = C and C ∼C = ⊤;
(h) (C ∼(D ⊓ E)) = C ∼((C ∼(C ∼D)) ⊓ (C ∼(C ∼E)));
(i) C ∼(C ∼(D ⊓ E)) = ((C ∼(C ∼D)) ⊓ (C ∼(C ∼E)));
(j) (C ∼(D ⊓ E)) = C ∼(C ∼((C ∼D) ⊔ (C ∼E))) and
(C ∼(D ⊔ E)) = (C ∼D) ⊓ (C ∼E);
(k) {(C ∼D) | C ⊑ D} is a Moore-family of the abstract interpretations of C,
containing C and such that ⊓_{i∈I}(C ∼D_{i}) = (C ∼(C ∼(⊓_{i∈I}(C ∼D_{i})))).

Proof. The proofs of these algebraic properties can be found in Frink [1962] and Grätzer [1978]. Varlet [1963] also contains a survey on the above standard algebraic properties of pseudocomplement. In particular, the proof of (a), (b), and (c) can be found in the proof of Glivenko’s Theorem [Grätzer 1978, Theorem 4, p. 49]. Their proof can also be found by observing that they correspond precisely to Eqs. (8), (9), and (11) in Frink [1962], respectively. The proof of (e), (g), (i), and (j) can be found in Frink [1962], corresponding to Eqs. (10), (15), (18), and (19), respectively. Part (d) is immediate by definition of pseudocomplement, while (f) is immediate from (a). Parts (h) and (k) can be derived as corollaries of Glivenko’s Theorem [Grätzer 1978, Theorem 4, p. 49]. Also, (h) corresponds precisely to Eq.

(17) in Frink [1962].

There exists a wide class of abstract domains for which we can always compute the complement (cf. Corollary 3.7). Indeed, the overwhelming majority of the abstract domains used as the basis of a static analysis satisfies the ascending chain condition

ACM Transactions on Programming Languages and Systems, Vol. 19, No. 1, January 1997.

(even most of them are finite domains). Furthermore, even if the abstract domain does not satisfy the ascending chain condition, meet-continuity can be checked for it. As a remarkable example, we show later in Section 6 that the abstract lattice of intervals of integer numbers introduced in Cousot and Cousot [1977] to analyze the values of an integer variable does not satisfy the ascending chain condition and is not distributive, but it is meet-continuous.

Example 3.12. Let us consider the typical example of the rule of signs [Cousot and Cousot 1977; 1979] given by the lattice C depicted below. The concrete domain is ℘(ZZ) (ordered with set-theoretic inclusion ⊆). The concretization and abstraction maps are the obvious ones.

[figure: •; •; •; •; •; ≤ 0; ⊤; ≥ 0; 0; ⊥]

It is easy to verify that all the possible abstractions of this domain, i.e., all the closures on C, are the following:

D_{1} = {⊤}, D_{2} = {⊤, ≥ 0}, D_{3} = {⊤, 0}, D_{4} = {⊤, ⊥}, D_{5} = {⊤, ≤ 0},
D_{6} = {⊤, ≥ 0, ⊥}, D_{7} = {⊤, ≥ 0, 0}, D_{8} = {⊤, 0, ⊥}, D_{9} = {⊤, ≤ 0, 0},
D_{10} = {⊤, ≤ 0, ⊥}, D_{11} = {⊤, ≥ 0, 0, ⊥}, D_{12} = {⊤, ≤ 0, ≥ 0, 0},
D_{13} = {⊤, ≤ 0, 0, ⊥}, D_{14} = D.

Since C is a finite lattice, by Corollary 3.7 uco(C) is a pseudocomplemented lattice. In fact, uco(C) is the lattice depicted below, and it is simple to verify the pseudocomplementation of uco(C) straight from its Hasse diagram.

[figure: •; •; •; •; •; •; •; •; •; •; •; •; •; •; D_{1}; D_{2}; D_{3}; D_{4}; D_{5}; D_{6}; D_{7}; D_{8}; D_{9}; D_{10}; D_{11}; D_{12}; D_{13}; D_{14}]

ACM Transactions on Programming Languages and Systems, Vol. 19, No. 1, January 1997.

Indeed, the pseudocomplements, i.e., the complements relative to C of the above abstractions, are as follows.

D_{1}^{∗} = D_{14}, D_{2}^{∗} = D_{10}, D_{3}^{∗} = D_{14}, D_{4}^{∗} = D_{12}, D_{5}^{∗} = D_{6}, D_{6}^{∗} = D_{5}, D_{7}^{∗} = D_{10},

D_{8}^{∗} = D_{12}, D_{9}^{∗} = D_{6}, D_{10}^{∗} = D_{2}, D_{11}^{∗} = D_{5}, D_{12}^{∗} = D_{4}, D_{13}^{∗} = D_{2}, D_{14}^{∗} = D_{1}.

This example shows how complementation can work for domain decomposition. Suppose C has been incrementally designed by reduced product of the domains D_{2} and D_{13}. The complement (D_{2} ⊓ D_{13}) ∼ D_{2} is just the domain corresponding to the closure D_{2}^{∗} = D_{10}. In this case, (D_{2} ⊓ D_{13})∼D_{2} is a strict abstraction of D_{13}. It is worth noting that we can safely substitute D_{13} by (D_{2} ⊓ D_{13}) ∼ D_{13}, getting a more concise representation of the product (see the figure below).

[figure: •; •; •; •; •; ≤ 0; ⊤; ≥ 0; 0; ⊥; C] ^{=} ^{• • ⊤ ≥ 0 D^{2}  ⊓ • • • • ⊤ ≤ 0 0 ⊥ D^{13}}  ^{=} ^{• • ⊤ ≥ 0 D^{2} ⊓  • • • ⊤ ≤ 0 ⊥ ((D^{2} ⊓ D^{13})∼D^{2})}

Domain decomposition by complementation will be considered later in Section 4.

3.1 Construction of Complements

In this section, we present a method to generate the complement C ∼D, when C is a finite set. We will build C ∼D as the saturation point of an increasing sequence of closure operators.

In the following, given a complete lattice ⟨C, ⪯⟩, and X ⊆ C, we will denote by maxs(X) the set of maximal elements of X, viz., the objects x ∈ X such that ∀y ∈ X. x ⪯ y ⇒ x = y, and by Cl(X) the greatest (w.r.t. ⊑) closure operator containing X. Observe that, if X, Y are (sets of fixpoints of) closure operators on C, then Cl(X ∪ Y) = X ⊓ Y = {x ∧ y | x ∈ X and y ∈ Y }, and that Cl(X) can be computed by adding to X all the greatest lower bounds of subsets of X.

Let {X_{n}}_{n∈IN} be the following family:

X_{0} = {⊤}
X_{1} = Cl(X_{0} ∪ maxs(C \ Cl(X_{0} ∪ D)))
⋮
X_{n} = Cl(X_{n−1} ∪ maxs(C \ Cl(X_{n−1} ∪ D)))
⋮

The following proposition shows some properties of X_{n}, for n ∈ IN.

Proposition 3.1.1. In the family {X_{n}}_{n∈IN} defined as above, we have that

(1) ∀n ∈ IN. X_{n} ∈ uco(C),

(2) ∀n ∈ IN. X_{n} ⊆ X_{n+1},

ACM Transactions on Programming Languages and Systems, Vol. 19, No. 1, January 1997.

(3) ∀n ∈ IN.∀Y ∈ uco(C). (Y ⊓ D = C ⇒ X_{n} ⊆ Y).

Proof. Points (1) and (2) are obvious by definition. Let us now prove (3), by induction with respect to n.

(n = 0). Obvious.

(n > 0). Assume Y ∈ uco(C) and Y ⊓ D = C. Let x ∈ X_{n}. Then there exists X ⊆ X_{n−1} ∪ maxs(C \ Cl(X_{n−1} ∪ D)) such that x = ∧X. Let X′ ⊆ X_{n−1}, X′′ ⊆ maxs(C \ Cl(X_{n−1} ∪ D)) such that X = X′ ∪ X′′. By inductive hypothesis, X′ ⊆ Y. It is therefore sufficient to show that X′′ ⊆ Y and then use the fact that Y is closed with respect to the operation of greatest lower bound. Consider z ∈ X′′. Since Y ⊓ D = C, there exist y ∈ Y, y′ ∈ D such that z = y ∧ y′. It turns out that y ∉ Cl(X_{n−1} ∪ D), as otherwise we would have z ∈ Cl(X_{n−1} ∪ D). Hence, y ⪯ z, since z is a maximal of the complement of the set Cl(X_{n−1} ∪ D). But from z = y ∧ y′, it follows also that z ⪯ y; hence z = y ∈ Y.

This concludes the proof.

If C is finite, then from the above proposition, we derive that the sequence {X_{n}}_{n∈IN} converges in a finite number of steps to the complement C ∼D.

Corollary 3.1.2. If C is finite, then there exists n̄ such that X_{n̄+1} = Xn̄ and Xn̄ = C ∼D.

Proof. From Proposition 3.1.1, point (2), we have that X_{n̄+1} = Xn̄ for some n̄ ≤ |C|. By definition of X_{n̄+1}, this implies that Cl(Xn̄∪D) = C, i.e., Xn̄⊓D = C. The rest follows from Proposition 3.1.1, points (1) and (3).

The above corollary constitutes a proof of Theorem 3.6, in the finite case. If C is infinite, then the construction can be extended so as to obtain a transfinite sequence, by defining X_{α} = Cl(X_{α−1} ∪ maxs(C \ Cl(X_{α−1} ∪ D))) for α successor ordinal, and X_{α} = Cl(⋃_{β<α} X_{β}), for α limit ordinal. It is possible to show that Xᾱ = C ∼D, where ᾱ is the smallest ordinal such that |ᾱ| > |C|. For the detailed (nonconstructive) proof of Theorem 3.6, however, we refer to Giacobazzi et al. [1996].

Example 3.1.3. Consider the domains C and D_{2} of Example 3.12. Let us compute the complement C ∼ D_{2} using the method described above. It is simple to verify that the sequence of all the X_{n} is as follows: X_{0} = {⊤}, X_{1} = {⊤, ≤ 0}, X_{2} = {⊤, ≤ 0, ⊥}, X_{3} = X_{2}. Thus, the construction of the X_{n} generates the complement in three steps.

4. COMPLEMENTS TO DECOMPOSE ABSTRACT DOMAINS

Often, abstract domains for analysis are incrementally designed using reduced product of simpler domains (e.g., in logic program analysis see Codish et al. [1995], Muthukumar and Hermenegildo [1991], and Sundararajan and Conery [1992]). This introduces modularity in domain design, which is helpful both to design domaindependent abstract operations and to simplify proofs of properties for complex domains for analysis. The inverse operation of domain decomposition does not exist in the standard theory of abstract interpretation. This would be clearly helpful to achieve modularity from domains which are not originally designed as reduced product.

ACM Transactions on Programming Languages and Systems, Vol. 19, No. 1, January 1997.

Definition 4.1. A (conjunctive) decomposition for a domain D is any tuple of domains ⟨D_{i}⟩_{i∈I} such that D = ⊓_{i∈I}D_{i}.

Obviously, with ⊓ being the greatest lower bound operation on domains, if ⟨D_{i}⟩_{i∈I} is a decomposition of D then each D_{i} is an abstraction of D. Moreover, notice that trivial decompositions always exist. In fact, for any domain D, ⟨D⟩ and the pair ⟨D, ⊤⟩ (and ⟨⊤, D⟩) are evidently (straightforward) decompositions of D.

Example 4.2. Consider Example 3.12. ⟨D_{1}, D_{2}⟩ and ⟨D_{1}, C ∼ D_{1}⟩ are both binary decompositions for C.

Clearly, the complement operation provides a systematic way to factorize a given domain into binary decompositions. This may be helpful to decompose domains that are not originally designed by products of more abstract domains. The case of the domain Sharing, designed by Jacobs and Langen [1989; 1992] for aliasing analysis of logic programs, is a typical case of a complex abstract domain for which no decomposition is known in the literature. This case will be discussed in Section 8.

It is well known (cf. Ward [1942]) that uco(C), for any complete lattice C, is dualatomistic. Recall that a complete lattice L is (dual-) atomistic if every element of L is the join (meet) of the (dual-)atoms in L preceding (following) it. A (dual-)atom is a nonbottom (top) element a ∈ L such that for any b ∈ L, ⊥ ≺ b ⪯ a ⇒ a = b (a ⪯ b ≺ ⊤ ⇒ a = b). Hence, each closure which is different from the top closure λx.⊤ is the infimum of the set of dual-atoms following it. It is therefore always possible to decompose any abstract domain in terms of a (possibly infinite) family of basic domains. If C is a complete lattice, we call basic domains those abstract domains which correspond to dual-atoms in uco(C). The dual-atoms in uco(C) are all and only those closures φ_{x}, for x ∈ C, with x ≠ ⊤, such that φ_{x}(C) = {x, ⊤} [Ward 1942], namely the functions

φ_{x}(y) = \{ \begin{matrix}x & if y ⪯_{C} x; \\ ⊤ & otherwise. \end{matrix}

Therefore, the basic abstract domains for a concrete domain C are all and only the two-element domains {⊤, x}, for x ∈ C \ {⊤}. This decomposition is straightforward, and corresponds, in most cases, to enumerating the elements of the domain.

Example 4.3. Consider the domain C of Example 3.12. Its basic abstract domains are those associated with the dual-atoms D_{2}, D_{3}, D_{4}, and D_{5}. However, it is immediate to verify that ⟨D_{2}, D_{4}, D_{5}⟩ is a decomposition for C as well, i.e., C = D_{2} ⊓ D_{4} ⊓ D_{5}, involving only three dual-atoms. The corresponding basic domains are the two-point lattices {⊤, ≥ 0}, {⊤, ≤ 0}, and {⊤, ⊥}, respectively.

The following definition introduces a natural preordering relation between decompositions of a given domain.

Definition 4.4. If ⟨D_{i}⟩_{i∈I} and ⟨D_{j}⟩_{j∈J} are decompositions of D, then ⟨D_{i}⟩_{i∈I} is space better than ⟨D_{j}⟩_{j∈J} if ∑_{i∈I} |D_{i}| ≤ ∑_{j∈J} |D_{j}|.

Thus, the above definition allows to compare decompositions with respect to their “space complexity.” This definition gives rise to space minimal decompositions, where a decomposition ⟨D_{i}⟩_{i∈I} for a domain D is space minimal if D has no decomposition strictly space better than ⟨D_{i}⟩_{i∈I}.

ACM Transactions on Programming Languages and Systems, Vol. 19, No. 1, January 1997.

On the other hand, it is possible to compare decompositions of fixed length in a pointwise manner, exploiting the order of precision between abstract domains.

Definition 4.5. If ⟨D_{i}⟩_{i∈I} and ⟨E_{i}⟩_{i∈I} are decompositions of D (of the same length), then ⟨D_{i}⟩_{i∈I} is better than ⟨E_{i}⟩_{i∈I} if ∀i ∈ I. E_{i} ⊑ D_{i}.

It is immediate to observe that this definition actually induces a partial ordering. However, least decompositions (w.r.t. this order) of a given fixed length in general do not exist. In fact, for any domain D, with |D| > 1, ⟨D, ⊤⟩ and ⟨⊤, D⟩ are uncomparable minimal binary decompositions of D. Moreover, as observed in Filé and Ranzato [1996], it is simple to verify that ⟨D_{i}⟩_{i∈I} is a minimal decomposition of D if for all k ∈ I, (D_{k} ⊏ E_{k}) ⇒ (C ⊏ (⊓_{i∈I\{k}}D_{i}) ⊓ E_{k}).

As the following straightforward lemma states, complementation naturally induces minimal decompositions.

Lemma 4.6 [Filé and Ranzato 1996]. ⟨D_{i}⟩_{i∈I} is a decomposition of D such that for any k ∈ I, D ∼(⊓_{i∈I\{k}}D_{i}) = D_{k} iff it is minimal.

In particular, note that if D ⊑ E then, using the above lemma and Proposition 3.11 part (c), ⟨D ∼ E, D ∼ (D ∼ E)⟩ always yields a minimal binary decomposition for D. The role played by complementation for the decompositions is particularly important whenever we deal with an abstract domain built by reduced product of simpler domains. Suppose that D = ⊓_{i∈I}D_{i} and |I| = n. Then, complementation allows to improve on the representation of D. In fact, for any k ∈ I,

⟨D_{1},…, D_{k−1}, D ∼(⊓_{i∈I\{k}}D_{i}), D_{k+1},…, D_{n}⟩  (∗)

is a decomposition both better and space better than the starting one ⟨D_{i}⟩_{i∈I}. Moreover, each one of these decompositions can be further improved by iterating this process, applying complementation to the other components, until a minimal decomposition is reached. In this case, we get a minimal decomposition if, by iterating this kind of application of the complementation, we get a domain decomposition where each component has been considered in at least one step of (∗). The following proposition proves the correctness of the algorithm in Figure 1. This algorithm is nondeterministic, since the function choose selects an arbitrary element from an input set.

Proposition 4.7. The algorithm in Figure 1 correctly computes a minimal decomposition for D.

Proof. It is immediate to observe that the algorithm terminates in n steps. Let I = {1, ..., n}, and assume that D = ⟨A_{1}, ..., A_{n}⟩ is the decomposition given as output by the algorithm. Note that for any i ∈ I, we have that A_{i} = D ∼ E_{i}, for a suitable domain E_{i}, since, for each component of the input decomposition, a step (∗) has been applied. Note also that, by construction, for any j ∈ I, D ∼ (⊓_{i∈I\{j}}D_{i}) ⊑ D ∼ E_{j}. By Lemma 4.6, it is enough to verify that for any k ∈ I, D ∼(⊓_{i∈I\{k}}D ∼E_{i}) = D ∼E_{k}. Obviously, for any i ∈ I, D_{i} ⊑ D ∼E_{i}. Then, with fixed k ∈ I, we have that ⊓_{i∈I\{k}}D_{i} ⊑ ⊓_{i∈I\{k}}D ∼E_{i}. Then, by Proposition 3.11 part (b), we get D ∼ (⊓_{i∈I\{k}}D ∼ E_{i}) ⊑ D ∼ (⊓_{i∈I\{k}}D_{i}) ⊑ D ∼ E_{k}. On the other hand, D ∼ E_{k} ⊑ D ∼ (⊓_{i∈I\{k}}D ∼ E_{i}) evidently holds, hence concluding the proof.

ACM Transactions on Programming Languages and Systems, Vol. 19, No. 1, January 1997.

Input: A decomposition for D as an array D of n domains. Output: A minimal decomposition for D in D.

begin J := {1, ..., n}; repeat

k := choose(J); J := J \ {k}; A := ⊤; for i := 1 to n do

if i ≠ k then A := A ⊓ D[i];

D[k] := D ∼A until J = ∅ end

Fig. 1. An algorithm for minimal decompositions.

For instance, if D = D_{1} ⊓ D_{2} ⊓ D_{3} then by calling E = D ∼(D_{1} ⊓ D_{2}),

⟨D ∼((D ∼(D_{1} ⊓ E)) ⊓ E), D ∼(D_{1} ⊓ E), E⟩

is a minimal decomposition both better and space better than ⟨D_{1}, D_{2}, D_{3}⟩. Clearly, if D = ⊓_{i∈I}D_{i} and |I| = n, then by this process we can get at most n! different minimal decompositions of D, all better and space better than the starting one. In the binary case, if we start from a decomposition ⟨D_{1}, D_{2}⟩ of D then we get the two minimal decompositions: ⟨D ∼D_{2}, D ∼(D ∼D_{2})⟩ and ⟨D ∼(D ∼D_{1}), D ∼D_{1}⟩.

5. COMPOSITIONAL VERIFICATION OF DOMAIN PROPERTIES

One of the advantages of abstract domain decompositions lies in checking properties of abstract domains compositionally, by checking them on domain factors. Instead of proving properties for general domains, one can prove properties for more abstract (and simple) factors, provided that these properties are preserved under composition, which is in our case reduced product.

In the following sections, we consider two examples of domain properties which are particularly important in abstract interpretation and which can be verified on the factors of domain decompositions. This may greatly simplify their test for complex domains.

5.1 Dual-Atomicity

Atomicity and dual-atomicity are important lattice-theoretic properties which can allow efficient domain implementation. The intuition behind atomicity in abstract domains is simple: atoms represent primitive properties for program analysis.^{1} (Dual-)atomistic domains can therefore be generated by considering only their (dual-)atoms. It turns out that dual-atomicity can be verified on the factors of domain decomposition. We need first some preliminary definitions. Given a complete lattice L, we say that two subsets A, B ⊆ L are not comparable in L if for any a ∈ A, b ∈ B, a ⪯̸ b and a ⪰̸ b. A closure operator (or equivalently an abstract

1This observation, in the context of program analysis, has been done first by Nielson [1985].

ACM Transactions on Programming Languages and Systems, Vol. 19, No. 1, January 1997.

domain) is (dual-)atomistic if the set of its fixpoints is a (dual-)atomistic lattice. We denote by DAtom(L) the set of dual-atoms of L.

Proposition 5.1.1. Let {ρ_{i}}_{i∈I} be a set of dual-atomistic closure operators on a complete lattice L, such that DAtom(ρ_{i}) and DAtom(ρ_{j}) are not comparable in L, for any i, j ∈ I with i ≠ j. If K ⊆ I then ⊓_{k∈K}ρ_{k} is dual-atomistic.

Proof. Trivial if K = ∅. Thus, assume that ∅ ≠ K ⊆ I. We observe first that any element x ∈ ⊓_{k∈K}ρ_{k} is such that there exists Y ⊆ ∪_{k∈K}DAtom(ρ_{k}) for which x = ∧Y. This is immediate because by definition of reduced product x = ∧_{k∈K}y_{k}, where, for any k ∈ K, y_{k} ∈ ρ_{k}. Therefore, because {ρ_{k}}_{k∈K} is a set of dual-atomistic closure operators, we have that for any k ∈ K, there exist Y_{k} ⊆ DAtom(ρ_{k}) such that y_{k} = ∧Y_{k}. Hence, x = ∧_{k∈K}(∧Y_{k}) for some Y_{k} ⊆ DAtom(ρ_{k}), and k ∈ K. Thus, in order to conclude, we have to prove that ∪_{k∈K}DAtom(ρ_{k}) = DAtom(⊓_{k∈K}ρ_{k}).

(⊆). Assume that x ∈ DAtom(ρ_{j}) for some j ∈ K, but x ∉ DAtom(⊓_{k∈K}ρ_{k}). By definition of dual-atom, there exists y ∈ ⊓_{k∈K}ρ_{k}, y ≠ ⊤, such that x ≺ y. Because any y ∈ ⊓_{k∈K}ρ_{k} can be generated as glb of elements in ∪_{k∈K}DAtom(ρ_{k}), then there exist k ∈ K and z ∈ DAtom(ρ_{k}) (with z ≠ ⊤), such that y ⪯ z. Clearly k ≠ j; otherwise x cannot be a dual-atom in ρ_{j}. Moreover, if k ≠ j then we also have a contradiction because, by hypothesis, DAtom(ρ_{k}) and DAtom(ρ_{j}) are not comparable sets, and therefore x ⊀ z.

(⊇). Assume that x ∈ DAtom(⊓_{k∈K}ρ_{k}), but x ∉ ∪_{k∈K}DAtom(ρ_{k}). Since x can be generated as glb of elements in ∪_{k∈K}DAtom(ρ_{k}), there exist k ∈ K and y ∈ DAtom(ρ_{k}) (with y ≠ ⊤), such that x ≺ y. For any k ∈ K, DAtom(ρ_{k}) ⊆ ⊓_{k∈K}ρ_{k}, and therefore y ∈ ⊓_{k∈K}ρ_{k}, which contradicts the fact that x was an atom.

This concludes the proof.

Let us now consider an example. Consider the domains for parity, sign, and ±1-interval analysis, respectively P arity, Sign, and Sign^{±1}, for data-flow analysis of integer variables, depicted below. In Sign^{±1}, which is a strict abstraction of the Cousot and Cousot [1976; 1977] lattice of intervals later considered in Section 6, ±1 represents the closed interval [−1, 1], while ≤ −1 and ≥ 1 represent the intervals (−∞, −1] and [1, +∞), respectively. In the abstract domain P arity, od, and ev represent the set of odd and even numbers, respectively. The concrete domain is ⟨℘(ZZ), ⊆⟩. By these identifications, the concretization and abstraction maps for these domains are the obvious ones.

[figure: ⊤; od; ev; ⊥; •; •; •; •; P arity; ⊤; +; −; ⊥; 0; •; •; •; •; •; Sign; ⊤; 1; −1; ⊥; ≤ −1; ≥ 1; ±1; •; •; •; •; •; •; •; Sign^{±1}]

[figure: •; •; •; •; •; •; •; •; •; •; •; •; •; •; •; ⟨⊥, ⊥⟩; ⟨−1, od⟩; ⟨1, od⟩; ⟨≤−1, ev⟩; ⟨≤−1, od⟩; ⟨±1, od⟩; ⟨≥1, od⟩; ⟨±1, ev⟩; ⟨≥1, ev⟩; ⟨≤−1, ⊤⟩; ⟨⊤, od⟩; ⟨±1, ⊤⟩; ⟨⊤, ev⟩; ⟨≥1, ⊤⟩; ⟨⊤, ⊤⟩]^{Fig. 2. Sign^{±1} ⊓ P arity.}

Sign^{±1} and P arity are dual-atomistic lattices, where both DAtom(Sign^{±1}) = {≤ −1, ±1, ≥ 1} and DAtom(P arity) = {od, ev} are not comparable in ℘(ZZ). Therefore, by Proposition 5.1.1, the reduced product Sign^{±1} ⊓ P arity depicted in Figure 2 is a dual-atomistic lattice. It is worth noting that the reduced product Sign^{±1} ⊓ P arity provides also a characterization for 0, which is ⟨±1, ev⟩. Because of dual-atomicity, any element in Sign^{±1} ⊓ P arity can be represented as a set of atoms in DAtom(Sign^{±1}) ∪ DAtom(P arity) = {≤ −1, ±1, ≥ 1, ev, od}. For example, ⟨+1, od⟩ can be equivalently represented by the dual-atoms {±1, ≥ 1}.

The condition in Proposition 5.1.1, specifying that dual-atoms of a conjunctive decomposition have to be uncomparable, is essential to maintain dual-atomicity by reduced product. Consider the domains Sign and P arity above. The domain Sign is different from that in Example 3.12, as it does not characterize possibly null or negative (positive) values. Note that while Sign is clearly both atomistic and dual-atomistic, the domain C in Example 3.12 is neither atomistic nor dual-atomistic. Note however that the sets of dual-atoms of Sign and P arity contain comparable elements in ℘(ZZ). In this case, DAtom(Sign) = {+, 0, −} and DAtom(P arity) = {ev, od}, and 0 is contained in ev. Indeed, the reduced product Sign ⊓ P arity, which is depicted in Figure 3, is not dual-atomistic, because ⟨0, ev⟩ cannot be constructed as meet of dual-atoms in DAtom(Sign ⊓ P arity) = {⟨−, ⊤⟩, ⟨⊤, od⟩, ⟨+, ⊤⟩, ⟨⊤, ev⟩}.

5.2 Domain Completeness

Traditionally, abstract interpretation is intended to create sound approximations of concrete semantics (cf. Cousot and Cousot [1977]). If C is a concrete domain, and

ACM Transactions on Programming Languages and Systems, Vol. 19, No. 1, January 1997.

[figure: •; •; •; •; •; •; •; •; •; •; •; ⟨⊥, ⊥⟩ = ⟨0, od⟩; ⟨−, od⟩; ⟨+, od⟩; ⟨−, ev⟩; ⟨+, ev⟩; ⟨0, ev⟩; = ⟨0, ⊤⟩; ⟨−, ⊤⟩; ⟨⊤, od⟩; ⟨+, ⊤⟩; ⟨⊤, ev⟩; ⟨⊤, ⊤⟩]^{Fig. 3. Sign ⊓ P arity.}

T_{P} : C → C is a monotone semantic operation for a program P, then the soundness criterion for an abstraction given by a G.i. (γ, D, C, α), and an abstract semantic operator T_{P}^{♯} : D → D, is α ∘ T_{P} ⪯_{D} T_{P}^{♯} ∘ α. This ensures that the least-fixpoint abstract semantics lfp(T_{P}^{♯}) approximates lfp(T_{P}), i.e., α(lfp(T_{P})) ⪯_{D} lfp(T_{P}^{♯}) (cf. Cousot and Cousot [1977]). Completeness is the dual relation T_{P}^{♯} ∘ α ⪯_{D} α ∘ T_{P}. Because soundness is required in most abstract interpretations, in the following we abuse terminology and say that (γ, D, C, α) and T_{P}^{♯} are complete w.r.t. T_{P} if α ∘ T_{P} = T_{P}^{♯} ∘ α.

Completeness is recurrent in the relations between (concrete) semantics of programming languages at different levels of abstraction (cf. Comini and Levi [1994], Cousot and Cousot [1992b], and Giacobazzi [1996]). In the context of program analysis, it has been studied by Cousot and Cousot [1977], Mycroft [1993], and Cortesi et al. [1996]. This condition ensures that α(lfp(T_{P})) = lfp(T_{P}^{♯}). Hence, in analysis, complete abstract interpretations represent, in a sense, an ideal situation, where no loss of precision is introduced in the analysis by using abstract operations.

Completeness can be made a property of domains, by making this notion independent on the choice for T_{P}^{♯}. It is well known [Cousot and Cousot 1977; 1979] that, given a concrete semantic operation T_{P}, any G.i. naturally defines an abstract semantic operation for T_{P}, which is its best correct approximation in D, viz., α ∘ T_{P} ∘ γ. Hence, because γ is always a 1-1 function in a G.i., and by the correspondence between G.i.’s and closure operators (see Section 2.3), we can define a notion of completeness for closure operators relatively to any monotonic function as follows.

Definition 5.2.1. Let C be a complete lattice and f : C → C be a monotone function. Then, ρ ∈ uco(C) is complete w.r.t. f if ρ ∘ f = ρ ∘ f ∘ ρ.

ACM Transactions on Programming Languages and Systems, Vol. 19, No. 1, January 1997.

Example 5.2.2. The lattice C in Example 3.12 for sign analysis is complete with respect to integer multiplication. This proves that the rule of sign is complete (see Mycroft [1993]).

Completeness can be verified compositionally, by verifying it on the factors of a domain decomposition. Let C be a complete lattice, and let f : C → C be a monotone function. Define Γ(f) = {ρ ∈ uco(C) | ρ ∘ f = ρ ∘ f ∘ ρ} as the set of complete domains w.r.t. f.

Proposition 5.2.3. If {ρ_{i}}_{i∈I} ⊆ Γ(f) then ⊓_{i∈I}ρ_{i} ∈ Γ(f).

Proof. Let {ρ_{i}}_{i∈I} ⊆ Γ(f). Then, by definition, for any i ∈ I we have ρ_{i} ∘ f = ρ_{i} ∘ f ∘ ρ_{i}. Let x ∈ C. Clearly, by extensivity of closure operators, ∧_{i∈I}ρ_{i}(f(x)) ⪯_{C} ∧_{i∈I}ρ_{i}(f(∧_{i∈I}ρ_{i}(x))). Moreover, by monotonicity we have ∧_{i∈I}ρ_{i}(f(∧_{i∈I}ρ_{i}(x))) ⪯_{C} ∧_{i∈I}ρ_{i}(f(ρ_{i}(x))). By completeness, we have ∧_{i∈I}ρ_{i}(f(ρ_{i}(x))) = ∧_{i∈I}ρ_{i}(f(x)). Hence, ∧_{i∈I}ρ_{i}(f(x)) = ∧_{i∈I}ρ_{i}(f(∧_{i∈I}ρ_{i}(x))), which concludes the proof.

Clearly, both the straightforward abstractions given by the identity closure C and the top closure {⊤_{C}} are complete. Hence, Γ(f) ∈ uco(uco(C)).

6. IMPERATIVE PROGRAMMING: DECOMPOSING INTEGER INTERVAL DOMAIN

In this section, we apply complementation to some abstractions of the standard lattice of integer intervals, introduced by Cousot and Cousot [1976; 1977] as an abstract domain for data-flow analysis of (imperative) programs with variables assuming integer values. The lattice of integer intervals is particularly important because it provides a typical example of abstract domain for analysis which is meet-continuous, but it is neither distributive nor does it satisfy the ascending chain condition.

6.1 Domains for Integer Variable Analysis

For simplicity, we consider a single integer variable to analyze (the generalization is straightforward), and therefore the domain of concrete denotations is the powerset of the integers, ℘(ZZ), ordered by subset inclusion.

The abstract domain I of integer intervals is defined as follows:

\begin{aligned}I & = & \{[a, b] | a, b ∈ ZZ, a ≤ b\} ∪ \{(−∞, b] | b ∈ ZZ\}∪ \\ & & \{[a, +∞) | a ∈ ZZ\} ∪ \{(−∞, +∞)\} ∪ \{⊥\}, \end{aligned}

where the ordering ≤ on ZZ is the natural ordering on the integer numbers. The ordering relation ≤_{I} on intervals is defined as follows:

—for any x ∈ I, ⊥ ≤_{I} x ≤_{I} (−∞, +∞), —for any a, b, c, d ∈ ZZ, [a, b] ≤_{I} [c, d] ⇔ c ≤ a & b ≤ d, —for any b, d ∈ ZZ, (−∞, b] ≤_{I} (−∞, d] ⇔ b ≤ d, —for any a, b, d ∈ ZZ, [a, b] ≤_{I} (−∞, d] ⇔ b ≤ d, —for any a, c ∈ ZZ, [a, +∞) ≤_{I} [c, +∞) ⇔ c ≤ a, —for any a, b, c ∈ ZZ, [a, b] ≤_{I} [c, +∞) ⇔ c ≤ a.

This domain I is depicted in Figure 4. Notice that the top element in I is the interval (−∞, +∞). As pointed out in Cousot and Cousot [1977], it turns out that ⟨I, ≤_{I}⟩ is a complete lattice.

ACM Transactions on Programming Languages and Systems, Vol. 19, No. 1, January 1997.

[figure: •; •; •; •; •; •; •; •; •; •; •; •; •; •; •; •; •; •; •; •; •; •; •; ⊥; [-2,-2]; [-1,-1]; [0,0]; [1,1]; [2,2]; [-2,-1]; [-1,0]; [0,1]; [1,2]; (-∞,-2]; [-2,0]; [-1,1]; [0,2]; [2,+∞); (-∞,-1]; [-2,1]; [-1,2]; [1,+∞); (-∞,0]; [-2,2]; [0,+∞); (-∞,+∞); ⋯; ⋯; ⋯; ⋯; ...; ...; ...; ...; ...; ...; ...; ...; ...; ...; ...; ⋮; ...; ...; ...; ...; ...; ...; ...; ...; ...; ...; ...]

Fig. 4. The abstract domain I.

I enjoys a Galois insertion with ⟨℘(ZZ), ⊆⟩, which is determined by the following mappings:

α_{I}(S) = \{ \begin{matrix}⊥ & if S = ∅ \\ [a, b] & if min(S) = a and max(S) = b \\ (−∞, b] & if ∄min(S) and max(S) = b \\ [a, +∞) & if min(S) = a and ∄max(S) \\ (−∞, +∞) & if ∄min(S) and ∄max(S); \end{matrix}

γ_{I}(x) = \{ \begin{matrix}∅ & if x = ⊥ \\ \{z ∈ ZZ | a ≤ z ≤ b\} & if x = [a, b] \\ \{z ∈ ZZ | z ≤ b\} & if x = (−∞, b] \\ \{z ∈ ZZ | a ≤ z\} & if x = [a, +∞) \\ ZZ & if x = (−∞, +∞). \end{matrix}

Cousot and Cousot [1977] introduced some abstractions of the domain of the intervals. We recall these domains in Figure 5.

An abstraction of the intervals I is given by the domain I_{CS} depicted in Figure 5. This domain is obtained by identifying any integer number z by the interval [z, z], the elements − and + by (-∞,0] and [0,+∞), respectively, and the element ⊤ by (-∞,+∞). It is clear that I_{CS} is an abstraction of I, since it corresponds to a Moorefamily of elements of I. I_{CS} is an appropriate domain for constant propagation and sign analysis.

ACM Transactions on Programming Languages and Systems, Vol. 19, No. 1, January 1997.

[figure: •; •; •; •; •; •; •; •; •; •; •; ⊥; -3; -2; -1; 0; 1; 2; 3; −; +; ⊤; ⋯; ⋯; ⋯; ⋯; ⋯; ⋯; •; •; •; •; •; •; •; •; •; ⊥; -3; -2; -1; 0; 1; 2; 3; ⊤; ⋯; ⋯; ⋯; ⋯; ⋯; ⋯; •; •; •; •; •; ⊥; 0; −; +; ⊤]

Fig. 5. The abstract domains I_{CS}, I_{C}, and I_{S}.

A further abstraction of I_{CS}, and hence of I, is given by the domain I_{C} also depicted in Figure 5. I_{C} is clearly a Moore-family of elements of I_{CS} and therefore an abstraction of I_{CS}.

Finally, a third abstraction of I_{CS}, incomparable with I_{C}, is the domain I_{S} also given in Figure 5. Also in this case, I_{S} is obviously a Moore-family of I_{CS} and hence an abstraction of it.

The domain I_{C} is the standard lattice for constant propagation analysis [Kam and Ullman 1977; Kildall 1973], namely used to detect program expressions computing the same value on all executions of the program, while I_{S} is used for sign analysis [Cousot and Cousot 1977]. I_{CS} is an enrichment of both I_{C} and I_{S}. Indeed, it is immediate to observe that I_{CS} is exactly the reduced product of I_{C} and I_{S}.

Lemma 6.1.1. I_{CS} = I_{C} ⊓ I_{S}.

6.2 The Complements

Evidently, the lattice of intervals I does not satisfy the ascending chain condition. Moreover I is not distributive; in fact, (A ∨ B) ∧ C differs from (A ∧ C) ∨ (B ∧ C), with A = [−1, −1], B = [−1, 0], and C = [1, 1]. Nevertheless, complementation is equally possible, since a simple direct inspection of the Hasse diagram of I reveals that I is meet-continuous, and hence Theorem 3.6 is applicable. Thus, we can compute the three complements I ∼I_{CS}, I ∼I_{C}, and I ∼I_{S}. First, we will compute I ∼I_{C} and I ∼I_{S}, and then I ∼I_{CS} will be a simple consequence of these two.

The complement of constant propagation relative to intervals is somehow surprising; in fact, it turns out that this complement is precisely the lattice of intervals itself.

Proposition 6.2.1. I ∼I_{C} = I.

Proof. Trivially, I_{C} ⊓ I = I. I ∼ I_{C} must contain the top (-∞,+∞). Also, every proper interval (namely, each interval x such that |γ_{I}(x)| > 1) must belong to I ∼ I_{C}, since the closure on I associated with the abstraction of I_{C} maps each of them into ⊤. Consequently, I ∼I_{C} contains clearly ⊥ and each [z, z], for z ∈ ZZ, since every [z, z] is the meet of two proper intervals (viz., [z, z] = [z−1, z]∧[z, z+1]). Thus, we conclude that I ∼I_{C} = I.

The complement of the sign domain I_{S} relative to the interval domain I is given

ACM Transactions on Programming Languages and Systems, Vol. 19, No. 1, January 1997.

[figure: •; •; •; •; •; •; •; •; •; •; •; •; •; •; •; •; •; •; ⊥; [-2,-2]; [-1,-1]; [1,1]; [2,2]; [-2,-1]; [1,2]; (-∞,-2]; [-1,1]; [2,+∞); (-∞,-1]; (-∞,1]; [-2,1]; [-1,2]; [-2,2]; [1,+∞); [-1,+∞); (-∞,+∞); ⋯; ⋯; ⋯; ⋯; ...; ...; ...; ...; ...; ...; ...; ...; ...; ...; ⋮; ...; ...; ...; ...; ...; ...; ...; ...; ...; ...]

Fig. 6. The complement I ∼I_{S}.

by the Hasse diagram of Figure 6. Thus, the elements of this complement are exactly given by

I ∼I_{S} = I \ ({[z, 0] ∈ I | z ∈ ZZ} ∪ {[0, z] ∈ I | z ∈ ZZ} ∪ {(−∞, 0], [0, +∞)}).

Hence, this domain I ∼ I_{S} is not able to represent those intervals having 0 as an extreme. In this sense, I ∼I_{S} captures interval information but not sign.

Proposition 6.2.2. I ∼I_{S} is the domain depicted in Figure 6.

Proof. First of all, note that the domain of Figure 6, let us call it D, is indeed an abstraction of I, being closed by glb. Also, I_{S} ⊓ D = I: in fact, it is enough to observe that each element [z, 0], for -∞ < z ≤-1, can be obtained by reduced product as [z, 0] = (-∞, 0] ∧ [z, 1] (analogously for each [0, z], for 1 ≤ z < +∞). Finally, D is actually the complement I ∼ I_{S}. This follows because each element of D must belong to I ∼ I_{S}; otherwise there is no way to recover it by reduced product.

Finally, we compute the complement of the domain I_{CS} relative to the interval lattice I. It turns out that this complement is precisely the above-computed I ∼I_{S}, which is depicted in Figure 6.

Proposition 6.2.3. I ∼I_{CS} = I ∼I_{S}.

Proof. By Lemma 6.1.1, we know that I_{CS} = I_{C} ⊓ I_{S}. Then, exploiting Propo-

ACM Transactions on Programming Languages and Systems, Vol. 19, No. 1, January 1997.

sition 3.11 parts (e) and (j) and Proposition 6.2.1, we get the following equalities:

I ∼I_{CS} = I ∼(I_{C} ⊓ I_{S})
= I ∼(I ∼((I ∼I_{C}) ⊔ (I ∼I_{S})))
= I ∼(I ∼(I ⊔ (I ∼I_{S})))
= I ∼(I ∼(I ∼(I ∼I_{S})))
= I ∼I_{S}.

This concludes the proof.

7. FUNCTIONAL PROGRAMMING: DECOMPOSING COMPORTMENTS

In this application, we consider complements relative to the lattice of comportment analysis, designed by Cousot and Cousot [1994] in order to generalize Mycroft’s strictness and termination analysis [Mycroft 1980; 1981], Wadler and Hughes’ projection analysis [Wadler and Hughes 1987], and Hunt’s PER analysis [Hunt 1990]. This provides a decomposition of the lattice of comportments into sensible factors, which gives a better comprehension of its structure.

The comportment analysis applies to higher-order monomorphically typed lazy functional programming languages. To illustrate Cousot and Cousot’s comportment analysis, we consider abstract interpretation of a simply typed lambda calculus with basic types β. Denote D^{τ} the domain of values of a type τ, and by ⊥ its bottom element. For simplicity, we consider abstractions of functional basic types β → β (i.e., elements in D^{β→β} = D^{β} → D^{β}, the lattice of total continuous functions from D^{β} to D^{β} ordered pointwise). The following abstract domain B_{C} represents the lattice of basic comportment analysis, ordered with respect to the approximation order, for function basic types β → β.

[figure: •; •; •; •; tot; top; str; ide; •; •; •; ∅; div; con]

Basic comportments B_{C}

The meaning of basic comportments in B_{C} is given in Table I, in terms of a concretization function γ^{β→β} mapping basic comportments into ℘(D^{β→β}), the concrete domain of the standard collecting semantics.

It is easy to verify that both the standard Mycroft strictness S and termination T analyses are actually abstract interpretations of B_{C}, yielding the following simpler domains, respectively:

• • •div str top

Strictness S

• • •con tot top

Termination T

ACM Transactions on Programming Languages and Systems, Vol. 19, No. 1, January 1997.

Table I. Basic Comportment Analysis B_{C}

truth  γ^{β→β}(top) = D^{β→β}
strictness  γ^{β→β}(str) = {f | f(⊥) = ⊥}
totality  γ^{β→β}(tot) = {f | ∀x ∈ D^{β} \ {⊥}. f(x) ≠ ⊥}
identity  γ^{β→β}(ide) = {f | ∀x ∈ D^{β}. f(x) = ⊥ ⇔ x = ⊥}
divergence γ^{β→β}(div) = {f | ∀x ∈ D^{β}. f(x) = ⊥}
convergence γ^{β→β}(con) = {f | ∀x ∈ D^{β}. f(x) ≠ ⊥}
falsity  γ^{β→β}(∅) = ∅

By an inspection of the lattice of basic comportments B_{C}, we notice that the complement of the strictness (termination) domain relative to B_{C} is the termination (strictness) analysis.

Proposition 7.1. B_{C} ∼S = T and B_{C} ∼T = S

Proof. Note that B_{C} is a finite lattice. Hence, by the iterative method in Section 3.1 applied to B_{C} ∼S, we get X_{0} = {top}, X_{1} = {top, tot}, and X_{2} = X_{3} = {top, tot, con} = T . The proof for B_{C} ∼T is analogous.

Hence, by Lemma 4.6, ⟨S, T ⟩ is a minimal decomposition for the lattice of basic comportments. In particular, the identity information ide as well as ∅ can be both constructed by conjunction of strictness and termination values (str and tot for ide and div and con for ∅). Therefore, the lattice of basic comportments B_{C} is precisely the reduced product of strictness and termination. As we will show later on, in this example the identity information will be always definable as the conjunction of factors involving strictness information (i.e., in factorizations of analysis involving strictness, such as strictness or projection analysis), even though the lattice of comportments will be lifted at a powerset level.

As proved by Cousot and Cousot [1994], more precise comportment properties for higher-order functional languages can be characterized by lifting the domain of basic comportments to its disjunctive completion. Disjunctive completion is here used to mimic the collecting semantics construction. Collecting semantics are defined by “collecting” in sets the possible output values corresponding to a given set of possible input values, as defined by the standard semantics of the language. Hence, in order to exploit sets of values, Cousot and Cousot considered a powerset completion of the abstract domain, which corresponds, at the level of abstract domains, to the collecting semantics construction. The abstraction of sets of functions in D^{β→β} yields a corresponding abstract domain for comportments which can be systematically derived by reduction of a powerset completion of the lattice of basic comportments B_{C}. In this case, the meaning of sets Ψ of basic comportments is given by a concretization function γ^{℘} such that γ^{℘}(Ψ) = ∪{γ^{β→β}(ψ) | ψ ∈ Ψ}. The following lattice C, ordered by the approximation order, corresponds precisely to this (disjunctive) comportment analysis. It is obtained by (e.g., antichain) powerset completion and reduction (viz., sets of basic comportments denoting the same object in ℘(D^{β→β}) are identified). The new element abs corresponds here to the set of basic comportments {con, div} and represents absence.

[figure: ∅; {con}; {div}; {ide, div}; {str}; {top}; abs; {ide}; {tot}; {tot, div}; •; •; •; •; •; •; •; •; •; •]

Comportments C

As shown in Cousot and Cousot [1994], this lattice generalizes projection P and dual-projection D_{P} depicted respectively below, as well as the above strictness S and termination T analyses (in the latter case, the concretization in C of an element x is the singleton {x}).

[figure: {div}; {str}; {top}; abs; ∅; •; •; •; •; •]

Projection P

[figure: ∅; {con}; {div}; {top}; {tot}; •; •; •; •; •]

Dual-projection D_{P}

Some interesting properties of comportment analysis can be studied by looking at the complements of projection, dual-projection, strictness, and termination in C.

Proposition 7.2.

(1 ) C ∼P = {{top}, {tot, div}, {tot}}, (2 ) C ∼S = {{top}, {tot, div}, {tot}, abs, {con}}, and (3 ) C ∼T = C ∼D_{P} = {{top}, {tot, div}, {str}, abs, {ide, div}, {div}}.

Proof. We only include the proof for

C ∼T = C ∼D_{P} = {{top}, {tot, div}, {str}, abs, {ide, div}, {div}}

since the other proofs are similar. Because C is a finite domain, by applying the iterative method in Section 3.1, we obtain

—X_{0} = {{top}}, —X_{1} = {{top}, {tot, div}, {str}, {ide, div}}, and —X_{2} = X_{3} = {{top}, {tot, div}, {str}, {ide, div}, abs, {div}}.

ACM Transactions on Programming Languages and Systems, Vol. 19, No. 1, January 1997.

The equality C ∼ T = C ∼ D_{P} is a consequence of the fact that {div} is always obtained by combining the maximal elements abs and {ide, div} which are both neither included in T , nor in D_{P}.

The complements C ∼P, C ∼S, and C ∼T are depicted below.

[figure: \begin{matrix}\{tot, div\} & \{top\} & \{tot\} & • & • & • \\ C ∼P \end{matrix}; \{tot, div\}; \{tot\}; \{top\}; abs; \{con\}; •; •; •; •; •; C ∼S; \{div\}; abs; \{ide, div\}; \{top\}; \{tot, div\}; \{str\}; •; •; •; •; •; •; C ∼T = C ∼D_{P}]

Note that C ∼P characterizes possible divergence in total functions. This domain factorizes C, where in particular the (disjunctive) identity information, i.e., {ide} and {ide, div}, as well as the convergence {con} can be reconstructed by reduced product involving C ∼ P and P. The identity and convergence information is therefore redundant for the decomposition ⟨P, C ∼P⟩. C ∼S is a domain for totality analysis. This domain characterizes precisely the nonstrictness comportments. It is worth noting that also in this case the identity information, as well as ∅, can be reconstructed by composing C ∼ S with strictness, and it is therefore redundant. As observed in Proposition 7.2, C ∼ T = C ∼ D_{P}. This domain characterizes exactly the nonterminating (or divergent) comportments. Note that both ⟨P, C ∼ P⟩ and ⟨S, C ∼ S⟩ provide binary decompositions of the lattice of comportments, which are strictly space better than ⟨T , C ∼T ⟩. A domain for nonterminating and nonstrictness comportments can be further obtained as the complement of strictness relative to C ∼T , or equivalently as the complement of termination relative to C ∼S, i.e., (C ∼ S) ∼ T = (C ∼ T ) ∼ S = (C ∼ D_{P}) ∼ S, as depicted below. We omit the proofs for this complement, since it is similar to that in Proposition 7.2.

{tot, div} {top} abs • • •
(C ∼S)∼T = (C ∼T )∼S = (C ∼D_{P})∼S

Note that ⟨S, T , (C ∼S)∼T ⟩ is a decomposition for the lattice of comportments C. Hence, by iterating complementation of these factors, by Proposition 4.7, we get the following minimal decomposition for C.

Proposition 7.3. ⟨{{top}, {str}}, {{top}, {tot}}, {{top}, {tot, div}, abs}⟩ is a minimal decomposition for C.

ACM Transactions on Programming Languages and Systems, Vol. 19, No. 1, January 1997.

Proof. We iterate the application of complementation, as suggested in Proposition 4.7, to the input decomposition ⟨S, T , (C ∼ S) ∼ T ⟩. It is worth noting that ((C ∼ S) ∼ T ) ⊓ T = (C ∼ S), and because (C ∼ S) ∼ T = (C ∼ T ) ∼ S, then ((C ∼S)∼T ) ⊓ S = (C ∼T ). Moreover, by Proposition 7.1, S ⊓ T = B_{C}. Hence, by applying the iterative method in Section 3.1, we get

C ∼(C ∼S). X_{0} = {{top}}, X_{1} = {{top}, {str}}, which is a fixpoint;
C ∼(C ∼T ). X_{0} = {{top}}, X_{1} = {{top}, {tot}}, which is a fixpoint;
C ∼B_{C}.  X_{0} = {{top}}, X_{1} = {{top}, {tot, div}}, X_{2} = {{top}, {tot, div}, abs}
which is a fixpoint. Hence, C ∼B_{C} = (C ∼S)∼T .

The proof follows by Proposition 4.7.

Therefore, the whole domain of comportments C can be represented, more concisely, by the following decomposition:

⟨{{top}, {str}}, {{top}, {tot}}, {{top}, {tot, div}, abs}⟩

which is just a tuple of chains, corresponding to the data structure below.

[figure: •; •; •; •; •; abs; {tot, div}; {str}; {tot}; {top}]

The above decomposition shows the logical relation between comportment and strictness and termination analysis in abstract interpretation of functional languages. The following diagram summarizes the relation (in uco(C)) between some of the complements obtained above, involving strictness and termination only.

[figure: •; C; •; B_{C}; •; C ∼S; •; C ∼T; •; (C ∼S)∼T; •; T; •; S; •; C ∼(C ∼S); •; C ∼(C ∼T )]

As far as dual-projection is concerned, we have shown that the comportment analysis cannot be obtained as the reduced product of projection and dual-projection, because the elements {tot, div} and {ide, div} cannot be reconstructed. Indeed, C ∼P is not comparable (as abstract interpretation) with D_{P}. However, note that C = P ⊓ D_{P} ⊓ (C ∼ P) may provide an alternative decomposition of the domain of comportments. Finally, the factorization of the domain of basic comportments into

ACM Transactions on Programming Languages and Systems, Vol. 19, No. 1, January 1997.

the pair ⟨S, T ⟩ proves that the domain of comportments is indeed (isomorphic to) the space of all relations between strictness and termination (at least for the case of the functional basic types). This clarifies the relationship between the domain of comportments and the domains for termination and strictness analysis.

8. LOGIC PROGRAMMING: A DECOMPOSITION FOR SHARING

In this section, we apply complementation to the case of Sharing, a well-known domain for variable aliasing and groundness analysis of logic programs introduced by Jacobs and Langen [1989; 1992]. In Cortesi et al. [1992], it has been shown that Sharing represents, in addition to variable sharing, ground dependency. We prove that Sharing enjoys a Galois insertion (not only a Galois connection as proved in Cortesi et al. [1992]) with the domain Def [Marriott and Søndergaard 1993]. Further, we investigate what is left of Sharing once we remove Def , i.e., the complement of Def with respect to Sharing. This domain, on the one hand, must represent variable independency and sharing and, on the other hand, must disregard ground dependency. We show that such a domain is characterized by a simple closure operator on Sharing.

8.1 Notation on Substitutions

Let Var be a countable set of variables x, y, z,…, and let A be an alphabet of constant and function symbols. A substitution σ on (A, Var) is a function mapping each x ∈ Var to a term σ(x) built on the variables of Var and on the symbols of A, and such that σ(x) ≠ x holds only for a finite number of variables x. We denote a substitution by the list of its nontrivial bindings, i.e., σ = {x/σ(x) | σ(x) ≠ x}. Given a term t, we denote by var(t) the set of variables which occur in t. Given two substitutions σ and θ, the composition θ∘σ is defined as the substitution which maps each x into θ(σ(x)), where θ(t) is the term obtained from t by replacing each y ∈ var(t) by θ(y). A substitution σ is idempotent if σ ∘ σ = σ. We denote by Subst the set of idempotent substitutions. It is possible to define the relation ≤ of instantiation on Subst (actually a preorder) in the usual way: if σ, θ ∈ Subst then σ ≤ θ iff there exists a substitution δ (possibly nonidempotent) such that σ = δ ∘ θ. In this case, we say that σ is an instance of θ. The set of all instances of σ is denoted by Δ_{σ}. The concrete domain of computation of a logic program is the set ℘(Subst) ordered by set inclusion. In the following, we illustrate the domains Sharing and Def as abstractions of ℘(Subst) with respect to a given finite set of variables of interest VI ⊆ Var.

8.2 The Domain Sharing

The abstract domain Sharing is defined as the set

{S ⊆ ℘(VI ) | S ≠ ∅ ⇒ ∅ ∈ S}

ordered with respect to set inclusion. For instance, if VI = {x, y}, then Sharing is the domain illustrated in Figure 7.

Jacobs and Langen [1989; 1992] proved that Sharing enjoys a Galois insertion into the concrete domain ℘(Subst). We recall briefly the construction of the mappings. For x ∈ Var and σ ∈ Subst, let share(σ, x) be the set of variables of interest whose images under σ contain the variable x, i.e., share(σ, x) = {y ∈ VI | x ∈ var(σ(y))}.

ACM Transactions on Programming Languages and Systems, Vol. 19, No. 1, January 1997.

[figure: {∅, {x}, {y}, {x, y}}; {∅, {y}, {x, y}}; {∅, {x}, {y}}; {∅, {x}, {x, y}}; {∅, {y}}; {∅, {x, y}}; {∅, {x}}; {∅}; ∅; true; x → y; y → x; y; x ↔ y; x; x ∧ y; false]

Fig. 7. The domains Sharing and Def for VI ={x, y}.

The abstraction and concretization functions between ℘(Subst) and Sharing are then defined as follows. For Σ ∈ ℘(Subst) and S ∈ Sharing

α_{Sharing}(Σ) = {share(σ, x) | σ ∈ Σ, x ∈ Var},
γ_{Sharing}(S) = {σ ∈ Subst | α_{Sharing}({σ}) ⊆ S}.

Intuitively, α_{Sharing} extracts the sharing information from substitutions, i.e., for a substitution σ, we have that y_{1}, y_{2},… share under σ (i.e., their images under σ share a variable) iff there exists A ∈ α_{Sharing}({σ}) such that y_{1}, y_{2},… ∈ A. As a particular case, we obtain also the ground information: y is ground in σ (i.e., its image under σ is a ground term) iff for every A ∈ α_{Sharing}({σ}), y ∉ A.

For example, let VI = {x, y, z, w}, and consider the set {∅, {w}, {y, z, w}} ∈ Sharing. This set represents the substitutions under which x is ground and y, z, and w may share. In particular, σ_{1} = {x/a, y/b, z/c} and σ_{2} = {x/b, y/v, z/v, w/v} (where a, b, c are constant symbols and where v is a variable) satisfy these properties. Therefore, {σ_{1}, σ_{2}} ⊆ γ_{Sharing}({∅, {w}, {y, z, w}}).

8.3 The Domain Def

The domain Def was introduced by Marriott and Søndergaard [1993] to analyze the ground dependencies induced by substitutions on a given set of variables of interest VI . We recall briefly its construction.

Assume that VI = {x_{1},…, x_{n}}. Given the Boolean domain B = {true, false}, we say that the Boolean function f : B^{n} → B is positive iff f(true,…, true) = true. Given an interpretation m : VI → B, and an n-ary boolean function f, we say that m is a model of f (notation m ⊧ f) iff f(m(x_{1}),…, m(x_{n})) = true. By Models(f) we denote the set of models of a given f. We also say that f validates f′ (notation f ⊧ f′) iff all the models of f are models also of f′. Given two interpretations m_{1}, m_{2}, the conjunction m_{1} ∧ m_{2} is the pointwise extension of the logical conjunction, i.e., ∀x. (m_{1} ∧ m_{2})(x) = m_{1}(x) ∧ m_{2}(x). We will represent an interpretation also as a set a variables, i.e., the set of elements of VI which are mapped into true. For instance, {x, y} represents the interpretation which assigns true to x and y and false to all the other variables of VI . Clearly, in this representation conjunction corresponds to set intersection.

ACM Transactions on Programming Languages and Systems, Vol. 19, No. 1, January 1997.

The domain Def consists of all positive n-ary Boolean functions whose models are closed under model conjunction, plus the bottom element false (the constant function which always returns false), ordered by ⊧.

Obviously, n-ary Boolean functions can be represented by means of propositional formulae on VI .^{2} It is possible to show that each formula of Def is equivalent to false or to a conjunction of definite (propositional) clauses. It turns out that Def is a (finite) lattice (e.g., Armstrong et al. [1994]), where the glb is simply logical conjunction, while the lub is f_{1} ∨_{Def} f_{2} = ∧{f ∈ Def | f_{1} ⊧ f and f_{2} ⊧ f}. For VI = {x, y}, Def is depicted in Figure 7.

We now recall the Galois insertion of Def into ℘(Subst). For σ ∈ Subst the formula that expresses the ground dependencies of σ is

gdep(σ) = ∃\overline{V I}. ∧ \{x ↔ ∧var(σ(x)) | σ(x) ≠ x\}

where ∃\overline{VI} is the existential quantification over the variables of noninterest, i.e., the variables in V ar \ VI . The interpretation which specifies which variables in VI are bound by σ to ground terms, and which are not, is

ground(σ) = {x ∈ VI | var(σ(x)) = ∅}.

The abstraction and concretization maps are as follows [Marriott and Søndergaard 1993]. For any Σ ∈ ℘(Subst) and f ∈ Def

α_{Def} (Σ) = ∨_{Def} {gdep(σ) | σ ∈ Σ},
γ_{Def} (f) = {σ ∈ Subst | ∀σ′ ≤ σ. ground(σ′) ⊧ f}.

These two mappings form a Galois insertion of Def into ℘(Subst) [Armstrong et al. 1994; Marriott and Søndergaard 1993].

As an example, assume VI ={x, y, z, w}. The formula x ∧ (y ↔ z) is an element of Def that represents the substitutions σ such that for any instance σ′ of σ the following conditions hold: the term σ′(x) is ground, and σ′(y) is ground iff also σ′(z) is ground. In particular, σ_{1} = {x/a, y/b, z/c} and σ_{2} = {x/a, y/v, z/v, w/u} satisfy these properties. Thus, {σ_{1}, σ_{2}} ⊆ γ_{Def} (x ∧ (y ↔ z)).

The following result relates a substitution with its abstraction in Def . It will be useful later.

Lemma 8.3.1. For any σ ∈ Subst, Models(α_{Def} ({σ}))={ground(σ′)|σ′ ∈ Δ_{σ}}.

Proof. The ⊇ inclusion follows by definition of α_{Def} . For the other direction, we show that for any m ∈ Models(α_{Def} ({σ})), there exists a substitution σ_{m} = δ ∘σ ∈ Δ_{σ} such that ground(σ_{m}) = m. Since m ⊧ ∃\overline{V I}. ∧ \{x ↔ ∧var(σ(x)) | σ(x) ≠ x\}, there exists m′ that extends m on all the variables in σ (also those not in V I), such that m′ ⊧ ∧{x ↔ ∧var(σ(x)) | σ(x) ≠ x}. Using m′ we define δ as follows:

∀x ∈ V ar. δ(x) = \{ \begin{matrix}a & if x ∈ m′ \\ x & otherwise. \end{matrix}

2The formulae of propositional logic defined by taking as propositional variables the elements of VI (see also Armstrong et al. [1994] and Marriott and Søndergaard [1993]).

ACM Transactions on Programming Languages and Systems, Vol. 19, No. 1, January 1997.

It is easy to see that for any x ∈ V ar, σ_{m}(x) is ground ⇔ x ∈ m′. In fact

σ_{m}(x) is ground ⇔ δ(σ(x)) is ground
⇔ m′ ⊇ V ar(σ(x))
⇔ x ∈ m′  (since m′ ⊧ x ↔ ∧V ar(σ(x))).

It suffices now to observe that ground(σ_{m}) = m′ ∩ V I = m.

By this lemma, the following fact about the abstraction in Def of sets of substitutions is immediate. Here, the following notation is used: if A is any set and X ⊆ ℘(A), then cli(X) is the least superset of X that is closed under intersection of its elements.

Corollary 8.3.2. For any Σ ⊆ Subst,

α_{Def} (Σ) = cli({ground(σ′) | σ′ ∈ Δ_{σ}, σ ∈ Σ}).

8.4 Relation between Def and Sharing

In Cortesi et al. [1992], it has been shown that there is a Galois connection between Def and Sharing. We prove here something more, namely the existence of a Galois insertion.

The abstraction function which maps an element S of Sharing into a formula of Def capturing its ground dependency information is defined as follows:

α(S) = f, such that Models(f) = \{\overline{∪B} | B ≠ ∅ and B ⊆ S\},

where \overline{∪B} is the set-theoretic complement of ∪B with respect to VI, i.e., \overline{∪B} = VI \ ∪B. It is not difficult to see that, according to the above definition, α is welldefined, i.e., α(S) ∈ Def for all S ∈ Sharing. In fact, Y = \{\overline{∪B} | B ≠ ∅ and B ⊆ S\} is closed under intersection (i.e., conjunction of models):

∀m_{1} = \overline{∪B_{1}}, m_{2} = \overline{∪B_{2}} ∈ Y. m_{1} ∩ m_{2} = \overline{∪(B_{1} ∪ B_{2})} ∈ Y.

For instance, if VI = {x, y, z, w} and S = {∅, {x, y}, {x, z}}, then α(S) is the formula in Def with the following models:

{∅} ⊆ S gives the model ⟶ {x, y, z, w}

{{x, y}} ⊆ S gives the model ⟶ {z, w}

{{x, z}} ⊆ S gives the model ⟶ {y, w}

{{x, y}, {x, z}} ⊆ S gives the model ⟶ {w}.

From this, one sees that α(S) = w ∧ (x ↔ (y ∧ z)), which expresses that for every σ ∈ γ_{Sharing}(S) the variable w is ground in σ, and x is ground in σ iff also y and z are ground in σ. Also observe that α(∅) = false.

In Cortesi et al. [1992], an abstraction function from Sharing to Def was given that looks different from the α described above. However, it is easy to show that the two functions coincide. The abstraction map C was given as follows:

C(S) = \{ \begin{matrix}false & if S = ∅ \\ ∧\{∧W → x | \{x\}, W ⊆ V I, ∀A ∈ S. x ∈ A ⇒ W ∩ A ≠ ∅\} & otherwise. \end{matrix}

Lemma 8.4.1. C = α.

ACM Transactions on Programming Languages and Systems, Vol. 19, No. 1, January 1997.

Proof. The case of S = ∅ is trivial. It is easy to see that ∀S ∈ Sharing \ {∅}. α(S) ⊧ C(S): assume that m is a model of α(S) and that m |̸= C(S). Then, there is a definite formula ∧W → x implied by C(S) such that W ⊆ m and x ∉ m. Since m = \overline{∪X}, for some X ⊆ S, this means that there is A ∈ X (and thus in S) such that x ∈ A and W ∩ A = ∅, but this contradicts the hypothesis that C(S) ⊧ ∧W → x.

For the other direction, assume that there is a model m of C(S) that is not a model of α(S). Let X = \{A ∈ S | A ⊆ \overline{m}\}. By the hypothesis that m |̸= α(S), it must be that \overline{∪X} ⊃ m, and thus there exists y ∈ \overline{∪X} \ m. It is obvious that m |̸= ∧m → y. We will now show that C(S) ⊧ ∧m → y, finding a contradiction. To this end, it suffices to observe that all A ∈ S such that A ∩ m = ∅ are in X, and thus, since y ∈ \overline{∪X}, y is in none of these sets.

The concretization function from Def into Sharing, adjoint to α, is defined as follows:

γ(f) = \{\overline{m} ⊆ VI | m ⊧ f\}.

The functions α and γ are obviously monotonic. Indeed, they form a Galois insertion.

Theorem 8.4.2. α and γ form a Galois insertion of Def into Sharing.

Proof. We show the following points: (i) ∀S ∈ Sharing. S ⊆ γ(α(S)); (ii) ∀f ∈ Def . f = α(γ(f)).

(i) If A ∈ S ∈ Sharing, by definition of α, \overline{A} ⊧ α(S), and thus, by definition of γ, A ∈ γ(α(S)).

(ii) It suffices to observe that, since each formula f ∈ Def has its set of models closed under intersection, γ(f) is an element of Sharing closed under union. From this and the definition of α, the desired relation follows.

This concludes the proof.

The domain Def can therefore be represented as the closure operator γ ∘ α on Sharing. From the proof of the above theorem, it will not be surprising that this closure operator is as follows.

Lemma 8.4.3. The closure operator γ ∘ α is the function that, for any S ∈ Sharing, gives the closure of S under set union. Formally, γ ∘ α = clu, where

clu(S) = {A | ∃A_{1},…, A_{n} ∈ S. A = A_{1} ∪… ∪ A_{n}}.

We show now that this insertion of Def into Sharing is coherent with the insertions of Sharing into ℘(Subst), and of Def into ℘(Subst). More precisely, we show that α_{Def} = α ∘ α_{Sharing} and that γ_{Def} = γ_{Sharing} ∘ γ. The following lemma is useful for this purpose. It is interesting to observe the similarity of this result with Lemma 8.3.1 and Corollary 8.3.2.

Lemma 8.4.4. Let Σ ⊆ Subst and α_{Sharing}(Σ) = S. Then,

cli(\{ground(σ′) | σ′ ∈ Δ_{σ}, σ ∈ Σ\}) = \{\overline{∪X} | X ⊆ S\}.

ACM Transactions on Programming Languages and Systems, Vol. 19, No. 1, January 1997.

Proof.

(⊆). Let σ′ ∈ Δ_{σ} and σ ∈ Σ. We define

X = {share(σ, y) | y ∈ V ar, var(σ′(y)) ≠ ∅}.

We want to show that ground(σ′) = \overline{∪X}. If σ′(y) is not ground, then all the variables x in share(σ, y) are not ground in σ′, i.e., var(σ′(x)) contains var(σ′(y)); conversly, if x ∉ ∪X, then all variables in var(σ(x)) are made ground by σ′, and thus x is also ground in σ′. Let us consider now two substitutions σ_{1} and σ_{2} that are instances of (possibly distinct) substitutions in Σ. By the above argument, there are X_{i} ⊆ S, i = 1, 2, such that ground(σ_{i}) = \overline{∪X_{i}}; from this, ground(σ_{1})∩ground(σ_{2}) = \overline{∪(X_{1} ∪ X_{2})}.

(⊇). By the argument just used, it suffices to show the following:

∀A ∈ S.∃σ ∈ Σ, σ′ ∈ Δ_{σ}. ground(σ′) = \overline{A}.

By definition of α_{Sharing}, there must be y ∈ V ar and σ ∈ Σ such that A = share(σ, y). The desired instance of σ is σ′ = δ ∘ σ, with δ as follows:

∀x ∈ V ar. δ(x) = \{ \begin{matrix}a & if share(σ, x) ≠ share(σ, y), \\ x & otherwise. \end{matrix}

It is easy to see that ground(σ′) = \overline{A}.

This concludes the proof.

We can now prove the coherency of α and γ.

Theorem 8.4.5. α_{Def} = α ∘ α_{Sharing} and γ_{Def} = γ_{Sharing} ∘ γ.

Proof. Since the composition of Galois insertions produces a Galois insertion [Cousot and Cousot 1992a], α ∘ α_{Sharing} and γ_{Sharing} ∘ γ form a Galois insertion of Def into ℘(Subst). From this and the well-known fact that in a Galois insertion one of the two functions uniquely determines the other one [Cousot and Cousot 1992a], it suffices to show only one of the two relations in order to prove the other one too. We will show that α_{Def} = α ∘ α_{Sharing}. For any Σ ∈ ℘(Subst),

α_{Def} (Σ) = cli({ground(σ′) | σ′ ∈ Δ_{σ}, σ ∈ Σ}) (by Corollary 8.3.2)
= \{\overline{∪X} | X ⊆ α_{Sharing}(Σ)\}  (by Lemma 8.4.4)
= α(α_{Sharing}(Σ))  (by definition of α).

This concludes the proof.

As a consequence of previous results, we get the following corollary.

Corollary 8.4.6.

(i) α = α_{Def} ∘ γ_{Sharing}; (ii) γ = α_{Sharing} ∘ γ_{Def} .

Proof. (i): From α_{Def} = α ∘ α_{Sharing}, shown in Theorem 8.4.5, one obtains, composing both sides with γ_{Sharing},

α_{Def} ∘ γ_{Sharing} = α ∘ α_{Sharing} ∘ γ_{Sharing}.

It suffices now to observe that α_{Sharing} ∘ γ_{Sharing} is the identity, because the two functions form a Galois insertion. Point (ii) is shown similarly.

ACM Transactions on Programming Languages and Systems, Vol. 19, No. 1, January 1997.

8.5 Sharing^{+}: The Complement of Def w.r.t. Sharing

In previous sections, we have shown that Def corresponds to the closure operator clu on Sharing, where for any S ∈ Sharing, clu(S) is the closure of S under set union. We now compute the complement of Def with respect to Sharing by using the methodology illustrated in Section 3.1. We will call such a domain Sharing^{+}. In the following, we will use the representation of Def as (the set of fixpoints of) clu, i.e., Def = {S ∈ Sharing | S = clu(S)}.

We construct a chain X_{0}, X_{1}, X_{2},… of subsets of Sharing following the definitions in Section 3.1. According to such definitions, we have that

X_{0} = {℘(VI )}.

In order to construct X_{1}, consider the set X = maxs(Sharing \ Def ). The set X_{1} is defined as the closure of X_{0} ∪ X under the glb on Sharing, namely under set intersection. Let us analyze X. For each S ∈ X, S is not closed under set union (otherwise S ∈ Def ), and there exists only a nonempty set A ⊆ VI such that A ∉ S, i.e., S = ℘(V I) \ {A} with A ≠ ∅ (otherwise S would not be maximal). Furthermore, since S is not closed under union, A cannot be a singleton. Hence, we have

X = {℘(VI ) \ {A} | A ⊆ VI and |A| ≥ 2}.

Observe now that every element of Sharing which contains the empty set and all singletons of VI either is ℘(VI ), or it can be obtained by set intersection of suitable elements of X. If we define singletons(VI ) = {{x} | x ∈ VI }, we therefore have

X_{1} = {S ∈ Sharing | singletons(VI ) ⊆ S}.

We show now that the closure of X_{1} ∪ Def under set intersection coincides with Sharing, which implies that we have already reached the limit of the construction, i.e., X_{2} = X_{1}. Let S ∈ Sharing. If S = ∅ then S ∈ Def . Otherwise, observe that S ∪ singletons(VI ) ∈ X_{1}, clu(S) ∈ Def , and

(S ∪ singletons(VI )) ∩ clu(S) = (S ∩ clu(S)) ∪ (singletons(VI ) ∩ clu(S))
= S ∪ (singletons(VI ) ∩ S)
= S.

We can therefore conclude that X_{2} = X_{1}. Thus, defining

Sharing^{+} = {S ∈ Sharing | singletons(VI ) ⊆ S}

we have proved the following theorem.

Theorem 8.5.1. Sharing ∼Def = Sharing^{+}.

The closure operator on Sharing corresponding to Sharing^{+} is, of course, the closure under union with singletons(VI ). Formally, denoting such operator by cls, we have cls(S) = S ∪ singletons(VI ). For instance, if VI ={x, y}, then Sharing^{+} is the simple domain depicted below.

\begin{matrix}\{∅, \{x\}, \{y\}, \{x, y\}\} \\ \{∅, \{x\}, \{y\}\} \end{matrix}

ACM Transactions on Programming Languages and Systems, Vol. 19, No. 1, January 1997.

Let us try to interpret this result. If a set S ∈ Sharing contains the singleton {x}, then S gives no ground dependency information concerning x, i.e., it represents all those substitutions where the groundness of x does not depend on the groundness of any other variable in VI. Thus, the presence of singletons prevents expressing ground dependencies. This intuition is confirmed by the easy observation that for any S ∈ Sharing^{+}, α(S) = true. Apart from the ground dependencies, however, for S ∈ Sharing, all S′ such that S \ singletons(VI ) ⊆ S′ ⊆ S ∪ singletons(VI ) do provide the same sharing information as S. This is because for any y, z ∈ VI and any substitution σ, the fact that y and z share under σ is represented in Sharing by a set of cardinality at least two. These observations are coherent with the fact that Sharing^{+} is what remains of Sharing once Def is removed from it.

9. RELATED AND FURTHER WORK

In this article, we have introduced the notion of complementation in abstract interpretation. Although our interest in this work is mainly concerned with abstract interpretation for program analysis, the same notion of complementation can be applied in any field where abstract interpretation theory is used. In particular, complementation can also be used for semantics related by abstract interpretation. Cousot and Cousot [1992b] proved that abstract interpretation can be used to systematically design hierarchies of semantics. In this case, both the standard denotational and axiomatic semantics can be derived by abstract interpretation of a generalized SOS operational semantics of the language. This technique has been recently applied in logic programming in Comini and Levi [1994], and Giacobazzi [1996], where hierarchies of collecting semantics are designed by abstracting SLD resolution. The interest in complementation is therefore evident in this field. Semantics, as well as analyses, can be composed and complemented, providing a real algebra of observable properties and semantics of programming languages. A preliminary report on this research is in Giacobazzi and Ranzato [1996].

Very recently, Filé and Ranzato [1996] have stated a new sufficient lattice-theore-tic condition on the complete lattice L that guarantees the existence of pseudocomplements of closure operators on L. The relationship with the condition of meetcontinuity of L in Theorem 3.6 is, to the best of our knowledge, not yet known in the lattice-theoretic literature. Also, Filé and Ranzato [1996] provided a practical systematic methodology, based on standard lattice-theoretic notions, to compute complements, having some analogy with that presented in Section 3.1. Further work will be devoted to understand the precise relationship between the two approaches. Another recent related work is in Marchiori [1996], where the author considers decompositions of some domains for the analysis of logic programs characterized by means of first-order formulae.

ACKNOWLEDGMENTS

We are grateful to the anonymous referees and to the TOPLAS Associate Editor Sam Kamin, for their helpful comments. This article has been conceived while Roberto Giacobazzi and Francesco Ranzato were visiting LIX, Laboratoire d’Informatique, École Polytechnique, Paris. They thank LIX , and in particular Radhia Cousot, for the kind hospitality.

ACM Transactions on Programming Languages and Systems, Vol. 19, No. 1, January 1997.

REFERENCES

Armstrong, T., Marriott, K., Schachte, P., and Søndergaard, H. 1994. Boolean functions for dependency analysis: Algebraic properties and efficient representation. In Proceedings of the 1st International Static Analysis Symposium (SAS ’94 ), B. Le Charlier, Ed. Lecture Notes in Computer Science, vol. 864. Springer-Verlag, Berlin, 266–280.

Birkhoff, G. 1967. Lattice Theory. AMS Colloquium Publication, 3rd edition. AMS, Providence,

R.I. Codish, M., Mulkers, A., Bruynooghe, M., García de la Banda, M., and Hermenegildo,

M. 1995. Improving abstract interpretations by combining domains. ACM Trans. Program. Lang. Syst. 17, 1, 28–44.

Comini, M. and Levi, G. 1994. An algebraic theory of observables. In Proceedings of the 1994 International Logic Programming Symposium (ILPS ’94 ), M. Bruynooghe, Ed. The MIT Press, Cambridge, Mass., 172–186.

Cortesi, A., Filé, G., and Winsborough, W. 1992. Comparison of abstract interpretations. In Proceedings of the 19th International Colloquium on Automata, Languages and Programming (ICALP ’92 ), W. Kuich, Ed. Lecture Notes in Computer Science, vol. 623. Springer-Verlag, Berlin, 521–532.

Cortesi, A., Filé, G., and Winsborough, W. 1996. Optimal groundness analysis using propo-

sitional logic. J. Logic Program. 27, 2, 137–167. Cousot, P. 1978. Méthodes Itératives de Construction et d’Approximation de Points Fixes

d’Opérateurs Monotones sur un Treillis, Analyse Sémantique des Programmes. Ph.D. thesis, Université Scientifique et Médicale de Grenoble, Grenoble, France.

Cousot, P. and Cousot, R. 1976. Static determination of dynamic properties of programs. In

Proceedings of the 2nd International Symposium on Programming. Dunod, Paris, 106–130. Cousot, P. and Cousot, R. 1977. Abstract interpretation: A unified lattice model for static

analysis of programs by construction or approximation of fixpoints. In Conference Record of the 4th ACM Symposium on Principles of Programming Languages (POPL ’77 ). ACM Press, New York, 238–252.

Cousot, P. and Cousot, R. 1979. Systematic design of program analysis frameworks. In Conference Record of the 6th ACM Symposium on Principles of Programming Languages (POPL ’79 ). ACM Press, New York, 269–282.

Cousot, P. and Cousot, R. 1992a. Abstract interpretation and application to logic programs.

J. Logic Program. 13, 2-3, 103–179. Cousot, P. and Cousot, R. 1992b. Inductive definitions, semantics and abstract interpretation.

In Conference Record of the 19th ACM Symposium on Principles of Programming Languages (POPL ’92 ). ACM Press, New York, 83–94.

Cousot, P. and Cousot, R. 1994. Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and per analysis of functional languages). In Proceedings of the IEEE International Conference on Computer Languages (ICCL ’94 ). IEEE Computer Society Press, Los Alamitos, Calif., 95–112.

Dart, P. 1988. Dependency analysis and query interfaces for deductive databases. Ph.D. thesis,

Univ. of Melbourne, Melbourne, Australia. Dart, P. 1991. On derived dependencies and connected databases. J. Logic Program. 11, 2,

163–188. Davey, B. A. and Priestley, H. A. 1990. Introduction to Lattices and Order. Cambridge

University Press, Cambridge, U.K. Dwinger, P. 1954. On the closure operators of a complete lattice. Indagationes Mathematicæ 16,

560–563. Filé, G., Giacobazzi, R., and Ranzato, F. 1996. A unifying view of abstract domain design.

ACM Comput. Surv. 28, 2, 333–336. Filé, G. and Ranzato, F. 1996. Complementation of abstract domains made easy. In Pro-

ceedings of the 1996 Joint International Conference and Symposium on Logic Programming (JICSLP ’96 ), M. Maher, Ed. The MIT Press, Cambridge, Mass., 348–362.

Frink, O. 1962. Pseudo-complements in semi-lattices. Duke Math. J. 29, 505–514.

Giacobazzi, R. 1996. “Optimal” collecting semantics for analysis in a hierarchy of logic program semantics. In Proceedings of the 13th International Symposium on Theoretical Aspects of Computer Science (STACS ’96 ), C. Puech and R. Reischuk, Eds. Lecture Notes in Computer Science, vol. 1046. Springer-Verlag, Berlin, 503–514.

Giacobazzi, R., Palamidessi, C., and Ranzato, F. 1996. Weak relative pseudo-complements of

closure operators. Algebra Universalis 36, 3, 405–412. Giacobazzi, R. and Ranzato, F. 1996. Complementing logic program semantics. In Proceedings

of the 5th International Conference on Algebraic and Logic Programming (ALP ’96 ), M. Hanus and M. Rodríguez Artalejo, Eds. Lecture Notes in Computer Science. Springer-Verlag, Berlin, 238–253.

Gierz, G., Hofmann, K. H., Keimel, K., Lawson, J. D., Mislove, M., and Scott, D. S. 1980.

A Compendium of Continuous Lattices. Springer-Verlag, Berlin. Grätzer, G. 1978. General Lattice Theory. Birkhäuser Verlag, Basel, Switzerland. Hunt, S. 1990. PERs generalize projections for strictness analysis. In Proceedings of the 1990

Glasgow Functional Programming Workshop, S. Peyton Jones, G. Hutton, and C. K. Holst, Eds. Workshops in Computing. Springer-Verlag, Berlin, 156–168.

Jacobs, D. and Langen, A. 1989. Accurate and efficient approximation of variable aliasing in logic programs. In Proceedings of the 1989 North American Conference on Logic Programming (NACLP ’89 ), E. L. Lusk and R. A. Overbeek, Eds. The MIT Press, Cambridge, Mass., 154– 165.

Jacobs, D. and Langen, A. 1992. Static analysis of logic programs for independent AND-

parallelism. J. Logic Program. 13, 2-3, 154–165. Kam, J. B. and Ullman, J. D. 1977. Monotone data flow analysis frameworks. Acta Informat-

ica 7, 305–317. Kildall, G. A. 1973. A unified approach to global program optimization. In Conference Record

of the 1st ACM Symposium on Principles of Programming Languages (POPL ’73 ). ACM Press, New York, 194–206.

Marchiori, E. 1996. Prime factorizations of abstract domains using first order logic. In Proceedings of the 5th International Conference on Algebraic and Logic Programming (ALP ’96 ), M. Hanus and M. Rodríguez Artalejo, Eds. Lecture Notes in Computer Science. Springer-Verlag, Berlin, 209–223.

Marriott, K. and Søndergaard, H. 1993. Precise and efficient groundness analysis for logic

programs. ACM Lett. Program. Lang. Syst. 2, 1-4, 181–196. Morgado, J. 1962. Note on complemented closure operators of complete lattices. Portu-

galiæMathematica 21, 3, 135–142. Muthukumar, K. and Hermenegildo, M. 1991. Combined determination of sharing and freeness

of program variables through abstract interpretation. In Proceedings of the 8th International Conference on Logic Programming (ICLP ’91 ), K. Furukawa, Ed. The MIT Press, Cambridge, Mass., 49–63.

Mycroft, A. 1980. The theory and practice of transforming call-by-need into call-by-value. In Proceedings of the 4th International Symposium on Programming, B. Robinet, Ed. Lecture Notes in Computer Science, vol. 83. Springer-Verlag, Berlin, 270–281.

Mycroft, A. 1981. Abstract interpretation and optimising transformations for applicative pro-

grams. Ph.D. thesis, CST-15/81, Univ. of Edinburgh, Edinburgh, Scotland. Mycroft, A. 1993. Completeness and predicate-based abstract interpretation. In Proceedings

of the ACM Symposium on Partial Evaluation and Program Manipulation (PEPM ’93 ). ACM Press, New York, 179–185.

Nielson, F. 1985. Tensor products generalize the relational data flow analysis method. In Proceedings of the 4th Hungarian Computer Science Conference, M. Arató, I. Kátai, and L. Varga, Eds. 211–225.

Sundararajan, R. and Conery, J. 1992. An abstract interpretation scheme for groundness, freeness, and sharing analysis of logic programs. In Proceedings of the 12th Conference on Foundations of Software Technology and Theoretical Computer Science (FST&TCS ’92 ), R. Shyamasundar, Ed. Lecture Notes in Computer Science, vol. 652. Springer-Verlag, Berlin, 203–216.

Varlet, J. 1963. Contribution à l’étude des treillis pseudo-complémentés et des treillis de Stone.

Mémoires de la Société Royale des Sciences de Liège 8, 4, 1–71. Wadler, P. and Hughes, R. J. M. 1987. Projections for strictness analysis. In Proceedings of the

Conference on Functional Programming Languages and Computer Architecture (FPCA ’87 ), G. Kahn, Ed. Lecture Notes in Computer Science, vol. 274. Springer-Verlag, Berlin, 385–407.

Ward, M. 1942. The closure operators of a lattice. Ann. Math. 43, 2, 191–196. Yi, K. and Harrison, W. L. 1993. Automatic generation and management of interprocedu-

ral program analyses. In Conference Record of the 20th ACM Symposium on Principles of Programming Languages (POPL ’93 ). ACM Press, New York, 246–259.

Received November 1995; revised June 1996; accepted October 1996