A characterization of symmetric semantics by domain complementation

Roberto Giacobazzi

Dipartimento Scienti�co e Tecnologico

Universit� a di Verona

Strada Le Grazie, I-37134 Verona, Italy

giaco@sci.univr.it

Isabella Mastroeni

Dipartimento Scienti�co e Tecnologico Universit� a di Verona

Strada Le Grazie, I-37134 Verona, Italy

mastroen@arena.sci.univr.it

ABSTRACT

We characterize the symmetric structure of Cousot’s hierarchy of semantics in terms of a purely algebraic manipulation of abstract domains. We consider domain complementation in abstract interpretation as a formal method for systematically deriving complementary semantics of programming languages. We prove that under suitable hypothesis the semantics abstraction commutes with respect to domain complementation. This result allows us to prove that angelic and demonic/infinite semantics are complementary and provide a minimal decomposition of all natural-style trace-based, relational, denotational, Dijkstra’s predicate transformer and Hoare’s axiomatic semantics. We apply this construction to the case of concurrent constraint programming, characterizing well known semantics as abstract interpretation of maximal traces of constraints.

Categories and Subject Descriptors

D.3 [Programming languages]: Formal definitions and theory—Semantics; F.3 [Logics and meanings of programs]: Semantics of Programming Languages—algebraic approaches to semantics, denotational semantics, operational semantics

General Terms

Theory

Keywords

Abstract interpretation, domain complementation, program semantics, concurrent constraint programming.

1. INTRODUCTION

Since its origin in 1977, abstract interpretation [9] has been widely used, implicitly or explicitly, to describe and formalize approximate computations in many different areas of

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for pro�t or commercial advantage and that copies bear this notice and the full citation on the �rst page. To copy otherwise, to republish, to post on servers or to redistribute to lists, requires prior speci�c permission and/or a fee. PPDP ’00, Montr� eal, Canada. Copyright 2000 ACM 1-58113-265-4/00/0009 ..$5.00

computer science, from its very beginning use in formalizing (compile-time) program analysis frameworks to more recent applications in model checking, program verification, data security, type inference, automated deduction, and comparative semantics. This justifies a now well established definition of abstract interpretation as a general theory to approximate the semantics of discrete dynamic systems” [7].

Semantics is central in the construction of an abstract interpretation. The so called concrete semantics specifies the observable property of program behavior and any more abstract semantics, e.g. decidable semantics for program analysis, can be derived by abstraction. As a consequence, semantics, at any level of abstraction, can be fully specified as an abstract interpretation of a more concrete base semantics. This key idea is the basis of Cousot’s design of a complete hierarchy of semantics of programming languages [12, 8]. A number of semantics including big-step, termination and nontermination, Plotkin’s natural, Smyth’s demonic, Hoare’s angelic relational and corresponding denotational, Dijkstra’s predicate transformer weakest-precondition and weakest-liberal precondition and Hoare’s partial and total axiomatic semantics, have all been derived by successive abstractions from an (operational) maximal trace semantics of a transition system. The resulting hierarchy (here called Cousot’s hierarchy) provides a complete account on the structure and the relative precision of most well known semantics of programming languages. One of the major challenges of this construction is that semantics can be fully characterized as domain abstractions, and therefore they can be manipulated in a purely algebraic way by modifying domains. This view of semantics as domains provides both a better insight on the structure and relative precision of traditional well known semantics of programming languages and the possibility to systematically specify new semantics by composition, decomposition, refinement and simplification of existing ones, by manipulating the corresponding domains.

1.1 The main results

In this paper we analyze Cousot’s hierarchy of semantics and we characterize its symmetric structure (see Fig. 1) in terms of a purely algebraic manipulation of domains. We consider abstract domain complementation introduced in [6] as the basic formal method for decomposing semantics and reduced product of domains introduced in [11] as the basic operation for composing semantics. Given any two semantics 𝒮_{1} and 𝒮_{2}, the product semantics 𝒮_{1} ⊓ 𝒮_{2} is the most abstract semantics which is as precise as both 𝒮_{1} and 𝒮_{2}, namely which is able to observe both the observables of 𝒮_{1} and 𝒮_{2}. Domain complementation was originally introduced to decompose abstract domains in static program analysis, and it is the inverse operation to reduced product. In our case, this operation provides a systematic methodology for decomposing semantics by characterizing the most abstract semantics 𝒮 which, when composed with a given semantics ℬ, yields the semantics 𝒞 = 𝒮 ⊓ ℬ as result. These operations provide advanced methods for comparing semantics with respect to their relative expressiveness. This kind of information is particularly relevant when studying hierarchies of semantics, in particular in studying semantics observing complementary behaviors of programs, e.g. finite and infinite computations of a transition system. According to Cousot’s construction in fact, any semantic style (trace-operational, relational, denotational, Dijkstra’s predicate transformer and Hoare’s axiomatic semantics) may have a corresponding natural, finite/angelic, demonic, and infinite nature. The nature of each semantics defines a corresponding observable behavior of programs (later called observable), which can be parameterized according to the chosen semantic style, and it corresponds respectively to: finite and infinite, terminating, chaotic nonterminating, and infinite computations. We prove that this highly symmetric structure is a consequence of a common pattern of abstraction between semantic styles and observables, ranging from operational trace-based to the more abstract Hoare’s axiomatic semantics. We characterize this pattern in terms of some basic properties of the closure operators associated with the semantics abstractions in Cousot’s hierarchy. This allows us to prove the basic results on symmetric semantics for the trace-operational semantic style only, deriving the results concerning all the other styles and observables as a simple consequence. In particular we prove that natural semantics are always the reduced product of finite/angelic and demonic or infinite semantics, and that these semantics factorize the natural semantic construction by complementation. We prove that any finite/angelic semantics can be systematically derived as the domain complementation in the natural semantics of the demonic or infinite semantics. Moreover, we prove that finite/angelic and infinite semantics always form a most abstract decomposition of any natural semantics, and that demonic semantics can be further factorized in terms of infinite semantics and a new semantics, here called pseudo-demonic, which is unable to observe infinite computations in presence of finite chaos, namely when programs may produce any possible output in finite time. These results provide both an algebraic characterization of complementary observable properties in semantics and a decomposition result for observable properties of programs in terms of complementary observables, similarly to the wellknown Alpern & Schneider’s safety/liveness decomposition of properties of concurrent program executions (cf. [2]). Our results are general and can be applied to any programming languages whose semantics can be defined as traces of program states in a transition system.

We apply this construction to the case of concurrent constraint programming ccp languages [28]. These languages well fit into Cousot’s hierarchy of semantics being easily defined in terms of traces of constraints in a transition system. We prove that both Saraswat’s closure-based denotational [29] and de Boer et al.’s predicate transformer semantics [13] can be derived by abstract interpretation from maximal traces of constraints associated with an operational smallstep transition system semantics of ccp programs, and consequently the corresponding finite/angelic, demonic, and infinite semantics can be specified by domain complementation. The paper is organized as follows. In Sec. 2 we recall the basic theory of abstract interpretation. Cousot’s hierarchy of semantics is summarized in Sec. 3, while in Sec. 4 we recall the basic notion of domain complementation. In Sec. 5 we prove some basic results concerning closure operators and domain complementation. These results are the basis for generalizing the results in Sec. 6 and characterizing the symmetric structure of different observables, to the whole hierarchy of semantics. This generalization is in Sec. 6.2. In Sec. 6.3, we consider the complementation of semantics with respect to a different order, which is used as computational order in Cousot’s hierarchy, and in Sec. 7 we apply our results to the case of concurrent constraint programming. Sec. 8 concludes.

1.2 State of the art

The foundation for a theory of abstract domains was fixed by Cousot & Cousot in [11]. The authors gave the main structure of abstract domains enjoying Galois connections and some basic operators to systematically compose domains, respectively the reduced product and reduced power operations. Since then, a number of papers have developed new domain operations and studied the impact of these operations in the design of abstract interpretations (e.g. see [21] for a survey). The notion of domain refinement and domain simplification, introduced in [16, 21], provided the very first generalization of these ideas. Intuitively a refinement is any operator performing an action of refinement with respect to the standard order of precision, e.g. by adding information to domains; while simplificators perform the dual action of “taking out” information from domains. Few examples are known on the use of systematic domain operations in abstract interpretation to reason about the structure and the expressiveness of semantics of programming languages. Most of these examples are in the semantics of logic programs, which basically relies on the hierarchy of semantics developed in [5, 18]. In [20] the authors study the relations between different semantics of logic programs, namely success pattern semantics, computed answer substitution semantics and call pattern semantics by means of complementation. This is the very first and unique example of the use of complementation in systematic semantics design. In [22], the authors proved that compositional (denotational) semantics of logic programs can be systematically designed by a generalization of Cousot’s reduced cardinal power operation [11] from non compositional semantics of computed answer substitution. To the best of our knowledge, the only use of domain operations in more general semantics constructions is in [8], where the domain operation of tensor product [30] is considered in order to design Hoare’s axiomatic semantics.

2. PRELIMINARIES

2.1 Basic notions

If S and T are sets, then ℘(S) denotes the powerset of S, S ∖T denotes the set-difference between S and T, S ⊂ T denotes strict inclusion, and for a function f : S → T and X ⊆ S, f(X) =^{def} {f(x) | x ∈ X}. By g ∘ f we denote the composition of the functions f and g, i.e., g∘f =^{def} λx.g(f(x)). The notation ⟨P, ≤⟩ denotes a poset P with ordering relation ≤, while ⟨P, ≤, ∨, ∧, ⊤, ⊥⟩ denotes a complete lattice P, with ordering ≤, lub ∨, glb ∧, greatest element (top) ⊤, and least element (bottom) ⊥. Often, ≤_{P} will be used to denote the underlying ordering of a poset P, and ∨_{P}, ∧_{P}, ⊤_{P} and ⊥_{P} denote the basic operations and elements of a complete lattice. The notation C ≅ A denotes that C and A are isomorphic ordered structures. x ∈ C is meet-irreducible if x = a ∧ b ⇒ x ∈ {a, b}. The set of meet-irreducible elements in C is denoted Mirr(C). The downward closure

of S is defined as ↓ S =^{def} {x ∈ P | ∃y ∈ S. x ≤_{P} y}, and

for x ∈ P, ↓ x is a shorthand for ↓ {x}, while the upward closure ↑ is dually defined. S ⟶T denotes the set of all functions from S to T. We use the symbol ⊑ to denote pointwise ordering between functions: If S is any set, P a poset, and f, g : S → P then f ⊑ g if for all x ∈ S, f(x) ≤_{P} g(x). Let C and A be complete lattices. Then, C ⟶^{m}A, C ⟶^{c}A, C ⟶^{a}A, and C ⟶^{coa}A denote, respectively, the set of all monotone, (Scott-)continuous, additive, and coadditive functions from C to A. Recall [1] that f ∈ C ⟶^{c}A iff f preserves lub’s of (nonempty) chains iff f preserves lub’s of directed subsets, and f : C → A is (completely) additive if f preserves lub’s of all subsets of C (emptyset included). Co-additivity is defined by duality. We denote by lfp(f) and gfp(f), respectively, the least and greatest fixpoint, when they exist, of an operator f on a poset. If f ∈ C ⟶^{c}C then lfp(f) = ∨_{i∈ℕ}f^{i}(⊥_{C}), where, for any i ∈ ℕ and x ∈ C, the i-th power of f in x is inductively defined as follows: f^{0}(x) = x; f^{i+1}(x) = f(f^{i}(x)). Dually, if f is co-continuous then gfp(f) = ∧_{i∈ℕ}f^{i}(⊤_{C}). {f^{i}(⊥_{C})}_{i∈ℕ} and {f^{i}(⊤_{C})}_{i∈ℕ} are called, respectively, the upper and lower Kleene’s iteration sequences of f (see [10]).

2.2 Abstract interpretation

Abstract domains can be equivalently formulated either in terms of Galois connections or closure operators [11]. An upper closure operator on a poset P is an operator ρ : P → P monotone, idempotent and extensive (∀x ∈ P. x ≤_{P} ρ(x)). Lower closure operators are defined dually. The set of all upper (lower) closure operators on P is denoted by uco(P) (lco(C)). Let ⟨C, ≤, ∨, ∧, ⊤, ⊥⟩ be a complete lattice. A basic property of closure operators is that each closure is uniquely determined by the set of its fixpoints ρ(C). For upper closures: X ⊆ C is the set of fixpoints of an upper closure on C iff X is a Moore-family of C, i.e., X = ℳ(X) =^{def} {∧S | S ⊆ X} — where ∧∅ = ⊤ ∈ ℳ(X). For any X ⊆ C, ℳ(X) is called the Moore-closure of X in C, i.e., ℳ(X) is the least (w.r.t. set-inclusion) subset of C which contains X and it is a Moore-family of C. It turns out that ⟨ρ(C), ≤⟩ is a complete meet subsemilattice of C (i.e., ∧ is its glb). Often, we will find particularly convenient to identify closure operators with their sets of fixpoints, possibly using as notation capital Latin letters. If C is a complete lattice then uco(C) ordered pointwise is also a complete lattice, denoted by ⟨uco(C), ⊑, ⊔, ⊓, λx.⊤, λx.x⟩, where for every ρ, η ∈ uco(C), {ρ_{i}}_{i∈I} ⊆ uco(C) and x ∈ C:

– ρ ⊑ η iff ∀y ∈ C. ρ(y) ≤ η(y) iff η(C) ⊆ ρ(C);

– (⊓_{i∈I}ρ_{i})(x) = ∧_{i∈I}ρ_{i}(x);

– (⊔_{i∈I}ρ_{i})(x) = x ⇔ ∀i ∈ I. ρ_{i}(x) = x; If α : C ⟶^{m}A and γ : A⟶^{m}C are monotone functions such that λx.x ⊑ γ ∘ α and α∘γ ⊑ λx.x, then (A, α, γ, C) is called a Galois connection (GC for short) or adjunction between C and A, also denoted ⟨C, ≤_{C}⟩ ⟶ ⟵_{α}^{γ} ⟨A, ≤_{A}⟩. Note that in GC, for any x ∈ C and y ∈ A: α(x) ≤_{A} y ⇔ x ≤_{C} γ(y) and γ(y) = ⋁ { x | α(x) ≤ y } and α(x) = ⋀ { y | x ≤ γ(y) }. The set of all GC’s between two complete lattices A and C is the tensor product A ⊗ C, which is a complete lattice and A ⊗ C ≅ A⟶^{a}C ≅ C ⟶^{coa}A [30]. If in addition α ∘ γ = λx.x (γ ∘ α = λx.x), then (A, α, γ, C) is a Galois insertion (GI) (resp. projection) also denoted ⟨C, ≤_{C}⟩ \overrightarrow{⟶} ⟵_{α}^{γ} ⟨A, ≤_{A}⟩ (resp. ⟨C, ≤_{C}⟩ ⟶ \overleftarrow{⟵}_{α}^{γ} ⟨A, ≤_{A}⟩) of A in C. It is worth noting that A ≅ C if and only if ⟨C, ≤_{C}⟩ \overrightarrow{⟶} \overleftarrow{⟵}_{α}^{γ} ⟨A, ≤_{A}⟩. The standard abstract interpretation framework is based on the adjoint relation between abstraction and concretization functions [9]. The concrete and abstract domains, C and A, are assumed to be complete lattices and are related by abstraction and concretization maps forming a GC (A, α, γ, C). Following a standard terminology, A is called an abstraction of C, and C is a concretization of A. If (A, α, γ, C) is a GI, then each value of the abstract domain A is useful in representing C, because all the elements of A represent distinct members of C, being γ 1-1. Any GC may be lifted to a GI by identifying in an equivalence class those values of the abstract domain with the same concretization. This process is known as reduction of the abstract domain. Note that any GI (A, α, γ, C) uniquely determines an upper closure operator γ ∘ α ∈ uco(C) and conversely, any closure operator ρ ∈ uco(C) uniquely determines a GI (ρ(C), ρ, id, C), up to isomorphic representation of domain’s objects. Hence, we will identify uco(C) with the so-called lattice 𝔏_{C} of abstract interpretations of C (cf. [9, Section 7] and [11, Section 8]), i.e., the complete lattice of all possible abstract domains (modulo isomorphic representation of their objects) of the concrete domain C. The pointwise ordering on uco(C) corresponds precisely to the standard ordering used to compare abstract domains with regard to their precision: A_{1} is more precise than A_{2} (i.e., A_{2} is an abstraction of A_{1}) iff A_{1} ⊑ A_{2} in uco(C) iff ⟨A_{1}, ≤_{A_{1}}⟩ \overrightarrow{⟶} ⟵_{α}^{γ} ⟨A_{2}, ≤_{A_{2}}⟩. Let \{A_{i}\}_{i∈I} ⊆ uco(C): ⊔_{i∈I}A_{i} is the most concrete among the domains in 𝔏_{C} which are abstractions of all the A_{i}’s, i.e., ⊔_{i∈I}A_{i} is the least (w.r.t. ⊑) common abstraction of all the A_{i}’s; and ⊓_{i∈I}A_{i} is (isomorphic to) the well-known reduced product (basically cartesian product plus reduction) of all the A_{i}’s, or, equivalently, it is the most abstract among the domains in 𝔏_{C} which are more concrete than every A_{i}. Let us remark that the reduced product can be also characterized as Moore-closure of set-union, i.e., ⊓_{i∈I}A_{i} = ℳ(∪_{i∈I}A_{i}).

3. COUSOT’S SEMANTICS HIERARCHY

In this section we recall Cousot’s hierarchy of semantics [12, 8]. We consider the operational semantics of a programming language that associates a discrete transition system with each well-formed program. In other words we associate a pair ⟨Σ, τ⟩ where Σ is a nonempty set of states and τ ⊆ Σ × Σ is a binary transition relation between a state and its possible successors. In the following, Σ+ and Σω⃗ =^{def} ℕ⟶Σ denote respectively the set of finite nonempty and infinite sequences of symbols in Σ. The length of a sequence σ ∈ Σ ∞ =^{def} Σ+ ∪ Σω⃗ is denoted |σ| ∈ ℕ ∪ {ω} and its i-th element is denoted σ_{i}. A non-empty finite (infinite) trace σ is a finite (infinite) sequence of program states where two consecutive elements are in the transition relation τ, i.e., for all i < |σ|: ⟨σ_{i}, σ_{i+1}⟩ ∈ τ. A generic trace is any such element in Σ ∞. The maximal trace semantics of a transitions system [12] is τ ∞ =^{def} τ + ∪ τ ω⃗, where if T ⊆ Σ is a set of final/blocking states τ n⃗ = {σ ∈ Σ+||σ| = n, ∀i ∈ [0, n) . ⟨σ_{i}, σ_{i+1}⟩ ∈ τ}, τ ω⃗ = {σ ∈ Σω⃗| ∀i ∈ ℕ . ⟨σ_{i}, σ_{i+1}⟩ ∈ τ}, and τ + = ∪_{n>0}{σ ∈ τ n⃗| σ_{n−1} ∈ T }. τ ∞ has been obtained in [12] as a fixpoint of a monotone operator F ∞ : ℘(Σ ∞) → ℘(Σ ∞) which is defined by a biinductive (inductive and co-inductive) definition on ⟨℘(Σ ∞), ⊑ ∞, ⊓ ∞, ⊔ ∞, ⊓ ∞, Σ+, Σω⃗⟩, where X ⊑ ∞ Y iff X ∩ Σ+ ⊆ Y ∩ Σ+ and Y ∩ Σω⃗ ⊆ X ∩ Σω⃗. This allows us to combine both least and greatest fixpoint in a unique fixpoint presentation: finite (terminating) traces are obtained by induction (lfp) of F ∞ on ⟨℘(Σ+), ⊆⟩ and infinite traces are obtained by co-induction (gfp) on ⟨℘(Σω⃗), ⊆⟩, which corresponds to the lfp of F ∞ in ⟨℘(Σω⃗), ⊇⟩. In this case: τ ∞ = lfp(F ∞) (see [12] for details). All semantics in the hierarchy are derived as abstract interpretation of the trace-based semantics. Cousot distinguishes between an approximation order, which is set inclusion on sets of generic traces, and a computational order which corresponds to the lifted order ⊑ ∞ characterizing finite and infinite traces as fixpoint of F ∞. The basic semantics in Cousot’s hierarchy are summarized in Table 1. Each semantics in natural style corresponds to a suitable abstraction of the basic natural trace-based semantics τ ∞. The relational semantics ℛ associates an input-output relation with program traces by using the bottom symbol ⊥ ∉ Σ, to denote nontermination. This corresponds to an abstraction of the maximal trace semantics where intermediate computation states are ignored. The denotational semantics 𝒟 abstracts away from the history of computations by considering input-output functions. This semantics is isomorphic to relational semantics. Dijkstra’s predicate transformer gwp and Hoare’s axiomatic semantics gℋ are represented respectively as co-additive functions, denoting weakest-precondition predicate transformers, and elements in tensor product domains, i.e., GC’s, specifying the adjoint relation between weakest-precondition and strongestpostcondition in Hoare’s triples {P } C {Q} (see [8]). Each semantics in natural style may have a corresponding angelic, demonic, or infinite observable which is again an abstraction. We recall here only the corresponding abstractions for the trace-based semantics.

Angelic. The angelic trace semantics τ + is designed as an abstraction of the maximal trace semantics, and it is obtained by approximating sets of possibly infinite traces with their finite ones, i.e.,

⟨℘(Σ ∞), ⊆⟩ \overrightarrow{⟶} ⟵_{α^{+}}^{γ^{+}} ⟨℘(Σ+), ⊆⟩ where α^{+}(X) = X ∩ Σ+

We denote by ℛ^{+}, 𝒟^{+}, wlp, and pℋ respectively the bigstep relational semantics [27], angelic denotational, weakestliberal precondition [14], and Hoare’s partial correctness semantics [25]. All these semantics have been proved by Cousot [8] to be the angelic abstractions of the corresponding semantics in natural style.

Demonic. The demonic trace semantics, denoted as τ ∂, is derived from the maximal trace semantics by approximat-

ing the nontermination by chaos ⟨℘(Σ ∞), ⊆⟩ \overrightarrow{⟶} ⟵_{α^{∂}}^{γ^{∂}} ⟨D∂, ⊆⟩,

where D∂ ⊆ ℘(Σ ∞) is such that X ∈ D∂ iff

σ ∈ X ∧ |σ| = ω ⇒ ∀δ ∈ Σ+. σ_{0}δ ∈ X

and α^{∂}(X) = X ∪{ σ_{0}δ | σ ∈ X, |σ| = ω, δ ∈ Σ+ }. We de-

note by ℛ^{∂}, 𝒟^{∂}, wp, and tℋ the demonic relational, demonic denotational [3], weakest-precondition [14] and Hoare’s total correctness semantics [25]. These semantics have been proved by Cousot [8] to be the demonic abstractions of the corresponding semantics in natural style.

In�nte. The infinite trace semantics, denoted τ ω⃗, is derived by observing nonterminating traces only, namely by the

following abstraction ⟨℘(Σ ∞), ⊆⟩ \overrightarrow{⟶} ⟵_{α^{ω}}^{γ^{ω}} ⟨℘(Σω⃗), ⊆⟩ where

α^{ω}(X) = X ∩ Σω⃗. The corresponding infinite semantics are denoted by ℛ^{ω}, 𝒟^{ω}, wp^{ω}, and tℋ^{ω}.

The whole hierarchy, relating semantics styles and observables is shown in Fig. 1, where continuous lines and arrows denote, respectively, isomorphisms and strict abstractions between semantics.

[figure: •; •; •; •; •; •; •; •; •; •; ∘; •; •; •; •; •; •; ∘; ∘; ∘; ∘; ∘; ∘; ∘; ∘; τ ∞; ℛ; 𝒟; gwp; gℋ; τ +; ℛ+; 𝒟+; wlp; pℋ; τ ∂; ℛ∂; 𝒟∂; wp; tℋ; τ ϱ⃗; ℛϱ; 𝒟ϱ; ^{wpϱ}; ^{tℋ ϱ}; τ ω⃗; ℛω; 𝒟ω; ^{wpω}; ^{tℋ ω}; angelic; natural; demonic; infinite; pseudo-dem; Hoare’s axiomatic; Dijkstra’s pred-trans; Denotational; Relational; Trace-based]

Figure 1: Semantics in Cousot’s hierarchy.

4. DOMAIN COMPLEMENTATION

A sequence of abstract domains {A_{i}}_{i∈I} is a (conjunctive) decomposition of the abstract domain B if B = ⊓_{i∈I}A_{i}. Abstract domain complementation introduced in [6] provides a systematic method for decomposing abstract domains. Complementation is the inverse operation of the reduced product (see [21]), namely an operation which, starting from any two domains C ⊑ D, gives as result the most abstract domain C ⊖ D, whose reduced product with D is exactly C (i.e., (C ⊖ D) ⊓ D = C). By the equivalence between closure operators and abstract domains, the above notion of complementation corresponds precisely to pseudocomplementation for the closure ρ_{D} corresponding to D in uco(C). Recall that if L is a meet-semilattice with bottom then the pseudo-complement of x ∈ L, if it exists, is the

Semantics  Domain relation  Abstraction
ℛ = α^{r}(τ ∞)  ⟨℘(Σ ∞), ⊆⟩ \overrightarrow{⟶} ⟵_{α^{r}}^{γ^{r}} ⟨℘(Σ × Σ_{⊥}), ⊆⟩  α^{r}(X) = \{ ⟨σ_{0}, σ_{n−1}⟩ | σ ∈ X, |σ| = n \} ∪

{ ⟨σ_{0}, ⊥⟩ | σ ∈ X, |σ| = ω }

𝒟 = α^{▶}(ℛ)  ⟨℘(Σ × Σ_{⊥}), ⊆⟩ \overrightarrow{⟶} \overleftarrow{⟵}_{α^{▶}}^{γ^{▶}} ⟨Σ ⟶ ℘(Σ_{⊥}), ⊑⟩  α^{▶}(X) =^{def} λs.\{s′ ∈ Σ| ⟨s, s′⟩ ∈ X\}

gwp = α^{gwp}(𝒟) ⟨Σ ⟶ ℘(Σ_{⊥}), ⊑⟩  \overrightarrow{⟶} \overleftarrow{⟵}_{α^{gwp}}^{γ^{gwp}} ⟨℘(Σ_{⊥})⟶^{coa}℘(Σ), ⊒⟩  α^{gwp}(f) = λP. \{ s | f(s) ⊆ P \}

gℋ = α^{gH}(gwp) ⟨℘(Σ_{⊥})⟶^{coa}℘(Σ), ⊒⟩ \overrightarrow{⟶} \overleftarrow{⟵}_{α^{gH}}^{γ^{gH}} ⟨℘(Σ) ⊗ ℘(Σ_{⊥}), ⊇⟩ α^{gH}(Φ) = \{ ⟨X, Y ⟩ ∈ ℘(Σ) × ℘(Σ_{⊥}) | X ⊆ Φ(Y) \}

Table 1: Basic natural-style semantics as abstract interpretations

unique element x^{∗} ∈ L such that x ∧ x^{∗} = ⊥ and ∀y ∈ L. (x ∧ y = ⊥) ⇒ (y ≤ x^{∗}) [4]. In a complete lattice L, if x^{∗} exists then x^{∗} = ∨{y ∈ L | x ∧ y = ⊥}. If every x ∈ L has the pseudo-complement, L is pseudo-complemented. It is worth noting that pseudo-complementation is the only possible form of complementation for abstract interpretation. Indeed, it is well known [15, 26] that uco(C) is complemented (in the standard sense) iff C is a complete well-ordered chain, and this is a far too restrictive hypothesis for semantic domains. The following results [19, 17] provide sufficient conditions on C such that uco(C) is pseudo-complemented. Recall that a complete lattice C is meet-continuous if for any chain Y ⊆ C and x ∈ C, x ∧ (∨Y) = ∨_{y∈Y} (x ∧ y). Moreover C is meet-generated by S ⊆ C if C = ℳ(S).

Theorem 4.1. Let C be a complete lattice.

1. If C is a meet-continuous then uco(C) is pseudo-com-plemented [19].

2. If C is meet-generated by Mirr(C) then uco(C) is pseudo-complemented and, for any A ∈ uco(C), we have

A^{∗} =^{def} C ⊖ A = ℳ(Mirr(C)∖A) [17].

Note that for any A, B ∈ uco(C) such that A ⊑ B, A ⊖ B is well defined if ↑A = uco(A) is pseudo-complemented.

5. SYMMETRIC ABSTRACTIONS

In the following we characterize the symmetric structure of Cousot’s hierarchy of semantics in terms of a general algebraic property of closure operators. The fact that the same angelic/demonic/infinite observables are abstractions of the natural semantics in any style (trace-based, relational, denotational, predicate transformer and axiomatic) is indeed a consequence of the fact that the abstractions that relates the different styles of semantics and observables commute all over Cousot’s hierarchy.

In order to better understand this situation we suppose to have a concrete semantic domain C which is generated by its meet-irreducibles, and two closure operators ρ, η ∈ uco(C). Recall that ρ ∘ η ∈ uco(C) iff ρ ∘ η = η ∘ ρ = η ⊔ ρ [26]. Therefore the structure in Fig. 2 is perfectly symmetric if the closure ρ(C) ⊖ ρ(η(C)) corresponds precisely to the abstraction by ρ of the complementary closure C ⊖ η(C), namely if ρ is an ⊖-morphism: ρ(C⊖η(C)) = ρ(C)⊖ρ(η(C)) or, equivalently, whenever (ρ ⊔ η)^{∗} computed in uco(ρ(C)) is the same closure as ρ ⊔ η^{∗}.

[figure: •; •; •; •; •; •; C; ρ(C); ρ(η(C)); η(C); C ⊖ η(C); ρ(C) ⊖ ρ(η(C))]

Figure 2: Basic abstraction structure.

[figure: •; •; •; •; •; •; •; •; 0; −; +; ∅; 0−; 0+; ℤ; ≠0; •; •; •; •; •; ℤ; ≠0; −; +; ∅]

Figure 3: The Sign and Nzero domains.

Example 5.1. Note that it is not always the case that ρ is an ⊖-morphism. Let Sign be the domain for sign analysis of integer variables in Fig. 3 and ρ(Sign) = {ℤ, 0−, −}. If η(Sign) = {ℤ, 0−, ∅}, then ρ(η(Sign)) = {ℤ, 0−}. Then we have ρ(Sign ⊖ η(Sign)) = ρ({ℤ, 0+, ≠ 0, +}) = {ℤ} while ρ(Sign) ⊖ ρ(η(Sign)) = {ℤ, −}.

Lemma 5.2. Let ρ, η ∈ uco(C). If ρ ∘ η = η ∘ ρ and ρ ∘ η^{∗} = η^{∗} ∘ ρ then (ρ ⊔ η^{∗}) ⊑ ρ ⊖ (ρ ⊔ η).

Proof. It is known that ρ ∘ η ∈ uco(C) iff ρ ∘ η = η ∘ ρ = ρ ⊔ η. It is immediate that ρ ⊑ (ρ ⊔ η) ⊓ (ρ ⊔ η^{∗}). Moreover, by definition of domain complementation, for each x ∈ C: η(x) ∧ η^{∗}(x) = x. Therefore, if x ∈ ρ(C) ⊆ C we have

x = η(x) ∧ η^{∗}(x)
= η(ρ(x)) ∧ η^{∗}(ρ(x))
= (ρ ⊔ η)(x) ∧ (ρ ⊔ η^{∗})(x)

Hence ρ = (ρ ⊔ η) ⊓ (ρ ⊔ η^{∗}), and by definition of pseudocomplementation in uco(ρ(C)): (ρ ⊔ η^{∗}) ⊑ ρ ⊖ (ρ ⊔ η).

Lemma 5.3. Let ρ, η ∈ uco(C). If η ⊔ η^{∗} = {⊤} and Mirr(ρ(C)∩η^{∗}(C)) ⊆ Mirr(ρ(C)) then ρ⊖(ρ⊔η) ⊑ (ρ⊔η^{∗}).

Proof. Because η ⊔η^{∗} = {⊤} then Mirr(ρ(C)∩η^{∗}(C))∩ η(C) = ∅. Therefore by Theorem 4.1 if Mirr(ρ(C)∩η^{∗}(C)) ⊆ Mirr(ρ(C)) then ρ ⊖ (ρ ⊔ η) ⊑ (ρ ⊔ η^{∗}).

Lemma 5.4. Let ρ, η ∈ uco(C). If ρ ∘ η = η ∘ ρ and η ⊔ η^{∗} = {⊤} then ρ ∘ η^{∗} = η^{∗} ∘ ρ.

Proof. For any x ∈ C we have:

ρ(η^{∗}(x)) = η(ρ(η^{∗}(x))) ∧ η^{∗}(ρ(η^{∗}(x)))
= ρ(η(η^{∗}(x))) ∧ η^{∗}(ρ(η^{∗}(x)))
= ⊤ ∧ η^{∗}(ρ(η^{∗}(x)))
= η^{∗}(ρ(η^{∗}(x)))

Therefore, ρ(η^{∗}(x)) = ρ(η^{∗}(ρ(η^{∗}(x)))), namely ρ ∘ η^{∗} is monotone, idempotent and extensive, i.e., ρ ∘ η^{∗} ∈ uco(C) which is true iff ρ ∘ η^{∗} = η^{∗} ∘ ρ.

It is worth noting that the structure of meet-irreducible elements is not always preserved by abstraction. This is a consequence of the structure of abstract domains which are Moore families: ρ(Mirr(C)) ⊆ Mirr(ρ(C)) and the inverse inclusion does not hold in general, as shown in Example 5.1. The following result gives two sufficient conditions such that ρ commutes with ⊖. These conditions are both formulated in terms of the structure of the meet-irreducible elements of abstract domains.

Theorem 5.5. Let ρ, η ∈ uco(C) such that ρ ∘ η = η ∘ ρ.

(i) If η ⊔η^{∗} = {⊤} and Mirr(ρ(C)∩η^{∗}(C)) ⊆ Mirr(ρ(C)) then ρ(C ⊖ η(C)) = ρ(C) ⊖ ρ(η(C)).

(ii) If Mirr(ρ(C)) = ρ(Mirr(C)) then ρ(C ⊖ η(C)) = ρ(C) ⊖ ρ(η(C)).

Proof. (i). Immediate by Lemma 5.2, 5.3, and 5.4. (ii). We prove ρ(Mirr(C))∖ρ(η(C)) = ρ(Mirr(C)∖η(C)). We know that for any function f: f(A)∖f(B) ⊆ f(A∖B) so the inclusion ⊆ is valid. We now prove that:

x ∈ ρ(Mirr(C)∖η(C)) ⇒ x ∉ ρ(η(C))

Because ρ ∘ η = η ∘ ρ:

x ∈ ρ(η(C)) ⇒ x ∈ η(C) ⇒ x ∉ Mirr(C)∖η(C) ⇒ x = ρ(x) ∉ ρ(Mirr(C)∖η(C)).

Indeed, if x ∈ ρ(Mirr(C)∖η(C)) then x ∈ Mirr(C)∖η(C) which is absurd because x ∈ ρ(C)∩η(C). Moreover we have ρ(Mirr(C)∖η(C)) ⊆ ρ(Mirr(C)) and this fact together with what we proved above implies that

ρ(Mirr(C)∖η(C)) ⊆ ρ(Mirr(C))∖ρ(η(C))

So we have the equality. By the argument above this implies the following equalities:

Mirr(ρ(C) ⊖ ρ(η(C))) = Mirr(ρ(C))∖ρ(η(C))
= ρ(Mirr(C))∖ρ(η(C))
= ρ(Mirr(C)∖η(C))

from which follows the thesis.

The following example shows that the converse of Theorem 5.5-(ii) does not hold in general.

Example 5.6. Let Sign and ρ(Sign) = Nzero be the domains in Fig. 3 for sign and non-zero analysis of integer variables. If η(Sign) = {ℤ, 0−, −} then ρ(η(Sign)) = {ℤ, −}. In this case we have that ρ(Sign ⊖ η(Sign)) = ρ({ℤ, 0+, ≠ 0, +}) = {ℤ, ≠ 0, +} = Nzero ⊖ {ℤ, −} while ρ(Mirr(Sign)) = {≠ 0} and Mirr(Nzero) = {≠ 0, +, −}.

6. COMPLEMENTING SEMANTICS

In order to better understand how complementation factorizes a semantics, we need to characterize the reduced product of semantics. Let P rogram be the collection of all well-formed programs in a programming language. If C is some domain, e.g. execution traces, functions, sets of states, etc. ([8]), and [[·]] : P rogram → C is the semantics assigning with each program P ∈ P rogram its meaning in C, then for any ρ ∈ uco(C): [[·]]_{ρ} : P rogram → ρ(C) is the so called abstract semantics, and it is [[P]]_{ρ} =^{def} ρ([[P]]). The following result [20] formally expresses the intuition that the reduced product semantics corresponds precisely to the logical conjunction of the observables associated with each semantics in the product.

Theorem 6.1. If P, Q ∈ P rogram and {A_{i}}_{i∈I} ⊆ uco(C) then [[P]]_{⊓_{i∈I} A_{i}} = [[Q]]_{⊓_{i∈I} A_{i}} iff ∀i ∈ I. [[P]]_{A_{i}} = [[Q]]_{A_{i}}.

Proof. Assume that P, Q ∈ P rogram. (⇒) Assume that k ∈ I. Since ⊓_{i∈I}ρ_{i} ⊑ ρ_{k}, then we have [[P]]_{ρ_{k}} = [[Q]]_{ρ_{k}}, as desired. (⇐) Since ∀i ∈ I. ρ_{i}([[P]]) = ρ_{i}([[Q]]), we have ∧_{i∈I}ρ_{i}([[P]]) = ∧_{i∈I}ρ_{i}([[Q]]) which proves the thesis.

Therefore, given any two semantics X, A ∈ uco(C), such that X ⊑ A, the complement semantics [[·]]_{(X⊖A)} is the most abstract semantics such that [[P]]_{X} = [[Q]]_{X} iff [[P]]_{A} = [[Q]]_{A} and [[P]]_{(X⊖A)} = [[Q]]_{(X⊖A)}. In practice it is always possible to define complements of semantics, since the hypothesis in Theorem 4.1 and 4.1 assuring their existence are extremely weak. In most cases in fact the domain of interpretation is a continuous or even algebraic lattice, or it is generated by its meet-irreducible elements.

6.1 Complementing trace-based semantics

In this section we prove that angelic and demonic semantics provide a conjunctive decomposition of natural semantics, and that angelic and infinite semantics form a minimal (most abstract) decomposition of natural semantics. This is now proved for the basic operational trace-based semantics only, which represents the bottom (most concrete) semantics in Cousot’s hierarchy, see Fig. 1. We will generalize this construction to the whole hierachy in Sec. 6.2.

We consider the angelic/demonic/infinite closure operators on generic traces Ang, Dem, Inf ∈ uco(℘(Σ ∞), ⊆) induced by, respectively, the angelic, demonic, and infinite abstractions of trace semantics: Ang =^{def} γ^{+}∘α^{+}, Dem =^{def} γ^{∂}∘α^{∂}, and Inf =^{def} γ^{ω} ∘ α^{ω}. It is immediate to observe that for any X ∈ Σ ∞:

Ang(X) = X ∪ Σω⃗
Dem(X) = X ∪ \{ σ ∈ Σ+ | \begin{matrix}δ ∈ X ∩ Σω⃗ \\ δ_{0} = σ_{0} \end{matrix} \}
Inf (X) = X ∪ Σ+

We first consider the relational abstraction given by the closure ρ^{r} =^{def} γ^{r} ∘ α^{r} (see Table 1) which is the following function:

ρ^{r}(X) = \{ σ ∈ Σ ∞ | \begin{matrix}δ ∈ X, δ_{0} = σ_{0} \\ |δ| = n < ω ⇒ |σ| = k < ω ∧ \\ σ_{k−1} = δ_{n−1} \\ |δ| = ω ⇒ |σ| = ω \end{matrix} \}

The relational semantics is ℛ = ρ^{r}(τ ∞). We observe that Mirr(⟨℘(A), ⊆⟩) = {X |∃a ∈ A.X = A∖{a}} and that ℘(A) is generated by its meet-irreducibles. We have the following results relating angelic, demonic, infinite and relational semantics.

Lemma 6.2. Let σ ∈ Σ+ and δ ∈ Σω⃗. Then we have

Σ ∞ \ {σ} ∈ Ang  Σ ∞ \ {δ} ∉ Ang
Σ ∞ \ {σ} ∉ Dem  Σ ∞ \ {δ} ∈ Dem

Proof. It is immediate by definition that if σ ∈ Σ+ and δ ∈ Σω⃗ then: Ang(Σ ∞ \{σ}) = (Σ ∞ \{σ})∪Σω⃗ = Σ ∞ \{σ}, Ang(Σ ∞ \ {δ}) = (Σ ∞ \ {δ}) ∪ Σω⃗ = Σ ∞. The case for Dem is analogous.

The following proposition is immediate by Lemma 6.2 and Theorem 4.1.

Proposition 6.3. Dem^{∗} = Ang.

However, angelic and demonic abstractions do not factorize natural semantics in most abstract factors. In fact, while the complement of demonic semantics is angelic, the converse does not hold. It is worth noting that Ang^{∗} ≠ Dem. In particular, for any finite trace σ ∈ Σ+, Dem({σ}) = {σ} while Ang^{∗}({σ}) = Σ+ ⊃ {σ}.

Proposition 6.4. Ang^{∗} = Inf and Inf^{∗} = Ang.

Proof. Ang^{∗} = ℳ(Mirr(℘(Σ ∞)) ∖ Ang). Therefore we have that X ∈ Mirr(Ang^{∗}) iff there exists δ ∈ Σω⃗ such that X = Σ ∞ ∖{δ} = Σ+ ∪(Σω⃗ ∖{δ}). It is immediate therefore that X ∈ Ang^{∗} iff X = X ∪ Σ+, namely Ang^{∗} = Inf . The proof for Inf^{∗} = Ang is analogous.

It is worth noting that demonic semantics can be further factorized by the infinite one, namely Dem ⊖ Inf ≠ Dem.

Lemma 6.5.

Mirr(Dem) = Mirr(Inf ) ∪

\{ X ⊆ Σ ∞ | \begin{matrix}∃σ ∈ Σ+ . X = Σ ∞ ∖ (Δ_{σ} ∪ \{σ\}), \\ Δ_{σ} = \{δ ∈ Σω⃗ | δ_{0} = σ_{0}\} \end{matrix} \}

Proof. We denote Mirr(Dem) by M and we prove the two directions of the equality separately. In the following if X ⊆ Σ ∞ then X^{+} =^{def} X ∩ Σ+ and X^{ω} =^{def} X ∩ Σω⃗. We first prove that if X ∈ M then X is meet-irreducible in Dem. If X ∈ Mirr(Inf ) then it is immediate that X is meet-irreducible in Dem. Now, if X = Σ ∞ ∖ (Δ_{σ} ∪ {σ}) we have several cases. We can take A_{1}, A_{2} ∈ Dem such that A_{1} ∩ A_{2} = X, then we have that Σω⃗ ∖ Δ_{σ} ⊆ A_{i}^{ω}, and Σ+ ∖ {σ} ⊆ A_{i}^{+}, for i = 1, 2. So we have only these possible cases : A_{i}^{ω} = Σω⃗ ∖ Δ_{σ}, A_{i}^{ω} = Σω⃗ ∖ Δ_{0} where Δ_{0} ⊂ Δ_{σ} or A_{i}^{ω} = Σω⃗; on the other hand we have A_{i}^{+} = Σ+ ∖ {σ} or A_{i}^{+} = Σ+. Now we prove that in all these cases either A_{i} = X or we have an absurd. We consider A_{1}^{ω} = Σω⃗ ∖ Δ_{σ}. Then A_{1}^{+} = Σ+ (in the other case we have A_{1} = X) and we see what happens for A_{2}. A_{2}^{+} = Σ+∖{σ}, otherwise we have A_{1} ∩ A_{2} ≠ X, so if A_{2}^{ω} = Σω⃗ ∖ Δ_{σ} then we have A_{2} = X. Moreover if A_{2}^{ω} = Σω⃗ or A_{2}^{ω} = Σω⃗ ∖ Δ_{0} then A_{2} ∉ Dem. Now we consider A_{1}^{ω} = Σω⃗. Then A_{1}^{+} = Σ+ (in the other case A_{1} ∉ Dem) and we see what happens for A_{2}. If A_{2}^{ω} = Σω⃗ or A_{2}^{+} = Σ+, we have an absurd because A_{1} ∩ A_{2} ≠ X. So we consider A_{2}^{+} = Σ+ ∖ {σ} and if A_{2}^{ω} = Σω⃗ ∖ Δ_{σ} then A_{2} = X, else if A_{2}^{ω} = Σω⃗ ∖ Δ_{0} then A_{2} ∉ Dem. Finally we consider A_{1}^{ω} = Σω⃗ ∖ Δ_{0}. We have A_{1}^{+} = Σ+, otherwise A_{1} ∉ Dem. Then A_{2}^{+} = Σ+ ∖ {σ}, otherwise A_{1} ∩ A_{2} ≠ X. Moreover, if A_{2}^{ω} = Σω⃗ then A_{1}∩A_{2} ∉ Dem, if A_{2}^{ω} = Σω⃗ ∖Δ_{0} then A_{1} ∩ A_{2} ≠ X, and if A_{2}^{ω} = Σω⃗ ∖ Δ_{σ} then A_{2} = X. Now we have to prove that if X is meet-irreducible then it belongs to M. We suppose that X ∉ M. Then there exists D_{0} ⊆ Σω⃗ with D_{0} ⊃ Δ_{σ} such that X^{ω} = Σω⃗ ∖ D_{0} or there exists D_{1} ⊆ Σ+ with |D_{1}| > 1 such that X^{+} = Σ+ ∖ D_{1} or X ∉ Mirr(Inf ). Now we distinguish two cases; if X^{+} = Σ+ then we have to prove that X ∈ Mirr(Inf ) and this is immediate. So we consider X^{+} ⊂ Σ+. Now we consider X^{+} = Σ+ ∖ D_{1} and we define D′_{1} =^{def} D_{1} ∖ {σ′},

with σ′ ∈ D_{1}. Then we can take A = X^{ω} ∪ (Σ+ ∖ D′_{1}) and B = X^{ω} ∪ (Σ+ ∖ {σ′}). In this case A ∩ B = X but A ≠ X and B ≠ X, which is absurd. So X^{+} = Σ+ ∖ {σ}. Now we consider X^{ω} = Σω⃗ ∖ D_{0}, we define D′_{0} =^{def} D_{0} ∖ {δ′} with δ′ ∉ Δ_{σ} and δ′ ∈ D_{0}. Then we can take A = Σ ∞∖(D′_{0}∪{σ}) while B = Σ ∞∖{δ′}, so we have that A∩B = X but A ≠ X and B ≠ X, which is absurd.

The following closure operator, here called pseudo-demonic, characterizes the new complementary semantics defined by Dem ⊖ Inf : Dem^{ϱ} ∈ uco(Dem(℘(Σ ∞))) such that

Dem^{ϱ} =^{def} λX . X ∪ { δ ∈ Σω⃗ | chaos(δ) ⊆ X^{+} }

The idea here is that this new semantics is unable to distinguish whether a chaotic set of traces is a consequence of the existence of an infinite trace in τ ∞. This abstraction is achieved by enhancing any set of traces X with all the infinite traces δ ∈ Σω⃗ whenever the chaos generated by δ, namely chaos(δ) =^{def} {σ ∈ Σ+ | σ_{0} = δ_{0}}, is contained in X.

The following result is straightforward by Theorem 4.1 and by Lemma 6.5. As expected, this new semantics which is Dem^{ϱ}(Dem(τ ∞)) is unable to observe infinite behavior, as well as in the angelic case, whenever chaotic information is computed in τ ∞. In particular (Dem ⊖ Inf ) ∘ Dem is unable to factorize the basic trace semantics. Indeed, for any X ∈ Mirr(℘(Σ ∞)) we have (Dem ⊖ Inf )(Dem(X)) = Σ ∞.

Theorem 6.6. Dem ⊖Inf = Dem^{ϱ}, Dem ⊖Dem^{ϱ} = Inf , and (Dem^{ϱ} ∘ Dem)^{∗} = λx. x.

The angelic abstraction is fully complementary with respect to infinite and demonic ones, namely they share only the top element in ℘(Σ ∞) which is the set of all sequences Σ ∞.

Proposition 6.7. Ang ⊔ Dem = Ang ⊔ Inf = Dem^{ϱ} ⊔ Inf = Σ ∞.

In order to characterize the symmetric structure of the observables at the level of trace-based and relational semantics we consider Theorem 5.5, and we prove that angelic, demonic, pseudo-demonic, and infinite abstractions all provide commuting closures with respect to the relational abstraction.

Proposition 6.8.

1. ρ^{r} ∘ Ang = Ang ∘ ρ^{r}

2. ρ^{r} ∘ Dem = Dem ∘ ρ^{r}

3. ρ^{r} ∘ Inf = Inf ∘ ρ^{r}

4. ρ^{r} ∘ Dem^{ϱ} = Dem^{ϱ} ∘ ρ^{r}

Proof. It is easy to prove that ρ^{r} is additive. Therefore

ρ^{r}(Ang(X)) = ρ^{r}(X ∪ Σω⃗)
= ρ^{r}(X) ∪ ρ^{r}(Σω⃗)
= ρ^{r}(X) ∪ Σω⃗
= Ang(ρ^{r}(X)).

We prove that ρ^{r} ∘ Dem = Dem ∘ ρ^{r}. By definition and additivity of ρ^{r} we have ρ^{r}(Dem(X)) = ρ^{r}(X) ∪ ρ^{r}({σ ∈ Σ+|δ ∈ X ∩ Σω⃗, δ_{0} = σ_{0}}) and Dem(ρ^{r}(X)) = ρ^{r}(X) ∪ {σ ∈ Σ+|δ ∈ ρ^{r}(X) ∩ Σω⃗, δ_{0} = σ_{0}}. Note that θ ∈ ρ^{r}({σ ∈ Σ+|δ ∈ X ∩ Σω⃗, δ_{0} = σ_{0}}) iff θ ∈ Σ+, σ ∈ Σ+, δ ∈ X ∩ Σω⃗, and δ_{0} = σ_{0}, σ_{0} = θ_{0} and θ_{n−1} = σ_{k−1}, with |θ| = n and |σ| = k. Therefore θ ∈ {σ ∈ Σ+|δ ∈ X ∩ Σω⃗, δ_{0} = σ_{0}}. This implies that ρ^{r}({σ ∈ Σ+|δ ∈ X ∩ Σω⃗, δ_{0} = σ_{0}}) = {σ ∈ Σ+|δ ∈ X ∩ Σω⃗, δ_{0} = σ_{0}}. Moreover if θ is such that δ ∈ ρ^{r}(X) ∩ Σω⃗ and δ_{0} = θ_{0}, then by definition of ρ^{r}, there exists δ′ ∈ X ∩ Σω⃗ such that δ_{0} = δ′_{0} = θ_{0}. This implies that θ ∈ ρ^{r}({σ ∈ Σ+|δ ∈ X ∩ Σω⃗, δ_{0} = σ_{0}}) iff θ ∈ {σ ∈ Σ+|δ ∈ ρ^{r}(X) ∩ Σω⃗, δ_{0} = σ_{0}}. The equality ρ^{r} ∘ Inf = Inf ∘ ρ^{r} follows by Lemma 5.4. The case for Dem^{ϱ} is analogous because ρ^{r}({δ ∈ Σω⃗ | chaos(δ) ⊆ X}) = {δ ∈ Σω⃗ | chaos(δ) ⊆ ρ^{r}(X)}.

It is worth noting that the relational semantics does not factorize the trace-based one, being too abstract, i.e., (ρ^{r})^{∗} = λx.x or equivalently τ ∞ ⊖ ℛ = τ ∞. This does not allows us to the use Theorem 5.5-(ii) for relating the observables at the level of trace-based and relational semantics styles in Cousot’s hierarchy. Instead we can use Theorem 5.5-(i), as shown below.

Proposition 6.9.

1. Mirr(ρ^{r}(℘(Σ ∞)) ∩ Ang(℘(Σ ∞))) ⊆ Mirr(ρ^{r}(℘(Σ ∞)))

2. Mirr(ρ^{r}(℘(Σ ∞)) ∩ Inf (℘(Σ ∞))) ⊆ Mirr(ρ^{r}(℘(Σ ∞)))

3. Mirr(ρ^{r}(Dem(℘(Σ ∞))) ∩ Dem^{ϱ}(℘(Σ ∞))) ⊆ Mirr(ρ^{r}(Dem(℘(Σ ∞))))

Therefore, it is immediate by Theorem 5.5-(i) that:

ℛ = Ang(ℛ) ⊓ Dem(ℛ) = Ang(ℛ) ⊓ Inf (ℛ)
Dem(ℛ) = Dem^{ϱ}(ℛ) ⊓ Inf (ℛ)
Inf (ℛ) = Dem(ℛ) ⊖ Dem^{ϱ}(ℛ)
Dem^{ϱ}(ℛ) = Dem(ℛ) ⊖ Inf (ℛ)
Inf (ℛ) = ℛ ⊖ Ang(ℛ)
Ang(ℛ) = ℛ ⊖ Dem(ℛ).

6.2 Complementing all over the hierarchy

In this section we prove that the basic pattern of observables given by angelic, demonic, pseudo-demonic, and infinite can always be characterized by domain complementation for any semantics style in Cousot’s hierarchy. The following lemma characterizes the meet-irreducible elements in natural nondeterministic denotational semantics 𝒟. This semantics is isomorphic to the basic natural relational semantics ℛ [8].

Lemma 6.10.

Mirr(Σ ⟶ ℘(Σ_{⊥}), ⊑) =

= \{ f | \begin{matrix}∃\overline{s} ∈ Σ, ∃s′ ∈ Σ_{⊥} . f(\overline{s}) = Σ_{⊥}∖\{s′\} ∧ \\ ∀s ∈ Σ∖\{\overline{s}\} . f(s) = Σ_{⊥} \end{matrix} \}

Proof. Let A and B be sets. We prove the two implications of the equality separately.

(⇒) Let f be a meet-irreducible element in A ⟶ ℘(B), then for all g, h ∈ A ⟶ ℘(B) we have that if f = g ⊓ h then either g = f or h = f. Assume f ∉ M. By definition of M, this implies that either (1) ∃\overline{a} ∈ A . f(\overline{a}) = B∖D, |D| > 1 or (2)∃a ≠ \overline{a} . f(s) ⊂ B. We consider the two cases separately

(1) Let b_{0} ∈ D and D_{0} = D ∖{b_{0}} with |D_{0}| ≥ 1, then we can define the functions

h(a) = \{ \begin{matrix}f(a) & if a ≠ \overline{a} \\ B∖\{b_{0}\} & otherwise \end{matrix}

g(a) = \{ \begin{matrix}f(a) & if a ≠ \overline{a} \\ B∖D_{0} & otherwise \end{matrix}

Note that f ⊏ h and f ⊏ g because f(\overline{a}) ⊂ h(\overline{a}) and f(\overline{a}) ⊂ g(\overline{a}), while for the other elements the functions coincide. This implies that f ⊑ h ⊓ g. We prove the other inclusion. Foe each a ≠ \overline{a} we have that h(a) = g(a) = f(a); in particular f(a) = h(a) ∩ g(a), while h(\overline{a}) = B ∖ \{b_{0}\} and g(\overline{a}) = B∖D_{0}. Therefore h(\overline{a}) ∩ g(\overline{a}) = B∖(D_{0} ∪ \{b_{0}\}) = B ∖D = f(\overline{a}). Hence for all a ∈ A we have that f(a) = h(a) ∩ g(a), with f ≠ h and f ≠ g, but this is absurd from the hypothesis.

(2) Let \overline{a} ∈ A such that f(\overline{a}) = B ∖ \{b\}, and let a_{0} ∈ A∖\{\overline{a}\} such that f(a_{0}) ⊂ B. If f(a_{0}) = B∖D with |D| > 1 then we fall into the previous case; therefore f(a_{0}) = B ∖{b_{0}}. We define the following functions

h(a) = \{ \begin{matrix}f(a) & if a ≠ \overline{a} \\ B & otherwise \end{matrix}

g(a) = \{ \begin{matrix}f(a) & if a ≠ a_{0} \\ B & otherwise \end{matrix}

In this case we have that f ⊏ g and f ⊏ h because f(\overline{a}) ⊂ B and f(a_{0}) ⊂ B. Observe that for each a ≠ \overline{a}, a_{0} we have f(a) = g(a) = h(a) = g(a) ∩ h(a); while f(\overline{a}) = g(\overline{a}) ⊂ h(\overline{a}) and therefore g(\overline{a}) ∩ h(\overline{a}) = g(\overline{a}) = f(\overline{a}). In the same way f(a_{0}) = h(a_{0}) ⊂ g(a_{0}) and therefore g(a_{0}) ∩ h(a_{0}) = h(a_{0}) = f(a_{0}). So for all a ∈ A we have f(a) = g(a) ∩ h(a) but f ≠ g and f ≠ h, and this is absurd from the hypothesis.

(⇐) Let f ∈ M. Then there exists \overline{a} ∈ A and b ∈ B such that f(\overline{a}) = B∖\{b\}. Let g and h be such that f = g⊓h. Then ∀a ∈ A . f(a) = g(a) ∩ h(a). This means that ∀a ∈ A . f(a) ⊆ g(a) and ∀a ∈ A . f(a) ⊆ h(a). We know that if a ≠ \overline{a} then f(a) = B ⊆ g(a), but this implies that for these a’s, g(a) = B. In the same way we can say that for these a’s, h(a) = B. We consider now \overline{a}. Then we have:

g(\overline{a}) ⊇ B∖\{b\} ⇒ if g(\overline{a}) = B∖\{b\} then g = f if h(\overline{a}) = B then g(\overline{a}) ∩ h(\overline{a}) = B ≠ f(\overline{a})

which is absurd. So h(\overline{a}) = B∖\{b\} and then h = f. All these facts together mean that f is meet-irreducible.

This concludes the proof.

The following result proves that all semantics in Cousot’s hierarchy satisfy the hypothesis of Theorem 5.5-(ii). In the following we let Mirr_{ℛ} =^{def} Mirr(⟨℘(Σ × Σ_{⊥}), ⊆⟩).

Lemma 6.11.

Mirr(⟨Σ ⟶ ℘(Σ_{⊥}), ⊑⟩)  =  α^{▶}(Mirr_{ℛ} )
Mirr(⟨℘(Σ_{⊥})⟶^{coa}℘(Σ), ⊒⟩) =  α^{gwp}(α^{▶}(Mirr_{ℛ} ))
Mirr(⟨℘(Σ) ⊗ ℘(Σ_{⊥}), ⊇⟩) = α^{gH}(α^{gwp}(α^{▶}(Mirr_{ℛ} )))

Proof. We just prove that Mirr(⟨Σ ⟶ ℘(Σ_{⊥}), ⊑⟩) = α^{▶}(Mirr_{ℛ} ). We know that α^{▶}(X) = λs.{s′ |⟨s, s′⟩ ∈ X}. Now we prove the two implications of the equality separately. Let X ∈ Mirr_{ℛ} then

α^{▶}(X) = α^{▶}((Σ × Σ_{⊥})∖{⟨s_{0}, s_{1}⟩})
= \{ \begin{matrix}λs.Σ_{⊥} & if s ≠ s_{0} \\ λs.Σ_{⊥}∖\{s_{1}\} & otherwise \end{matrix}

But this implies that α^{▶}(X) ∈ Mirr(⟨Σ ⟶ ℘(Σ_{⊥}), ⊑⟩). Let now f ∈ Mirr(⟨Σ ⟶ ℘(Σ_{⊥}), ⊑⟩) then it exists s_{0} ∈ Σ and s_{1} ∈ Σ_{⊥} such that f(s_{0}) = Σ_{⊥}∖{s_{1}} and for all s ≠ s_{0} we have f(s) = Σ_{⊥}. Then we can take X = Σ × Σ_{⊥} ∖ {⟨s_{0}, s_{1}⟩} ∈ Mirr_{ℛ} such that f = α^{▶}(X).

The lemma above together with Theorem 5.5-(ii) implies the following result relating program semantics at different levels of abstraction, see Fig. 1. In this case we extend the scope of ⊖ from closures to semantics in the obvious way: Let 𝒜 = ρ^{𝒜} (τ ∞) and ℬ = η^{ℬ} (τ ∞) then 𝒜⊖ℬ = (ρ⊖η)(τ ∞). The semantics not originally included in Cousot’s hierarchy are represented in Fig. 1 with dashed lines and empty points.

Theorem 6.12. In Cousot’s hierarchy of semantics we have τ ∞⊖τ + = τ ω⃗ and τ ∞⊖τ ω⃗ = τ ∞⊖τ ∂ = τ +. Moreover:

ℛ ⊖ ℛ^{+} = ℛ^{ω}  𝒟 ⊖ 𝒟^{+} = 𝒟^{ω}
ℛ ⊖ ℛ^{∂} = ℛ ⊖ ℛ^{ω} = ℛ^{+}  𝒟 ⊖ 𝒟^{∂} = 𝒟 ⊖ 𝒟^{ω} = 𝒟^{+}
ℛ^{∂} ⊖ ℛ^{ϱ} = ℛ^{ω}  𝒟^{∂} ⊖ 𝒟^{ϱ} = 𝒟^{ω}
ℛ^{∂} ⊖ ℛ^{ω} = ℛ^{ϱ}  𝒟^{∂} ⊖ 𝒟^{ω} = 𝒟^{ϱ}
gwp ⊖ wlp = wp^{ω}  gℋ ⊖ pℋ = tℋ ^{ω}
gwp ⊖ wp = gwp ⊖ wp^{ω} = wlp gℋ ⊖ tℋ = gℋ ⊖ tℋ ^{ω} = pℋ
wp ⊖ wp^{ϱ} = wp^{ω}  tℋ ⊖ tℋ ^{ϱ} = tℋ ^{ω}
wp ⊖ wp^{ω} = wp^{ϱ}  tℋ ⊖ tℋ ^{ω} = tℋ ^{ϱ}

6.3 Complements in the computational order

We consider here the lifted computational order ⊑^{∞} on the trace-based semantics ℘(Σ ∞). We prove that most of the above results still hold for the computational order ⊑^{∞}, therefore they can be used to characterize complementary semantics defined by combining both inductive and co-induc-tive definitions. In this case it is possible to characterize the complement of the angelic relational semantics which is again the infinite relational semantics and, conversely, the complement of the infinite semantics which is the angelic one. This is not the case for the demonic semantics which is not an upper closure operator on ⟨℘(Σ ∞), ⊑^{∞}⟩, (cf. [8]).

Theorem 6.13. Let M_{Σ} =^{def} {Σ+ ∪ {δ} | δ ∈ Σω⃗}, then

Mirr(⟨℘(Σ ∞), ⊑^{∞}⟩) = Mirr(⟨℘(Σ+), ⊆⟩) ∪ M_{Σ}.

Proof. We prove the two directions of the equality separately. We first prove that if X ∈ Mirr(℘(Σ+)) ∪ M_{Σ} then X is irreducible in ⟨℘(Σ ∞), ⊑^{∞}⟩. If X ∈ Mirr(℘(Σ+)) then it is irreducible in ⟨℘(Σ ∞), ⊑^{∞}⟩ because it is irreducible in ℘(Σ+) and by definition of ⊑^{∞} it cannot be obtained as glb of sets containing infinite traces. Indeed let X = A ⊓^{∞} B, with A, B ⊆ Σ ∞ and suppose that there exists δ ∈ A^{ω}. Then X ⊑^{∞} A and this fact implies that X^{+} ⊆ A^{+} and X^{ω} ⊇ A^{ω}. This last relation says that δ ∈ X^{ω}, but this is absurd because X ∈ ℘(Σ+) and so X^{ω} = ∅. Assume that X ∈ M_{Σ}, i.e., X = Σ+ ∪ {δ} for some δ ∈ Σω⃗, and let A and B be as above, such that A ⊓^{∞} B = X. By definition of glb X ⊑^{∞} A, B and for each Y such that Y ⊑^{∞} A, B then Y ⊑^{∞} X. So X ⊑^{∞} A, which means that Σ+ ⊆ A^{+}, and this implies that A^{+} = Σ+. On the other hand {δ} ⊇ A^{ω} so A^{ω} = ∅ or A^{ω} = {δ}. Then if A^{ω} = {δ} it is obvious that A = X. We now suppose that A^{ω} = ∅. Then we can do the same reasoning about B and so we can say that B^{ω} = ∅ or B^{ω} = {δ}. If also B^{ω} = ∅, then A = B = Σ+ which means that A⊓^{∞}B = A = Σ+ ≠ X, but this is absurd for the hypothesis made. Therefore if A^{ω} = ∅ then B is such that B^{ω} = {δ}, and in this way we have that B = X, proving that X is meet-irreducible. We now prove that if X is meet-irreducible then we have X ∈ Mirr(℘(Σ+)) ∪ M_{Σ}. We suppose that X ∉ Mirr(℘(Σ+)) ∪ M_{Σ}, i.e., X ∉ Mirr(℘(Σ+)) and X ∉ M_{Σ}. If X^{ω} = ∅ then X ⊆ Σ+ and from the hypothesis of irreducibility of X, X belongs to Mirr(℘(Σ+)), but this is absurd from the hypothesis made. Therefore let X = X^{+} ∪ X^{ω} be such that X^{ω} ≠ ∅. Because X ∉ M_{Σ} then we have that either X^{+} ⊂ Σ+ or |X^{ω}| > 1.

• Assume X^{+} ⊂ Σ+ then we can take A =^{def} X^{+} ⊐^{∞} X

which holds because X^{ω} ⊃ ∅; and B =^{def} Σ+ ∪ X^{ω} ⊐^{∞}

X which is true because X^{+} ⊂ Σ+. Then X ⊑^{∞} A and X ⊑^{∞} B. We prove that X is the glb of A and B. Let Y ⊑^{∞} A, B, then Y^{+} ⊆ A^{+} = A = X^{+} and Y^{ω} ⊇ B^{ω} = X^{ω}, so Y ⊑^{∞} X, then by definition of glb X = A ⊓^{∞} B, but X ≠ A and X ≠ B. The result is absurd for the hypothesis made for X. So if X is meet-irreducible then X^{+} = Σ+.

• Let |X^{ω}| > 1 and let δ ∈ X^{ω} and D = X^{ω} ∖{δ} with D ≠ ∅. We take A =^{def} X^{+} ∪ {δ} ⊐^{∞} X which is true because X^{ω} ⊃ {δ}. Moreover we take B =^{def} X^{+}∪D ⊐^{∞} X which is true because X^{ω} ⊃ D. Then X ⊑^{∞} A and X ⊑^{∞} B. Let Y ⊑^{∞} A, B, then Y^{+} ⊆ A^{+} = X^{+}, Y^{ω} ⊇ A^{ω} = {δ} and Y^{ω} ⊇ B^{ω} = D. The last inequalities imply that Y^{ω} ⊇ D ∪ {δ} = X^{ω}, and therefore Y ⊑^{∞} X. As in the previous case, we have that X = A ⊓^{∞} B but X ≠ A and X ≠ B; which is absurd for the hypothesis on X. Therefore if X is meetirreducible then |X^{ω}| = 1.

Hence if X is meet-irreducible then X ∈ Mirr(℘(Σ+))∪M_{Σ}, which concludes the proof.

Cousot proved that α^{+} and γ̃^{+} =^{def} λx. x still define a Galois insertion between the natural trace-based semantics and its angelic counterpart under the lifted partial order ⊑^{∞}. This means that Ang^{∞} =^{def} α^{+} is a closure operator also in the computational order, i.e., Ang^{∞} ∈ uco(⟨℘(Σ ∞), ⊑^{∞}⟩). The same holds for Inf = γ^{ω} ∘ α^{ω} ∈ uco(⟨℘(Σ ∞), ⊑^{∞}⟩). In this case the pseudo-complement of Ang^{∞} and Inf coincide respectively with the pseudo-complement of the closure operator Ang and Inf with respect to the approximation order ⊆, and they still provide a most abstract factorization of the trace-based semantics which is perfectly symmetric all over Cousot’s hierarchy. Note that in the following all closure operators and constructions are considered in the complete lattice ⟨℘(Σ ∞), ⊑^{∞}, ⊓ ∞, ⊔ ∞, ⊓ ∞, Σ+, Σω⃗⟩. In particular (Ang^{∞})^{∗} = Ang^{∗} = Inf = ℳ(M_{Σ}), Inf^{∗} = Ang^{∞}, Ang^{∞} ⊔ Inf = Σ+, and ρ^{r} ∘ Ang^{∞} = Ang^{∞} ∘ ρ^{r}. Therefore, also Theorem 6.12 holds in the computational order ⊑^{∞} for angelic and infinite semantics.

Theorem 6.14. In Cousot’s hierarchy with computational order ⊑^{∞} we have τ ∞ ⊖τ + = τ ω⃗ and τ ∞ ⊖τ ω⃗ = τ +. Moreover we have:

ℛ ⊖ ℛ^{+} = ℛ^{ω}  𝒟 ⊖ 𝒟^{+} = 𝒟^{ω}
ℛ ⊖ ℛ^{ω} = ℛ^{+}  𝒟 ⊖ 𝒟^{ω} = 𝒟^{+}
gwp ⊖ wlp = wp^{ω}  gℋ ⊖ pℋ = tℋ ^{ω}
gwp ⊖ wp^{ω} = wlp  gℋ ⊖ tℋ ^{ω} = pℋ

7. AN EXAMPLE IN CCP

In this section we consider the case of concurrent constraint programming languages [28] and we derive its denotational closure-based [29] and axiomatic semantics [13] as an abstract interpretation of maximal traces of constraints in a transition system semantics. Concurrent constraint programming (ccp for short) is a well known concurrent programming paradigm where processes interacts through a common store [28]. This leads to a computational model based on the notion of store-as-constraint. The main features of a cc process is to refine the store (tellconstraints) or synchronize itself with other processes (askconstraints). The ask-tell paradigm, which is the basis of ccp languages, is an extension of constraint logic programming: In addition to satisfiability (tell), entailment (ask) is introduced. A store is a constraint representing the global state of the computation. Synchronization is achieved through blocking ask: A process is suspended when the store does not entail the ask constraint and it remains suspended until the store entails it. The constraint system represents the basic algebraic notion behind ccp. The construction in [29] is an extension of Scott’s partial information systems [1]. Informally, we have a denumerable set D of elementary assertions (containing distinct elements 1 and 0 representing the least informative assertion and the contradiction respectively) and a finite entailment relation ⊢⊆ ℘_{f} (D×D). A simple constraint system is Σ =^{def} ⟨℘(D), ⊣⟩/_{∼}, which is a complete ω-algebraic lattice [1] where X ∼ Y iff (X)^{⊣} = (Y)^{⊣}, being (X)^{⊣} the entailment closure of a set of assertions X. An arbitrary element of Σ is called a constraint. Compact elements are called finite constraints, since they are equivalent to a finite subset of D. In order to treat the hiding operator of the language, Saraswat et al. [29] introduce a family of unary operations called cylindrifications see [23]). Intuitively, given a constraint c, the cylindrification operation ∃_{x}(c) yields the constraint obtained by “projecting out” from c the information about the variable x. Diagonal elements (equational constraints between variables [23]) are considered as a way to provide parameter passing. Note that special variables (not accessible to the user) together with a suitable use of cylindrification and diagonal elements make variable renaming no longer needed [29].

Definition 7.1. A constraint system ⟨Σ, ⊢, false, true, ∧, V, ∃_{x}, d_{xy}⟩ is an algebraic structure where: ⟨Σ, ⊣⟩ is a simple constraint system, true = [1]_{∼} and false = [0]_{∼}, ∧ is the glb, V is a denumerable set of variables, and ∀x, y ∈ V, ∀c, c′ ∈ Σ, the operator ∃_{x} : Σ → Σ satisfies

1. c ⊢ ∃_{x}c

2. if c ⊢ c′ then ∃_{x}c ⊢ ∃_{x}c′

3. ∃_{x}(c ∧ ∃_{x}c′) = ∃_{x}c ∧ ∃_{x}c′

4. ∃_{x}(∃_{y}c) = ∃_{y}(∃_{x}c)

∀x, y, z ∈ V, ∀c ∈ Σ, the diagonal element d_{xy} satisfies

1. d_{xx} = true

2. if z ≠ x, y then d_{xy} = ∃_{z}(d_{xz} ∧ d_{zy})

3. if x ≠ y then d_{xy} ∧ ∃_{x}(c ∧ d_{xy}) ⊢ c

The semantic operators of concurrent constraint languages are: elementary actions (ask and tell), hiding (∃), parallel composition (∥), guarded nondeterministic choice (∑) and recursion. The semantics of ccp programs well fits into Cousot’s hierarchy being easily described as maximal consistent traces of a transition system, i.e., maximal traces ⟨A_{0}, c_{0}⟩ →_{𝒯} ⟨A_{1}, c_{1}⟩ →_{𝒯} … where A_{i} are agents and c_{i} ⊢ c_{i−1} are constraints. We denote by (Agent × Σ) ∞ ; Γ this set of traces. The standard syntax and transition-system semantics is in Table 2. The maximal-trace semantics of a ccp program P = D.A is immediately defined as the set of finite and infinite consistent traces of constraints generated from P in an initial store c ∈ Σ.

𝒪(D.A)(c) = \{δ ∈ (Agent × Σ) ∞ ; Γ | \begin{matrix}δ_{0} = ⟨A, c⟩, ∀i ∈ [0, |δ|) \\ δ_{i} ⟶_{𝒯} δ_{i+1} \end{matrix}\}

We define the maximal trace semantics of a ccp program P as follows [[P]] ∞ = β({ 𝒪(P)(c) | c ∈ Σ }), where the

Program ::= Dec . Agent
Dec  ::= ϵ
| p(x⃗) :− Agent . Dec
Agent  ::= tell(c)
| ∃x⃗.Agent
| Agent ∥ Agent
| ∑_{i=1}^{n} (ask(c_{i}) → Agent_{i})
| p(y⃗)

R1 ⟨tell(c) , σ⟩ ⟶_{𝒯} ⟨ϵ , σ ∧ c⟩
R2 \frac{σ ⊢ c_{i}}{⟨∑_{i=1}^{n} (ask(c_{i}) → A_{i}) , σ⟩ ⟶_{𝒯} ⟨A_{i} , σ⟩}

R3 \frac{⟨A , σ⟩ ⟶_{𝒯} ⟨A′ , σ′⟩}{\begin{matrix}⟨A∥B , σ⟩ ⟶_{𝒯} ⟨A′∥B , σ′⟩ \\ ⟨B∥A , σ⟩ ⟶_{𝒯} ⟨B∥A′ , σ′⟩ \end{matrix}}

R4 \frac{⟨A , d ∧ ∃x⃗σ⟩ ⟶_{𝒯} ⟨B , e⟩}{⟨∃(x⃗, d).A , σ⟩ ⟶_{𝒯} ⟨∃(x⃗, e).B , σ ∧ ∃x⃗e⟩}

R5 \frac{p(x⃗) :− A ∈ P}{⟨p(y⃗) , σ⟩ ⟶_{𝒯} ⟨∃(x⃗, d_{x⃗,y⃗}).A , σ⟩}

Table 2: The syntax and operational semantics of ccp

function β : ℘((Agent × Σ) ∞)⟶^{a}℘(Σ ∞) abstracts away the agent information from traces:

β(X) = { σ ∈ Σ ∞ | δ ∈ X, δ_{i} = ⟨A, σ_{i}⟩ } .

The following result characterizes both the closure-based denotational [29] and the predicate-transformer semantics of nondeterministic ccp programs P ∈ Program in [13] as abstract interpretations of the maximal trace semantics [[P]] ∞.

Theorem 7.2. Let P be a ccp program.

• [[P]]_{𝒟} =^{def} λX. ⋃ { α^{▶}(α^{r}([[P]] ∞))(c) | c ∈ X } is a linear continuous closure operator on Smith’s powerdomain ℘(Σ_{⊥}), with ⊥ representing divergence, and it corresponds to the denotational semantics in [29].

• [[P]]_{gwp} =^{def} λX. ⋃ { c | α^{▶}(α^{r}([[P]] ∞))(c) ⊆ X } =

α^{gwp}([[P]]_{𝒟} ) is a co-additive function on ℘(Σ_{⊥}) and its left adjoint function λX. ⋃ { [[P]]_{𝒟} (c) | c ∈ X } is the strongest-postcondition semantics in [13].

We close this section by considering examples of programs and their denotational semantics for the different observable behaviors corresponding to the different complementary semantics in Cousot’s hierarchy, namely the angelic, demonic, pseudo-demonic, and infinite semantics. These semantics are all abstractions of [[·]]_{𝒟} . Consider the following programs, where ask(true) → A is denoted A and the starting agent is underlined.

P : p(x) : − tell(x = 2) + q(x).

q(x) : − p(x). \underline{p(x)}

Q : p(x) : − tell(x = 2). \underline{p(x)}
U : p(x) : − tell(x = 1) + q(x).

q(x) : − p(x). \underline{p(x)}

It is immediate that [[P]]_{𝒟^{+}} = [[Q]]_{𝒟^{+}} and [[P]]_{𝒟^{∂}} ≠ [[Q]]_{𝒟^{∂}} , [[P]]_{𝒟^{ω}} ≠ [[Q]]_{𝒟^{ω}} , [[P]]_{𝒟^{ϱ}} ≠ [[Q]]_{𝒟^{ϱ}} . Moreover [[P]]_{𝒟^{+}} ≠ [[U]]_{𝒟^{+}} and [[P]]_{𝒟^{∂}} = [[U]]_{𝒟^{∂}} , [[P]]_{𝒟^{ω}} = [[U]]_{𝒟^{ω}} , [[P]]_{𝒟^{ϱ}} = [[U]]_{𝒟^{ϱ}} . As for the demonic, pseudo-demonic and infinite semantics are concerned, consider the following programs:

H : p(x) : − ask(x = 1) → q(x).
q(x) : − q(x). \underline{p(x)}
K : p(x) : − ask(x = 1) → q(x) +
ask(x > 1) → tell(y = 2 ∗ x).
q(x) : − q(x). \underline{p(x)}

In this case [[H]]_{𝒟^{ω}} = [[K]]_{𝒟^{ω}} but [[H]]_{𝒟^{∂}} ≠ [[K]]_{𝒟^{∂}} . Moreover, if we assume that Σ is a finite domain FD constraint system (see [24]), and A is a terminating agent that, given c ∈ Σ, generates all the c′ ∈ Σ such that c′ ⊢ c, then we have:

\begin{matrix}G : & p(x) : − p(x) + A. \underline{p(x)} \\ R : & p(x) : − A. \underline{p(x)} \end{matrix}

and [[G]]_{𝒟^{ϱ}} = [[R]]_{𝒟^{ϱ}} but [[G]]_{𝒟^{∂}} ≠ [[R]]_{𝒟^{∂}} .

8. CONCLUSION

We have shown that complementary semantics of transition systems in Cousot’s hierarchy of semantics can be systematically constructed by domain complementation in abstract interpretation. This provides both a better insight on semantics designed for characterizing complementary observable properties of programs and the possibility to decompose semantics into most abstract factors involving possibly new semantics (e.g. the pseudo-demonic semantics). We think that other operations for domain construction in abstract interpretation can be used for the systematic derivation of semantics in Cousot’s hierarchy. In particular, the compositional denotational semantics of a programming language seems to correspond to the reduced power [11, 22] of the non compositional inevitable termination semantics in [8].

9. REFERENCES

[1] S. Abramsky and A. Jung. Domain theory. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 3, pages 1–168. Clarendon Press, Oxford, U.K., 1994.

[2] B. Alpern and F. B. Schneider. Recognizing safety and liveness. Distributed Comp., 2:117–126, 1987.

[3] K. R. Apt and G. D. Plotkin. Countable nondeterminism and random assignment. J. ACM, 33(4):724–767, 1986.

[4] G. Birkhoff. Lattice Theory. AMS Colloquium Publication, 3rd edition. AMS, Providence, RI, 1967.

[5] M. Comini and G. Levi. An algebraic theory of observables. In M. Bruynooghe, editor, Proc. of the 1994 Internat. Logic Programming Symp. (ILPS ’94), pages 172–186. The MIT Press, Cambridge, Mass., 1994.

[6] A. Cortesi, G. Filé, R. Giacobazzi, C. Palamidessi, and F. Ranzato. Complementation in abstract interpretation. ACM Trans. Program. Lang. Syst., 19(1):7–47, 1997.

[7] P. Cousot. Abstract interpretation. ACM Comput. Surv., 28(2):324–328, 1996.

[8] P. Cousot. Constructive design of a hierarchy of semantics of a transition system by abstract interpretation (Invited Paper). In S. Brookes and M. Mislove, editors, Proc. of the 13th Internat. Symp. on Mathematical Foundations of Programming Semantics (MFPS ’97), volume 6 of Electronic Notes in Theoretical Computer Science. Elsevier, Amsterdam, 1997. URL: http://www.elsevier.nl/locate/entcs/volume6.html, 25 pages, extended version to appear in Theor. Comput. Sci.

[9] P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the 4th ACM Symp. on Principles of Programming Languages (POPL ’77), pages 238–252. ACM Press, New York, 1977.

[10] P. Cousot and R. Cousot. Constructive versions of Tarski’s fixed point theorems. Pacific J. Math., 82(1):43–57, 1979.

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

[12] P. Cousot and R. Cousot. Inductive definitions, semantics and abstract interpretation. In Conference Record of the 19th ACM Symp. on Principles of Programming Languages (POPL ’92), pages 83–94. ACM Press, New York, 1992.

[13] F. de Boer, M. Gabbrielli, E. Marchiori, and C. Palamidessi. Proving concurrent constraint programs correct. In Conference Record of the ACM Symp. on Principles of Programming Languages (POPL ’94). ACM Press, New York, 1994.

[14] E. Dijkstra. Guarded commands, nondeterminism and formal derivation of programs. Comm. of The ACM, 18(8):453–457, 1975.

[15] P. Dwinger. On the closure operators of a complete lattice. Indagat. Math., 16:560–563, 1954.

[16] G. Filé, R. Giacobazzi, and F. Ranzato. A unifying view of abstract domain design. ACM Comput. Surv., 28(2):333–336, 1996.

[17] G. Filé and F. Ranzato. Complementation of abstract domains made easy. In M. Maher, editor, Proceedings of the 1996 Joint International Conference and Symposium on Logic Programming (JICSLP ’96), pages 348–362. The MIT Press, Cambridge, Mass., 1996.

[18] R. Giacobazzi. “Optimal” collecting semantics for analysis in a hierarchy of logic program semantics. In C. Puech and R. Reischuk, editors, Proc. of the 13th Internat. Symp. on Theoretical Aspects of Computer Science (STACS ’96), volume 1046 of Lecture Notes in Computer Science, pages 503–514. Springer-Verlag, Berlin, 1996.

[19] R. Giacobazzi, C. Palamidessi, and F. Ranzato. Weak relative pseudo-complements of closure operators. Algebra Universalis, 36(3):405–412, 1996.

[20] R. Giacobazzi and F. Ranzato. Complementing logic program semantics. In M. Hanus and M. Rodríguez Artalejo, editors, Proceedings of the 5th International Conference on Algebraic and Logic Programming (ALP ’96), Lecture Notes in Computer Science, pages 238–253. Springer-Verlag, Berlin, 1996.

[21] R. Giacobazzi and F. Ranzato. Refining and compressing abstract domains. In P. Degano, R. Gorrieri, and A. Marchetti-Spaccamela, editors, Proc. of the 24th Internat. Colloq. on Automata, Languages and Programming (ICALP ’97), volume 1256 of Lecture Notes in Computer Science, pages 771–781. Springer-Verlag, Berlin, 1997.

[22] R. Giacobazzi and F. Ranzato. The reduced relative power operation on abstract domains. Theor. Comput. Sci, 216:159–211, 1999.

[23] L. Henkin, J. Monk, and A. Tarski. Cylindric Algebras. Part I. North-Holland, Amsterdam, 1971.

[24] P. V. Hentenryck, V. Saraswat, and Y. Deville. Constraint processing in cc(FD). In A. Podelski, editor, Constraint programming: Basics and trends, volume 910 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, 1995.

[25] C. Hoare. An axiomatic basis for computer programming. Comm. of The ACM, 12(10):576–580, 1969.

[26] J. Morgado. Note on complemented closure operators of complete lattices. Portug. Math., 21(3):135–142, 1962.

[27] G. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Comput. Science Dept., Aarhus Univ., Aarhus, Denmark, 1981.

[28] V. Saraswat. Concurrent Constraint Programming Languages. The MIT Press, Cambridge, Mass., 1993.

[29] V. Saraswat, V. A. Rinard, and P. Panangaden. Semantic foundations of concurrent constraint programming. In Conference Record of the 18th ACM Symp. on Principles of Programming Languages (POPL ’91), pages 333–353. ACM Press, New York, 1991.

[30] Z. Shmuely. The structure of Galois connections. Pacific J. Math., 54(2):209–225, 1974.