Compositionality in the puzzle of semantics

Roberto Giacobazzi

Dipartimento di Informatica

Universit� a di Verona

Strada Le Grazie, I-37134 Verona, Italy

giaco@sci.univr.it

Isabella Mastroeni

Dipartimento di Informatica Universit� a di Verona

Strada Le Grazie, I-37134 Verona, Italy

mastroeni@sci.univr.it

ABSTRACT

In this paper we study the connection between the structure of relational abstract domains for program analysis and compositionality of the underlying semantics. Both can be systematically designed as solution of the same abstract domain equation involving the same domain refinement: the reduced power operation. We prove that most well-known compositional semantics of imperative programs, such as the standard denotational and weakest precondition semantics can be systematically derived as solutions of simple abstract domain equations. This provides an equational presentation of both semantics and abstract domains for program analysis in a unique formal setting. Moreover both finite and transfinite compositional semantics share the same structure, and this allows us to provide consistent models for program manipulation.

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, Verification

Keywords

Abstract interpretation, reduced power, compositional semantics, transfinite semantics, program manipulation.

1. INTRODUCTION

Compositionality plays a key role in program manipulation and program analysis. Compositional semantics are typically used to derive compositional analyzers, where the analysis of a program can be obtained by composing the

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. PEPM ’02, Jan. 14-15, 2002 Portland, OR, USA Copyright 2002 ACM 1-58113-455-X/02/0001 ...$5.00.

analysis of its sub-components or to derive program manipulation algorithms. The essence of compositional semantics is usually hidden in the ability of the semantics to observe input/output relations about program’s behaviors. One of the best frameworks to study semantics and compare them according to their relative precision is the hierarchy developed in [8], here called Cousot’s hierarchy of semantics, where semantics at different levels of abstractions are related with each other by abstract interpretation. A number of semantics including big-step, termination and non-termination, 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 starting from an (operational) maximal trace semantics of a transition system. The resulting hierarchy provides a complete account on the structure and the relative precision of most well-known semantics of programming languages.

One of the major challenge in Cousot’s construction is that semantics are abstract domains. Therefore they can be transformed, refined, decomposed, and composed similarly to what is usually done with abstract domains in static program analysis [18]. In this paper we characterize compositional semantics as solutions of simple abstract domain equations. The idea is to consider the reduced power operation [9] for abstract domain refinement as the basic operation able to include input/output relations in domains. The reduced power operation has been proved to give the necessary structure of abstract domains in order to model relational properties of program behavior [10, 21, 24, 28]. A similar structure can be included in semantics as well. If [[P_{1}]] and [[P_{2}]] are the semantics of program components P_{1} and P_{2}, and ⋄ is a syntactic operator for program composition, then the semantics [[·]] is compositional if there exists an operation ∘ such that: [[P_{1} ⋄ P_{2}]] = [[P_{1}]] ∘ [[P_{2}]]. We show that most well-known compositional semantics of imperative programs, such as the standard angelic denotational and weakest-liberal precondition semantics, can be systematically derived as solutions of simple abstract domain equations. We consider sequential syntactic composition of programs and trace composition ⌢ for composing semantics. In this case compositionality boils down to [[P_{1}; P_{2}]] = [[P_{1}]]^{⌢}[[P_{2}]]. We prove that the compositional semantics observing finite computations only, such that the angelic denotational and weakest-liberal precondition semantics, can be systematically derived as the most abstract semantics closed under reduced power and including noncompositional semantics which observe respectively final and initial states of finite traces. Unfortunately this construction is not applicable to infinite semantics. This is mainly due to the fact that the composition of infinite traces looses precision as we are unable to observe limit states, when they exist, on which traces may compose. These facts put in evidence that the use of reduced power in these conditions is limited and it doesn’t allow us to capture exactly the relational information in infinite computations. This fact leads to a stronger notion of compositionality, where the equation above holds also for non-terminating slices of code.

In order to find a semantics that satisfies this new concept of compositionality we define a non-standard semantics of traces, here called transfinite trace semantics, that is able to observe what happens also after an infinite loop^{1}. The transfinite semantics of a program is the set of all its possibly transfinite computations, i.e. computations whose length can be any ordinal, finite or infinite. We insert this new semantics in the Cousot’s hierarchy as a concretization (through a Galois insertion) of the maximal trace semantics. In this context we are able to systematically build by reduced power a transfinite version of denotational and weakest precondition semantics and prove that the standard corresponding semantics are abstractions of these latter ones. In this way we can outline a projection of the Cousot’s (standard) hierarchy of semantics in a more concrete level, here called non-standard level, connected with the standard one by abstract interpretation (see Fig. 2). In this new context we are able to prove the optimality of denotational and weakest precondition non-standard semantics, i.e. they are the most abstract semantics, on the non-standard level, that observe respectively the last and the first state of computations and that are closed under reduced power refinement. Moreover we prove formally the compositionality, in the stronger sense, of these semantics. This peculiarity of the transfinite denotational and weakest precondition semantics allows us to use them for modeling program slicing [26, 32] and more in general in program manipulation. Moreover the fact that these semantics don’t loose precision in presence of infinite computations makes it possible to give semantics to a program P in a way such that the semantics of a slice of P is always contained in the semantics of P. This proves the consistency of program slicing with respect to these semantics.

Related work

The idea of using abstract domain transformers to study semantics of programming languages is not new. For instance in [7] the domain operation of tensor product [30] is considered in order to design Hoare’s axiomatic semantics by exploiting the adjoint relation between pre and post conditions in Hoare triples. Most of the works that apply abstract domain transformers in the design of semantics consider the logic programming paradigm, which basically relies on the hierarchy of semantics developed in [4, 15]. In [15] reduced product is used in order to systematically compose a concrete semantics with abstract domains for program analysis. In [17] the authors study the relations between different semantics of logic programs, such as success pattern semantics, computed answer substitution semantics, and call pattern semantics by means of complementation. This idea is

1Cousot, in [7], noted this possibility underlining the utility of a transfinite trace semantics for modeling program slicing. further exploited in [16] where domain complementation is considered in order to study the symmetrical structure of Cousot’s hierarchy of semantics, in particular in the characterization of the complementary nature of angelic, infinite, and demonic semantics of a transition system. As for compositionality is concerned, the very first and, up to our knowledge, unique example of construction of compositional semantics by abstract domain transformation is in [19]. In this work, the authors proved that compositional semantics of logic programs in [2, 14] can be systematically designed by a generalization of Cousot’s reduced cardinal power operation [9] from non-compositional semantics of computed answer substitution. This work represents a starting point for our work, which generalizes the results in [19] to arbitrary programming languages whose semantics can be specified by a transition system of states. Moreover, we prove that the standard and non-standard (transfinite) compositional semantics are optimal, i.e. they are the most abstract solutions of simple domain equations. Clearly, our results can be specialized to the case of logic and constraint logic programming, obtaining in this way an enhanced theory for logic programming compositionality with respect to [2, 14, 19]. As for program manipulation, and in particular program slicing, is concerned, in [1, 3, 26, 29] we can find several approaches to lazy semantics for program dependence graphs. These kind of semantics are used in order to model program manipulation in a way such that the semantics of a slice approximates the semantics of the full program.

2. PRELIMINARIES

In the following g ∘ f denotes function composition, i.e., g ∘ f =^{def} λx.g(f(x)). The identity function λx. x : X ⟶X is denoted ι_{X}, ≅ denotes the isomorphism of ordered structures, and S ⟶T denotes the set of all functions from S to T ordered point-wise by ⊑. 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 (i.e. commuting on arbitrary suprema), and coadditive functions from C to A. The first infinite ordinal is ω =^{def} ⋃_{n∈ℕ} n. The proper class of all the ordinals is 𝕆. 𝕆_{l} is the proper class of limit ordinals, and λ is a typical limit ordinal. Note that 0 ∈ 𝕆_{l}. Following standard definitions we consider abstract domains formulated either in terms of Galois connections or in terms of closure operators [9]. An upper closure operator on a poset ⟨P, ≤_{P} ⟩ is an operator ρ : P → P monotone, idempotent and extensive (∀x ∈ P. x ≤_{P} ρ(x)). uco(P) denotes the set of all upper closure operators on P. Often, we will find particularly convenient to identify closure operators with their sets of fix-points. If ⟨C, ≤, ∨, ∧, ⊤, ⊥⟩ is a complete lattice then ⟨uco(C), ⊑, ⊔, ⊓, λx.⊤, λx.x⟩ is also a complete lattice where, for every {ρ}, {η}, {ρ_{i}}_{i∈I} ⊆ uco(C) and x ∈ C: ρ ⊑ η iff ∀y ∈ C. ρ(y) ≤ η(y) iff η(C) ⊆ ρ(C)

and (⊓_{i∈I}ρ_{i})(x) = ∧_{i∈I}ρ_{i}(x). If α : C ⟶^{m}A and γ : A⟶^{m}C

are monotone functions such that ι_{C} ⊑ γ ∘ α and α∘γ ⊑ ι_{A}, then (A, α, γ, C) is a Galois connection (GC) between A and C. The set of all GC’s between two complete lattices A and C is the tensor product A ⊗ C. A ⊗ C ≅ A⟶^{a}C ≅ C ⟶^{coa}A [30]. If α ∘ γ = ι_{A} we have a Galois insertion (GI) also denoted ⟨C, ≤_{C}⟩ \overrightarrow{⟶} ⟵_{α}^{γ} ⟨A, ≤_{A}⟩. Note that A ≅ C if and only if ⟨C, ≤_{C}⟩ \overrightarrow{⟶} \overleftarrow{⟵}_{α}^{γ} ⟨A, ≤_{A}⟩. If ⟨C, ≤_{C}⟩ \overrightarrow{⟶} ⟵_{α}^{γ} ⟨A, ≤_{A}⟩ and f : C ⟶ C, the best correct approximation f^{♯} : A ⟶ A of f is defined as f^{♯} =^{def} α∘f∘γ. Note that α∘f ≤_{A} f^{♯}∘α. Any GI ⟨C, ≤_{C}⟩ \overrightarrow{⟶} \overleftarrow{⟵}_{α}^{γ} ⟨A, ≤_{A}⟩ uniquely determines an upper closure operator γ ∘ α ∈ uco(C) and conversely ρ ∈ uco(C) uniquely determines a GI (ρ(C), ρ, id, C). Hence, we will identify uco(C) with the so-called lattice 𝔏_{C} of abstract interpretations of C [9]. The point-wise 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}}⟩.

Reduced product and power are the best known operations to compose domains in order to exploit respectively the attribute independent and relational properties of programs [9]. The reduced product ⊓_{i∈I}A_{i} of a family of domains {A_{i}}_{i∈I} ⊆ uco(C) is the most abstract domain in 𝔏_{C} which is more concrete than every A_{i}. The reduced relative power in [19] is a generalization over arbitrary quantales of Cousot’s original reduced power [9]. Let ⟨D, ≤, ⊙⟩ be a semi-quantale [27], i.e. an algebraic structure where ⟨D, ≤⟩ is a complete lattice and ⊙ : D × D ⟶ D is an associative, monotone and left-additive binary operation. Given a pair of Galois connections between a concrete domain D and the two domains D_{1} and D_{2}: ⟨D, ≤_{D}⟩ \overrightarrow{⟶} ⟵_{α_{1}}^{γ_{1}} ⟨D_{1}, ≤_{D_{1}}⟩ and ⟨D, ≤_{D}⟩ \overrightarrow{⟶} ⟵_{α_{2}}^{γ_{2}} ⟨D_{2}, ≤_{D_{2}}⟩, we define the (relative) reduced power of D_{1} and D_{2}, as the set D_{1} ⟶^{⊙} D_{2} of all the monotone functions from D_{1} to D_{2} defined as λx.α_{2}(d ⊙ γ_{1}(x)) with d ∈ D. The dual operation for a right-additive operation ⊙ is D_{2} ⟵^{⊙} D_{1} and it represents the set of all the monotone functions λx.α_{2}(γ_{1}(x)⊙d). D_{1} ⟶^{⊙} D_{2} is called forward reduced power and the set D_{2} ⟵^{⊙} D_{1} is called backward reduced power. We have that ⟨D, ≤_{D}⟩ \overrightarrow{⟶} ⟵_{α}^{γ} ⟨D_{1} ⟶^{⊙} D_{2}, ⊑⟩ with the function α = λd. λx. α_{2}(d ⊙ γ_{1}(x)) and, by duality,

⟨D, ≤_{D}⟩ \overrightarrow{⟶} ⟵_{α}^{γ} ⟨D_{2} ⟵^{⊙} D_{1}, ⊑⟩ with α = λd.λx.α_{2}(γ_{1}(x)⊙d).

3. COUSOT’S SEMANTICS HIERARCHY

We consider Cousot’s hierarchy of semantics as depicted in Fig. 1 (see [7, 11]), where continuous lines and arrows denote, respectively, isomorphisms and strict abstractions between semantics. Given a transition system ⟨Σ, τ⟩ with τ ⊆ Σ × Σ, Σ^{+} and Σ^{ω} =^{def} ℕ⟶Σ denote respectively the set of finite non-empty and of (ω-)infinite sequences on Σ, the set of all sequences is Σ^{∞} = Σ^{+} ∪ Σ^{ω}. The length of a sequence σ 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}⟩ ∈ τ. The maximal trace semantics of a transitions system [11] is the set τ^{∞} of all the finite and infinite traces of a program. The concatenation of traces is defined as follows: Let σ, δ ∈ Σ^{∞}, |σ| = n, |δ| = m and A, B ⊆ Σ^{∞} then σ^{⌢}δ = η where σ_{n−1} = δ_{0} and ∀i < n . η_{i} = σ_{i} ∧ ∀n ≤ j < m . η_{j} = δ_{j−n+1} while A^{⌢}B = { σ^{⌢}δ | σ ∈ A ∧ δ ∈ B ∧ σ_{n−1} = δ_{0} }. This operation is both right and left additive and ∀X ∈ ℘(Σ^{∞}) . X^{⌢}∅ = ∅ and Σ^{⌢}X = X^{⌢}Σ = X. Each semantics in Cousot’s hierarchy is derived as abstract interpretation of the maximal trace semantics τ^{∞}, as summarized in Table 1. The relational semantics ℛ^{∞} associates an input/output relation with program traces by using the bottom symbol ⊥ ∉ Σ to denote non-termination. The denotational semantics 𝒟^{∞} gives semantics by considering input-output functions. Dijkstra’s predicate transformer g𝒲p and Hoare’s axiomatic semantics gℋ consider respectively the weakest precondition predicate transformers and the set of all the Galois connections that specify the adjoint relation between weakest precondition and strongestpostcondition in Hoare’s triples {P } C {Q} [7]. Each semantics in natural style may have a corresponding angelic, demonic, and infinite observable which is again an abstraction, as summarized in Table 1. The angelic trace semantics τ^{+} observes only finite computations. We denote by ℛ^{+}, 𝒟^{+}, 𝒲lp, and pℋ the angelic abstractions of the corresponding semantics in natural style. The demonic semantics approximates non-termination by chaos, i.e. if there is a possibility of non-termination then any possible output is given, and this corresponds to allow the worst possible behavior of the program [8, 13]. We denote by ℛ^{∂}, 𝒟^{∂}, 𝒲p^{∂}, and gℋ^{∂} the demonic observables of the corresponding semantics in natural style. The infinite trace semantics τ^{ω}, with corresponding infinite relational ℛ^{ω}, observes non-terminating traces only.

[figure: •; •; •; •; •; •; •; •; •; •; •; •; •; •; •; •; •; τ^{∞}; ℛ∞; 𝒟∞; g𝒲 p; gℋ; τ^{+}; ℛ+; 𝒟+; 𝒲 lp; pℋ; ℛ∂; 𝒟∂; ^{𝒲p ∂}; ^{gℋ ∂}; τ^{ω}; τ⊣?; ℛω; angelic; natural; demonic; infinite; Hoare’s axiomatic; Dijkstra’s pred-trans; Denotational; Relational; Trace-based]

Figure 1: Semantics in Cousot’s hierarchy.

4. PROGRAM MANIPULATION

In the following we consider a simple imperative language, Imp [33], with the following syntax:

c ::= nil | id := e | c; c | if e then c else c | while e do c

We know that the denotational semantics is compositional, namely it is equal to the composition of the semantics of program’s sub-components. We want to give a characterization of this property of denotational semantics as a property of the corresponding abstraction in Cousot’s hierarchy. One of the major consequence of Cousot’s construction of semantics as abstract interpretations is that semantics correspond to abstract domains, namely it is possible to associate with each semantics a closure operator, i.e. an abstract domain, defined on the domain of maximal finite and infinite traces, and representing what is actually observable by the semantics. Hence we can think of formulating the problem of compositionality in terms of closure operators: If X and Y are two sets of traces representing the semantics of the

Semantics  Domain relation  Abstraction

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

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

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

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

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

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

ℛ^{∂} = α^{ℛ∂} (ℛ^{∞})  ⟨℘(Σ × Σ_{⊥}), ⊆⟩ \overrightarrow{⟶} ⟵_{α^{ℛ∂}}^{γ^{ℛ∂}} ⟨D^{∂}, ⊆⟩  α^{ℛ∂} (X) = X ∪ \{ ⟨σ_{0}, s⟩ | \begin{matrix}⟨σ_{0}, ⊥⟩ ∈ X \\ ∧ s ∈ Σ \end{matrix} \}

ℛ^{ω} = α^{ℛω} (ℛ^{∞})  ⟨℘(Σ × Σ_{⊥}), ⊆⟩ \overrightarrow{⟶} ⟵_{α^{ℛω}}^{γ^{ℛω}} ⟨℘(Σ × \{⊥\}), ⊆⟩  α^{ℛω} (X) = X ∩ (Σ × \{⊥\})

Table 1: Basic semantics and observables as abstract interpretations

components of a program and ρ is a closure operator representing an observable property of the semantics, then the corresponding semantics is compositional if

(Comp) ρ(X^{⌢}Y) = ρ(ρ(X)^{⌢}ρ(Y))

where the concatenation operator, ^{⌢}, is the canonical way of composing traces. The idea is that we can compose the observations made on partial computations and obtain back, as result and without any loss of precision, the observation of the whole computation. Let’s consider a wellknown compositional semantics as regards the concatenation of traces, which is the maximal trace semantics. We remind that if we denote as [[·]] this semantics, then we can describe its compositionality as [[P_{1}; P_{2}]] = [[P_{1}]]^{⌢}[[P_{2}]], where P_{1} and P_{2} are generic programs. Consider a GI: ⟨℘(Σ^{∞}), ⊆⟩ \overrightarrow{⟶} ⟵_{α}^{γ} ⟨A, ≤_{A}⟩ defined on the concrete domain of the maximal traces ℘(Σ^{∞}). This induces an abstract semantics which is defined on the abstract domain of denotations A: [[·]]^{A} =^{def} α([[·]]). Our aim in this paper is that of characterizing those abstract semantics that are compositional as regards the concatenation of programs, i.e. such that [[P_{1}; P_{2}]]^{A} = [[P_{1}]]^{A} ⋄[[P_{2}]]^{A}. In this equation we have the abstract operation ⋄ that has to approximate the concrete composition of traces on abstract denotations. The best correct approximation of ^{⌢} in A is by definition the best choice defining ⋄: [[P_{1}]]^{A} ⋄ [[P_{2}]]^{A} =^{def} α(γ([[P_{1}]])^{⌢}γ([[P_{2}]])). Note that we have [[P_{1}; P_{2}]]^{A} = α([[P_{1}; P_{2}]]) = α([[P_{1}]]^{⌢}[[P_{2}]]). It is known that, if we consider ⋄ as the best correct approximation of^{⌢} as defined above, then the relation α([[P_{1}]]^{⌢}[[P_{2}]]) ≤ [[P_{1}]]^{A} ⋄ [[P_{2}]]^{A} = α(γ([[P_{1}]])^{⌢}γ([[P_{2}]])) holds. Now, for the relation between GI and closure operators, its clear that the abstract semantics that satisfy the equation (Comp) are exactly those semantics that make this relation an equality. This means that the equation (Comp) characterizes precisely the semantics that are compositional as regards the concatenation of traces. Clearly, not all the semantics satisfy condition (Comp), as shown in the following example.

Example 4.1. Consider the semantics obtained by approximating the trace semantics with the abstraction function α(X) = { σ_{n−1} | σ ∈ X ∧ |σ| = n }. This semantics observes the final states of finite computations only. Consider the program

P [ \begin{matrix}P_{1} [ \begin{matrix}x := 0; \\ while x ≤ 3 do x := x + 1; \end{matrix} \\ P_{2} [ \begin{matrix}y := 0; \\ z := x + y; \end{matrix} \end{matrix}

The concrete semantics of P, where the states are the values in ℕ_{⊥} of the variables of P, is the only finite trace

\begin{aligned}[[P]] & = & \{⟨0, ⊥, ⊥⟩ → ⟨1, ⊥, ⊥⟩ → ⟨2, ⊥, ⊥⟩ → \\ & & → ⟨3, ⊥, ⊥⟩ → ⟨4, ⊥, ⊥⟩ → ⟨4, 0, ⊥⟩ → ⟨4, 0, 4⟩\} \end{aligned}

and the concrete semantics of P_{1} and P_{2} are

[[P_{1}]] = {⟨0, ⊥, ⊥⟩ → ⟨1, ⊥, ⊥⟩ → ⟨2, ⊥, ⊥⟩ →
→ ⟨3, ⊥, ⊥⟩ → ⟨4, ⊥, ⊥⟩}
[[P_{2}]] = {⟨⊥, 0, ⊥⟩ → ⟨⊥, 0, ⊥⟩ → ⟨⊥, 0, ⊥⟩}

Then the abstract semantics, denoted by [[·]]^{A} =^{def} α([[·]]), are

\begin{aligned}[[P]]^{A} & = & \{⟨4, 0, 4⟩\} \\ [[P_{1}]]^{A} & = & \{⟨4, ⊥, ⊥⟩\} \\ [[P_{2}]]^{A} & = & \{⟨⊥, 0, ⊥⟩\} \end{aligned}

It is easy to observe that there is no way of combining [[P_{1}]]^{A} and [[P_{2}]]^{A} in order to obtain [[P]]^{A}, since we have lost the history of the computation of the programs above.

Another problem related with equation (Comp) corresponds to characterize how the semantics ρ behaves in presence of divergence. It is known that in standard semantics [33], if the X component diverges then ρ(X^{⌢}Y) = ρ(X). Even if equation (Comp) holds, this fact represents a bound in compositionality because for any two computations Y ≠ Z, if X diverges then ρ(X^{⌢}Y) = ρ(X) = ρ(X^{⌢}Z). In this case we are unable to characterize what may happen beyond divergent computations. On the contrary this information is essential in order to give a consistent model for program manipulation [32]. Program slicing is a program manipulation technique that identifies syntactically well-defined portions of programs which are semantically significant but not necessarily close to each other. In particular a program slice is defined as a set of program statements that directly or indirectly contribute to the values assumed by a set of variables at some program point. Whenever a program is sliced we have the problem of how the semantics of a slice relates with the semantics of the original program. In general slicing can change the termination status, and therefore the program behavior. Indeed a slice can terminate on specific inputs that lead the original program to non-termination. Note that slicing can’t introduce divergence, it can only introduce termination.

Example 4.2. Consider the following programs written in Imp, taken from [26]:

P_{1} [ \begin{matrix}x := 0 ; \\ i := 1 ; while i > 0 do i := i + 1 ; \\ y := x; \end{matrix}

P_{2} [ \begin{matrix}x := 0 ; \\ w := 1 ; \\ y := x; \end{matrix} P_{3} [ \begin{matrix}x := 0 ; \\ y := x; \end{matrix}

Note that P_{3} is a slice of both P_{1} and of P_{2}. Let ⊑_{sl} be the relation “is-slice-of”^{2}, and let ⊑_{sem} be the relation of semantic approximation. In standard denotational semantics of imperative languages (denoted as [[·]]) the commands are denoted as store transformations. P_{1} contains a loop so we have that [[P_{1}]] = λs. ⊥. Hence P_{3} ⊑_{sl} P_{1} and P_{3} ⊑_{sl} P_{2} but it is clear that [[P_{1}]] ⊑_{sem} [[P_{3}]] ⊑_{sem} [[P_{2}]]. In other words in the standard semantics of imperative languages the relation “is-slice-of” is inconsistent with the semantic approximation relation.

Compositionality as described in equation (Comp) is necessary for modeling program manipulation, but it is not sufficient, as shown above for program slicing. In this example it is clear that the problem of the semantics lies upon the fact that it is unable to distinguish programs that may diverge. This means that a semantics is consistent with the program slicing if, independently from the termination status of program’s sub-components, the semantics can always distinguish the meaning of programs even if some of its subcomponents diverge. We can formalize this fact in the following way:

[[P_{1}]] ≠ [[P_{2}]] ⇒ ∀Q, W . [[Q]] ⋄ [[P_{1}]] ⋄ [[W]] ≠ [[Q]] ⋄ [[P_{2}]] ⋄ [[W]].

It is clear that the above holds iff

[[P_{1}]] ≠ [[P_{2}]] ⇒ ∀Q . [[Q]] ⋄ [[P_{1}]] ≠ [[Q]] ⋄ [[P_{2}]].

2See [25] for a formal definition of the relation “is-slice-of” in terms of program dependency graphs, PDG.

In order to solve this problem, the composition ρ(X) ⋄ ρ(Y) of two semantics ρ(X) and ρ(Y) should keep trace of what happens in Y even if X diverges. This corresponds to ask a stronger form of compositionality with respect to equation (Comp), namely that it is possible to subtract part of the computation and still be able to re-compose the whole computation back by composing its fragments. This form of compositionality is called strong compositionality. In a certain sense we are looking for a semantics which is both compositional, as in (Comp), and monotone with respect to a relation ˜⊑ on semantic objects, such that X ˜⊑Y iff X = [[P_{1}]], Y = [[P_{2}]], and P_{1} ⊑_{sl} P_{2}. Clearly, the standard maximal trace semantics, even though compositional, is not concrete enough to provide the ground for defining semantics which are strongly compositional, i.e. monotone with respect to ˜⊑.

In the following we introduce systematic methods for deriving semantics of programming languages which are both compositional and strongly compositional, namely they are adequate for modeling program manipulation techniques like slicing. We provide a domain-theoretic characterization of these properties as solutions of simple recursive abstract domain equations. This will correspond to ask for a lazy compositional semantics to be compositional as specified in equation (Comp), even beyond non-terminating traces.

5. TRANSFINITE SEMANTICS

In order to find a compositional semantics which is useful for slicing we consider traces able to look beyond the infinite computations, namely we use semantics represented by transfinite state traces of programs (e.g. see [23]). For transfinite traces we mean traces whose length can be any β ∈ 𝕆. In this way the finite computations are finite traces, while the infinite computations can have lengths which overcome the first infinite ordinal ω.

We can generalize the definition of finite trace obtaining the set of traces of length at most β, with β ∈ 𝕆:

Σ^{<β} =^{def} ⋃_{α∈β} α ⟶ Σ

With this notation it is evident that Σ^{+} = Σ^{<ω}. In order to specify the relation between semantics observing program’s behavior at different β-depth, with β ∈ 𝕆, as abstract interpretations of a most concrete transfinite semantics, we have to find if there exists an upper-bound, expressed in terms of number of states, on the possible length of a generic trace in the semantics of an Imp program.

Theorem 5.1. Let P a program written in Imp. The upper bound for the length of possible traces expressed in term of number of states of P is ω^{ω+1} ∈ 𝕆.

Proof. Consider a program P written in the simple imperative language Imp. We have to prove that, independently from the number of instructions (always finite) of P, the number of states is upper bounded by ω^{ω+1}.

First of all each program has a number of instructions upper bounded by ω, because it has to be executed so it can have only a finite number of instructions. Now we have to find the possible bounds for the single instructions. The command while is the only one that can diverge and so it is the command that can generate the greater number of states, if compared with all the other commands. So a generic program with n instructions has a number of possible states which is surely less than a program that has n while’s. Therefore suppose that the program contains only while’s. We have to find the upper bound for this command. Now we prove, by induction on the nesting level of while that if n is the maximum number of nested while, then the bound for the possible states of the most external while is ω^{2n+2}. If the nesting level is 0, then we have a while only with instructions with a finite number of states, so the upper bound of each instruction is ω. In the worst case the command diverges and so we have ω iterations, this means that the length is bounded by ω · ω = ω^{2}. Now suppose that a while, with a nesting level of n, is bounded by ω^{2n+2} states. We prove that we can add another while externally, enhancing the level of nesting to n + 1, then the upper bound becomes ω^{2n+4}. A generic while with maximum nesting level n + 1 has surely a number of states less than the one that contains only while commands with maximum level n. Then the possible states for this instruction is the number of iterations, bounded by ω, multiplied by the bound of each instruction, that for inductive hypothesis is ω^{2n+2}, multiplied by the number of instructions in the while, bounded by ω. So we have the bound ω^{2n+2}ωω = ω^{2n+4}. This means that the bound of a generic while is ω^{ω}, because we know, from [22], that ⋃ { ω^{m} | m ∈ ω } = ω^{ω}. Because a generic program has a number of instruction bounded by ω, the final bound is ω^{ω} · ω = ω^{ω+1}.

We will denote this maximal ordinal as ∝ =^{def} ω^{ω+1}. At this point we can define the maximal transfinite trace semantics as the semantics represented by the traces of the domain ℘(Σ^{∝}), where

Σ^{∝} =^{def} ⋃_{α∈∝} α ⟶ Σ

Consider for instance the following program written in Imp:

P [ \begin{matrix}x := 1; \\ while x > 0 do x := 3; \\ x := 5; \end{matrix}

It is clear that the program loops infinitely but it is also clear that after the execution of while there exists another state of the program, which cannot be reached in any finite computation, and which associates the value 5 with the variable x. So we think of studying computations which lead to the infinite, in order to observe what happens after a divergence. We can generalize the concept of transition system to the transfinite case by supposing that the transition relation can distinguish at which degree of infinite the transition is possible. Let the length of a transfinite trace be α ∈ 𝕆. If α is a limit ordinal then the index of the last state is α, otherwise it is α − 1. In general we will denote always with σ_{κ−1} the last state of a transfinite trace.

In order to generalize the trace concatenation to transfinite traces, we have to specify a topology on transfinite traces which allows us to specify limit states for traces whose length is a limit ordinal. This is achieved by considering the standard topology on traces as induced by 𝕆 : The limit ordinal are the open elements on 𝕆 while the successor ones are the closed elements of the topology [23]. This induces a topology on Σ^{∝} and in the following we assume that this topology is metrizable and complete [31], i.e. any Cauchy sequence of transfinite traces has a limit in Σ^{∝}.

The transfinite semantics is more concrete than the maximal trace semantics defined in the Cousot semantic hierarchy. In the following we denote the semantics of transfinite traces of a program by τ^{∝}.

Example 5.2. Consider the following program written in Imp:

P [ \begin{matrix}x := 2; \\ while x > 0 do x := x + 1; \\ x := 5; \end{matrix}

we represent the trace of states on the maximal trace semantics by considering the trace of the values of x in the computation:

2 ⟶ 3 ⟶ 4 ⟶ 5 ⟶ ⋯ ⟶ n ⟶ ⋯ ⊥

Namely the maximal trace semantics is not able to see beyond the loop. Instead if we consider the transfinite trace semantics, the trace becomes

2 ⟶ 3 ⟶ 4 ⟶ 5 ⟶ ⋯ ⟶ n ⟶ ⋯ ω ⟶ 5

In the following we prove that the maximal trace semantics τ^{∞} is indeed an abstract interpretation of the transfinite semantics τ^{∝} given by a Galois insertion between ℘(Σ^{∞}) and ℘(Σ^{∝}). We define the functions α^{∝} : ℘(Σ^{∝}) ⟶ ℘(Σ^{∞}) and γ^{∝} : ℘(Σ^{∞}) ⟶ ℘(Σ^{∝}) as

\begin{matrix}α^{∝}(X) = \{ σ ∈ Σ^{ω} | ∃δ ∈ X . σ ≼ δ \} ∪ (X ∩ Σ^{+}) \\ γ^{∝}(Y) = (Y ∩ Σ^{+}) ∪ \{ σ ∈ Σ^{∝} | ∃δ ∈ Y^{ω} . δ ≼ σ \} \end{matrix}

The relation ≼ is the prefix relation generalized to transfinite traces, namely if we define the relation σ ≼^{n} δ as σ cut at the length n is prefix of δ, then we can define σ ≼^{∞} δ as ∀n ∈ ω . σ ≼^{n} δ. This is the same as ≼^{∞} =^{def} ⋂_{n∈ω} ≼^{n}. In the following we will denote with ≼ the relation ≼^{∞}.

Proposition 5.3.

⟨℘(Σ^{∝}), ⊆⟩ \overrightarrow{⟶} ⟵_{α^{∝}}^{γ^{∝}} ⟨℘(Σ^{∞}), ⊆⟩

The following theorem proves that the standard finite and infinite maximal trace semantics is an abstract interpretation of the non-standard transfinite one.

Theorem 5.4. τ^{∞} = α^{∝}(τ^{∝}).

6. SEMANTICS BY REDUCED POWER

In this section we systematically construct compositional (resp. denotational and weakest precondition) semantics by composing more abstract non-compositional semantics, and we prove that these semantics are optimal, viz. most abstract with respect to the domain refinement operation given by reduced power. This proves that these semantics can be obtained as the most abstract solution of an abstract domain equation which involves the reduced power and a basic non-compositional semantics. Kleene algebras are the typical algebraic structures to reason about traces [5, 12]. A Kleene algebra is a sixtuple ⟨K, ≤, ⊤, ·, ⊥, 1⟩ such that ⟨K, ≤, ∨, ∧, ⊤, ⊥⟩ is a complete lattice, ⟨K, ·, 1⟩ is a monoid and · : K × K ⟶ K is both left and right additive. In order to apply the reduced relative power operation to design compositional semantics out of non-compositional ones, we need a quantale structure on transfinite traces. Kleene algebras provide this structure.

Proposition 6.1. ⟨℘(Σ^{∝}), ⊆, Σ^{∝},^{⌢} , ∅, Σ⟩ is a Kleene algebra providing a unitary quantale, where for any X, Y ∈

℘(Σ^{∝}) we have X^{⌢}Y =^{def} { σδ | σ ∈ X ∧ σ_{κ−1}δ ∈ Y }.

6.1 Potential λ-termination semantics

In Example 4.1 we have shown a non-compositional semantics observing final terminating states. We generalize that semantics to transfinite traces.

We know that if α ∈ 𝕆 then there exist (unique) λ ∈ 𝕆_{l} and n ∈ ω such that α = λ + n. This corresponds to say that λ ≤ α < S_{l}(λ), where S_{l}(λ) is the limit ordinal which follows λ. We also note that the limit ordinal λ is such that ∀γ ∈ 𝕆_{l} . γ ≤ α and γ ≤ λ, namely such λ is the biggest limit ordinal contained in α. In the following we denote by ⟨s, λ⟩ with s ∈ Σ and λ ∈ 𝕆_{l} the state s, in a possibly transfinite trace σ, located, in σ, in a position which is after the limit ordinal λ. Hence, ⟨σ_{κ−1}, λ⟩ denotes the final state of a possibly transfinite trace whose length overcomes λ and ⟨σ_{0}, λ⟩ is the initial state of the sub-trace of σ starting after λ. Clearly, the initial and final states in a finite trace σ ∈ Σ^{+} are respectively ⟨σ_{0}, 0⟩ and ⟨σ_{κ−1}, 0⟩. This notation allows us to keep trace of states between any two consecutive limit ordinals, namely states that can be located after any sequence of divergent computations. Therefore we define the two functions α^{⊢} : ℘(Σ^{∝}) ⟶ ℘(Σ) and γ^{⊢} : ℘(Σ) ⟶ ℘(Σ^{∝}), where we abbreviate with Σ the set Σ×∝:

\begin{matrix}α^{⊢}(X) = \{ ⟨σ_{κ−1}, λ⟩ | σ ∈ X ∧ λ ≤ |σ| < S_{l}(λ) \} \\ γ^{⊢}(Y) = \{ σ ∈ Σ^{∝} | ⟨σ_{κ−1}, λ⟩ ∈ Y ∧ λ ≤ |σ| < S_{l}(λ) \} \end{matrix}

Dually we can define the maps α^{⊣} : ℘(Σ^{∝}) ⟶ ℘(Σ) and γ^{⊣} : ℘(Σ) ⟶ ℘(Σ^{∝}) as follows

\begin{matrix}α^{⊣}(X) = \{ ⟨σ_{0}, λ⟩ | σ ∈ X ∧ λ ≤ |σ| < S_{l}(λ) \} \\ γ^{⊣}(Y) = \{ σ ∈ Σ^{∝} | ⟨σ_{0}, λ⟩ ∈ Y ∧ λ ≤ |σ| < S_{l}(λ) \} \end{matrix}

Proposition 6.2. Under the previous hypothesis:

• ⟨℘(Σ^{∝}), ⊆⟩ \overrightarrow{⟶} ⟵_{α^{⊢}}^{γ^{⊢}} ⟨℘(Σ), ⊆⟩

• ⟨℘(Σ^{∝}), ⊆⟩ \overrightarrow{⟶} ⟵_{α^{⊣}}^{γ^{⊣}} ⟨℘(Σ), ⊆⟩

The closure operators associated with the, respectively so called, forward and backward λ-termination semantics are the following functions:

ρ^{⊢}(X) =^{def} γ^{⊢}α^{⊢}(X) = \{ σ ∈ Σ^{∝} | \begin{matrix}∃δ ∈ X . σ_{κ−1} = δ_{κ−1} \\ λ ≤ |σ|, |δ| < S_{l}(λ) \end{matrix} \}

ρ^{⊣}(X) =^{def} γ^{⊣}α^{⊣}(X) = \{ σ ∈ Σ^{∝} | \begin{matrix}∃δ ∈ X . σ_{0} = δ_{0} ∧ \\ λ ≤ |σ|, |δ| < S_{l}(λ) \end{matrix} \}

where the ordinals are all limit and they are the biggest ones less than the length of the considered traces. We denote with τ^{⊢} and τ^{⊣} respectively the domains ρ^{⊢}(τ^{∝}) and ρ^{⊣}(τ^{∝}). Note that τ^{⊣} generalizes the potential termination semantics in [8], here defined for finite traces only.

6.2 Systematic construction of 𝒟 semantics

In this section we systematically derive the denotational semantics 𝒟 by refining the potential termination semantics with respect to the input/output relations. This is obtained by considering as refined domain the space of all monotone functions between sets of states. The idea is to approximate transfinite traces with input/output relations, which are functions in the case of denotational semantics. In this section we prove that this construction can be obtained as the backward reduced power of the potential forward λtermination semantics. In this case the abstraction function is given by construction: α^{D}(X) = λY. α^{⊢}(γ^{⊢}(Y)^{⌢}X).

Proposition 6.3.

⟨℘(Σ^{∝}), ⊆⟩ ⟶ ⟵_{α^{D}}^{γ^{D}} ⟨℘(Σ) ⟶ ℘(Σ), ⊑⟩

where:

\begin{matrix}α^{D}(X) = λY. \{ ⟨η_{κ−1}, λ_{1}⟩ | \begin{matrix}η ∈ X ∧ ⟨η_{0}, λ⟩ ∈ Y \\ ∧ λ_{1} ≤ λ + |η| < S_{l}(λ_{1}) \end{matrix} \} \\ γ^{D}(f) = \{ σ ∈ Σ^{∝} | \begin{matrix}∃λ . ⟨σ_{κ−1}, λ′⟩ ∈ f(⟨σ_{0}, λ⟩) \\ λ′ ≤ λ + |σ| < S_{l}(λ′) \end{matrix} \} \end{matrix}

The semantics obtained so far by reduced power construction models the space of functions on ℘(Σ) representing input/output relations of states in transfinite traces. We denote by 𝒟^{∝} =^{def} α^{D}(τ^{∝}). The following theorem proves that the denotational semantics in [8] corresponds precisely to backward reduced power of potential forward λ-termination semantics, by observing input/output functionalities of traces whose length is at most ω.

Theorem 6.4. 𝒟 = α^{𝒟} ∘ α^{ℛ} ∘ α^{∝} ∘ γ^{D}(𝒟^{∝}).

6.3 Systematic construction of g𝒲p semantics

The weakest precondition semantics can be obtained in a similar way by dualizing the construction of the denotational semantics. Duality here means exchanging the observation from the final to the initial state and reversing the relative power operation. In this section we derive the transfinite weakest precondition semantics as the forward reduced power of the potential backward λ-termination semantics. As before, the corresponding abstraction function follows by construction. Let X ⊆ Σ^{∝}, then by construction: α^{W} (X) = λY. α^{⊣}(X^{⌢}γ^{⊣}(Y)).

Proposition 6.5.

⟨℘(Σ^{∝}), ⊆⟩ ⟶ ⟵_{α^{W}}^{γ^{W}} ⟨℘(Σ) ⟶ ℘(Σ), ⊑⟩

where:

\begin{matrix}α^{W} (X) = λY. \{ ⟨η_{0}, λ_{1}⟩ | \begin{matrix}η ∈ X ∧ ⟨η_{κ−1}, λ⟩ ∈ Y \\ ∧ λ_{1} ≤ λ + |η| < S_{l}(λ_{1}) \end{matrix} \} \\ γ^{W} (f) = \{ σ ∈ Σ^{∝} | \begin{matrix}∃λ . ⟨σ_{0}, λ′⟩ ∈ f(⟨σ_{κ−1}, λ⟩) \\ λ′ ≤ λ + |σ| < S_{l}(λ′) \end{matrix} \} \end{matrix}

This semantics models the space of functions on ℘(Σ) representing the largest set of states that may lead the possibly transfinite computation in a given set of output states. We denote by 𝒲p^{∝} =^{def} α^{W} (τ^{∝}). The following theorem proves that the weakest precondition semantics defined in [8] corresponds precisely to reduced power of potential backward λtermination semantics, by observing the largest set of states that reach a given output state in at most ω steps.

Theorem 6.6. g𝒲p = α^{g𝒲p} ∘ α^{𝒟} ∘ α^{ℛ} ∘ α^{∝} ∘ γ^{W} (𝒲p^{∝}).

In Fig. 2 we show the transfinite semantics, here called non-standard semantics, with respect to Cousot’s hierarchy

[figure: •; •; •; •; •; •; •; •; •; •; •; •; •; ∘; •; •; ∘; •; •; •; Standard; Non-standard; …; …; τ^{∝}; τ^{∞}; τ^{⊣}; τ^{⊣?}; 𝒟; τ^{+}; τ^{<β}; τ^{∝}∖τ^{<β}; τ^{ω}; 𝒟^{∝}; 𝒲p^{∝}; g𝒲 p; 𝒲 lp; 𝒟^{+}]

Figure 2: Symmetrical standard and non-standard semantics.

of standard semantics. The standard natural semantics is here the “projection”, specified as an abstraction, of the natural transfinite level through the pair of adjoint functions α^{∝} and γ^{∝}. With each natural transfinite semantics τ^{∝}, 𝒟^{∝}, and 𝒲p^{∝} and a given ordinal β ∈ 𝕆, it is possible to specify symmetric approximate semantics observing computations up to β (τ^{<β} etc.) and observing computations longer than β (τ^{<∝} ∖τ^{<β} etc.). It is easy to observe that the standard angelic and infinite semantics can be obtained by abstract interpretation and in particular:

τ^{<β} = γ^{<β} ∘ α^{<β}(τ^{∝}) and τ^{∝}∖τ^{<β} = γ^{≥β} ∘ α^{≥β}(τ^{∝})

where

\begin{matrix}α^{<β}(X) = X ∩ Σ^{<β} & α^{≥β}(X) = X ∩ (Σ^{∝} ∖ Σ^{<β}) \\ γ^{<β}(Y) = Y ∪ (Σ^{∝} ∖ Σ^{<β}) & γ^{≥β}(Y) = Y ∪ Σ^{<β}. \end{matrix}

Note that if β = ω, then τ^{<ω} = τ^{+} and α^{∝}(τ^{∝}∖τ^{<ω}) = τ^{ω}. The remaining abstractions from the non-standard to the standard hierarchy in Fig. 2, can be derived in a similar way for all the semantics.

The equivalence between denotational and weakest precondition semantics proved in [8] can be generalized to the transfinite case. This follows directly by construction and can be emphasized by considering the corresponding closure operators. It is immediate to observe that the standard denotational semantics viewed as a closure operation on maximal traces is:

Den(X) = gWp(X) = \{ σ ∈ Σ^{+} | \begin{matrix}∃δ ∈ X^{+} . δ_{0} = σ_{0} \\ ∧ δ_{n−1} = σ_{n−1} \end{matrix} \} ∪

{ σ ∈ Σ^{ω} | ∃δ ∈ X ∖ Σ^{+} . σ_{0} = δ_{0} }

As a consequence of Theorem 6.4 and 6.6, this semantics can be obtained by applying the abstraction α^{∝} to the domains

τ^{⊢} ⟵^{⌢} τ^{⊢} and τ^{⊣} ⟶^{⌢} τ^{⊣}, where γ^{D} ∘ α^{D} =^{def} τ^{⊢} ⟵^{⌢} τ^{⊢} and

γ^{W} ∘ α^{W} =^{def} τ^{⊣} ⟶^{⌢} τ^{⊣}.

Proposition 6.7.

\begin{matrix}τ^{⊢} ⟵^{⌢} τ^{⊢} = τ^{⊣} ⟶^{⌢} τ^{⊣} = \\ λX. \{ σ ∈ Σ^{∝} | \begin{matrix}∃η ∈ X . η_{κ−1} = σ_{κ−1} \\ η_{0} = σ_{0} \\ ∃λ′ . λ′ ≤ |η|, |σ| < S_{l}(λ′) \end{matrix} \} \end{matrix}

Corollary 6.8.

Den = gWp = α^{∝} ∘ (τ^{⊢} ⟵^{⌢} τ^{⊢}) = α^{∝} ∘ (τ^{⊣} ⟶^{⌢} τ^{⊣}).

Remark 6.9. It can be easily verified that, by inverting the direction of the arrow in τ^{⊢} ⟵^{⌢} τ^{⊢}, we obtain the identity, namely it is immediate to prove that τ^{⊢} ⟶^{⌢} τ^{⊢} = ι_{℘(Σ)}. Intuitively this happens because the forward reduced power of the forward λ-termination semantics encodes how a given set X of concrete traces behaves when these are extended with any possible trace ending in a given set of observable states Y. Hence by observing the final states of these extended traces we get back Y. Instead, if we consider the initial states in this construction we can observe the set of initial states of concrete traces that will have final states in Y. This is precisely Dijkstra’s weakest precondition semantics gWp, as proved in Theorem 6.6. A similar reasoning holds if we dualize τ^{⊣} ⟶^{⌢} τ^{⊣}.

6.4 Optimal natural denotational semantics

Now we can prove that the transfinite denotational and weakest precondition semantics obtained so far are respectively the most abstract solutions of the abstract domain equations:

X = τ^{⊢} ⊓ (X ⟵^{⌢} X) and X = τ^{⊣} ⊓ (X ⟶^{⌢} X)

This allows us to prove an optimality result for τ^{⊢} ⟵^{⌢} τ^{⊢} and τ^{⊣} ⟶^{⌢} τ^{⊣} with respect to the capability of observing input/output relations of transfinite traces, namely we prove that these semantics are the most abstract ones observing τ^{⊢} (resp. τ^{⊣}) and which are closed under ⟵^{⌢} (resp. ⟶^{⌢}).

Theorem 6.10.

• (τ^{⊢} ⟵^{⌢} τ^{⊢}) ⟵^{⌢} (τ^{⊢} ⟵^{⌢} τ^{⊢}) = τ^{⊢} ⟵^{⌢} τ^{⊢}

• (τ^{⊣} ⟶^{⌢} τ^{⊣}) ⟶^{⌢} (τ^{⊣} ⟶^{⌢} τ^{⊣}) = τ^{⊣} ⟶^{⌢} τ^{⊣}

We can conclude that the domain τ^{⊢} ⟵^{⌢} τ^{⊢} is the most abstract solution of the equation X = τ^{⊢}⊓X ⟵^{⌢} X because it is immediate that τ^{⊢} ⊑ τ^{⊢} ⟵^{⌢} τ^{⊢}. A similar result holds for τ^{⊣} ⟶^{⌢} τ^{⊣} with respect to X = τ^{⊣} ⊓ (X ⟶^{⌢} X).

7. ANGELIC SEMANTICS

In this section we follow the construction given above in order to systematically derive the angelic denotational and Dijkstra’s weakest liberal precondition semantics by the forward (resp. backward) reduced relative power of the backward potential 0-termination semantics (resp. the forward potential 0-termination semantics). It is worth noting that the backward potential 0-termination semantics is the potential termination semantics in [8]. The forward potential 0-termination semantics observes the final states of finite traces. This semantics is built as abstraction of the natural trace semantics, by using the functions α^{⊢?} : ℘(Σ^{∞}) → ℘(Σ) and γ^{⊢?} : ℘(Σ) → ℘(Σ^{∞}) defined as follows:

\begin{matrix}α^{⊢?}(X) = \{ σ_{n−1} | σ ∈ X^{+} \} \\ γ^{⊢?}(Y) = \{ σ ∈ Σ^{+} | σ_{n−1} ∈ Y \} ∪ Σ^{ω} \end{matrix}

and constitute a Galois insertion. The corresponding closure is given as follows:

ρ^{⊢?}(X) =^{def} γ^{⊢?}α^{⊢?}(X) = \{ σ ∈ Σ^{+} | \begin{matrix}∃δ ∈ X^{+} . \\ δ_{n−1} = σ_{n−1} \end{matrix} \} ∪ Σ^{ω}

In the following we will denote τ^{⊢?} =^{def} ρ^{⊢?}(τ^{∞}).

Let α^{D^{+}} : ℘(Σ^{∞}) ⟶ (℘(Σ) ⟶ ℘(Σ)) be the function build by reduced power as α^{D^{+}}(X) = λY. α^{⊢?}(γ^{⊢?}(Y)^{⌢}X) which is λY. { σ_{n−1} | σ ∈ X^{+} ∧ σ_{0} ∈ Y }.

Lemma 7.1. 𝒟^{+} ≅ α^{D^{+}}(τ^{∞}).

We can characterize the angelic denotational semantics as upper closure operator on the domain of finite and infinite traces (see [8]):

Ang^{𝒟} (X) = \{ σ ∈ Σ^{+} | \begin{matrix}∃δ ∈ X^{+} . σ_{0} = δ_{0} \\ ∧ σ_{n−1} = δ_{n−1} \end{matrix} \} ∪ Σ^{ω}

Theorem 7.2. Ang^{𝒟} = τ^{⊢?} ⟵^{⌢} τ^{⊢?}.

Similar results can be obtained for the weakest-liberal precondition semantics by means of Cousot’s backward potential 0-termination semantics, i.e. Wlp = τ^{⊣?} ⟶^{⌢} τ^{⊣?}, where τ^{⊣?} is the backward potential 0-termination semantics [8]. Due to the equivalence of angelic denotational and weakestliberal precondition semantics, we have:

τ^{⊣?} ⟶^{⌢} τ^{⊣?} = τ^{⊢?} ⟵^{⌢} τ^{⊢?}

Similar results for optimality can be proved also in the angelic case.

Theorem 7.3.

• (τ^{⊢?} ⟵^{⌢} τ^{⊢?}) ⟵^{⌢} (τ^{⊢?} ⟵^{⌢} τ^{⊢?}) = τ^{⊢?} ⟵^{⌢} τ^{⊢?}

• (τ^{⊣?} ⟶^{⌢} τ^{⊣?}) ⟶^{⌢} (τ^{⊣?} ⟶^{⌢} τ^{⊣?}) = τ^{⊣?} ⟶^{⌢} τ^{⊣?}

This fact says us that the denotational angelic (resp. weakest liberal precondition) semantics is the fixed point of a refining process starting from τ^{⊢?} (resp. τ^{⊣?}) by using ⟵^{⌢} (resp. ⟶^{⌢}). So this semantics is the most abstract one which observe the final states of finite traces and which is closed as regards the functional relations between these states.

Remark 7.4. We wonder if τ^{⊢?} ⟵^{⌢} τ^{⊢?} = τ^{⊢?} ⊓ τ^{⊣?} namely, if τ^{⊢?} ⟵^{⌢} τ^{⊢?} is the most abstract closure operator which observe both the input and output states of finite traces. It is easy to verify that τ^{⊢?} ⟵^{⌢} τ^{⊢?} ≠ τ^{⊢?} ⊓ τ^{⊣?} and in particular:

\begin{aligned}τ^{⊢?} ⊓ τ^{⊣?} & = & (ρ^{⊢?} ⊓ ρ^{⊣?})(X) = \\ & = & \{ σ ∈ Σ^{+} | \begin{matrix}∃δ, η ∈ X . σ_{0} = δ_{0} \\ ∧ σ_{n−1} = η_{n−1} \end{matrix} \} ∪ Σ^{ω} \end{aligned}

In this semantics we can note that the relation between input and output of traces is not expressed. Indeed there are also traces that don’t necessarily have the initial and final state bounded by the fact that they belong to the same trace. In τ^{⊢?} ⊓ τ^{⊣?} we take the product of all the possible initial states with all the possible final states of traces in X. It is clear

that τ^{⊢?} ⟵^{⌢} τ^{⊢?} ⊑ τ^{⊢?} ⊓ τ^{⊣?} namely that τ^{⊢?} ⟵^{⌢} τ^{⊢?} is not

the most abstract semantics more concrete then both of τ^{⊢?} and of τ^{⊣?}.

8. COMPOSITIONALITY

The aim of this section is that of proving that both the denotational semantics and the weakest precondition semantics, seen as closures on the transfinite trace semantics, satisfy the compositionality relation, namely they are both solutions of the equation (Comp). Moreover we will see that these semantics are optimal, namely they are the most abstract semantics on ℘(Σ^{∝}) for which this property holds. For proving this fact we will use a result in [20].

Theorem 8.1. The most abstract solution on uco(C) of the equation ρ(X^{⌢}Y) = ρ(ρ(X)^{⌢}ρ(Y)) is

ρ = ρ ⊓ (ρ ⟶^{⌢} ι_{C}) ⊓ (ι_{C} ⟵^{⌢} ρ) ⊓ ((ι_{C} ⟶^{⌢} ρ) ⟵^{⌢} ι_{C}).

We prove that the closure τ^{⊢} ⟵^{⌢} τ^{⊢} = τ^{⊣} ⟶^{⌢} τ^{⊣} is the most abstract compositional semantics definable on the set of transfinite traces, which includes respectively τ^{⊢} and τ^{⊣} as an abstract interpretation. In the following we will denote simply with ι the closure ι_{℘(Σ^{∝})}, identity on ℘(Σ^{∝}).

Lemma 8.2. Let ρ =^{def} τ^{⊢} ⟵^{⌢} τ^{⊢}. Then ι ⟶^{⌢} ρ = ρ =

ρ ⟵^{⌢} ι.

Hence, we can conclude that the desired result holds trivially.

Theorem 8.3. The closure ρ =^{def} τ^{⊢} ⟵^{⌢} τ^{⊢} is the most abstract one defined on the domain ℘(Σ^{∝}), solution of the equation ρ(X^{⌢}Y) = ρ(ρ(X)^{⌢}ρ(Y)).

The same result holds for the angelic semantics. In this case we have:

Lemma 8.4. Let ρ =^{def} τ^{⊢?} ⟵^{⌢} τ^{⊢?} = τ^{⊣?} ⟶^{⌢} τ^{⊣?}. Then

ι ⟶^{⌢} ρ = ρ = ρ ⟵^{⌢} ι.

The closure τ^{⊢?} ⟵^{⌢} τ^{⊢?} = τ^{⊣?} ⟶^{⌢} τ^{⊣?} is therefore the most abstract semantics defined on the domain ℘(Σ^{∞}), which is solution of the equation (Comp).

The fact that the equation (Comp) has solution on the transfinite semantics says that we can slice programs without loosing informations about the semantics and without loosing consistency between the semantics of the hole program and the semantics of its parts. Hence the fact that the transfinite denotational semantics satisfies the equation

ρ(X^{⌢}Y) = ρ(ρ(X)^{⌢}ρ(Y))

says that this semantics is consistent with the relation ⊑_{sl} described in Example 4.2 and therefore it is adequate for program slicing.

Example 8.5. Consider the programs defined in Example 4.2. Now we can define the transfinite denotational semantics which observe the final state even after infinite computations, denoted as [[·]].

[[P_{1}]] : \begin{matrix}x ↦ 0 \\ i ↦ ω \\ y ↦ 0 \end{matrix}  [[P_{2}]] : \begin{matrix}x ↦ 0 \\ w ↦ 1 \\ y ↦ 0 \end{matrix}  [[P_{3}]] : \begin{matrix}x ↦ 0 \\ y ↦ 0 \end{matrix}

In this way it is clear that the relations between the programs semantics are:

[[P_{3}]] ⊑_{sem} [[P_{1}]] and [[P_{3}]] ⊑_{sem} [[P_{2}]]

exactly as we wanted, namely they are consistent with the existing “is-slice-of” relation between programs ⊑_{sl}, described in Example 4.2.

Angelic Natural

Infinite

Hoare-logic/ Weakest-liberal:

X = τ^{⊣?} ⊓ X ⟶^{⌢} X [figure]

[figure]

α^{∝}(X = τ^{⊣} ⊓ X ⟶^{⌢} X) ⊖ (Y = τ^{⊣?} ⊓ Y ⟶^{⌢} Y) [figure]

[figure]

α^{∝}(X = τ^{⊣} ⊓ X ⟶^{⌢} X)

Denotational/ Relational:

X = τ^{⊢?} ⊓ X ⟵^{⌢} X [figure]

[figure]

[figure]

α^{∝}(X = τ^{⊢} ⊓ X ⟵^{⌢} X) ⊖ (Y = τ^{⊢?} ⊓ Y ⟵^{⌢} Y) [figure]

[figure]

τ^{⊣?}

Potential 0-term.

[figure] [figure]

[figure]

α^{∝}(X = τ^{⊢} ⊓ X ⟵^{⌢} X)

τ^{⊣}

Potential λ-term.

[figure]

[figure]

τ^{∞}

Maximal trace

[figure]

τ^{∝} ; Transfinite

Figure 3: Semantics as abstract domain equations

9. CONCLUSION

We have shown a strong connection between the structure of relational abstract domains for program analysis and compositionality of the underlying semantics. Both can be systematically designed by solving the same abstract domain equation by means of the same domain refinement: the reduced power operation (see [28] for an example of relational abstract domains for program analysis as solutions of recursive domain equations). These results provide an equational presentation of semantics and abstract domains for program analysis in a unique formal setting. Fig. 3 shows the structure of Cousot’s hierarchy of semantics as a hierarchy of abstract domain equations. Here ⊖ is abstract domain complementation [6], and it is applied to characterize the complementary nature of angelic and infinite semantics as shown in [16]. Moreover both finite and transfinite compositional semantics share the same structure, and this allows us to provide consistent models for program manipulation. It is worth noting that the algebraic properties of program integration techniques (and therefore of program slicing) are similar to the properties of reduced power which, as we proved in this paper, is the basic operation to refine any non-compositional semantics in order to make it compositional. Therefore similar algebraic operators can be used to model both syntactic manipulation techniques and the corresponding compositional semantics. As observed in [25], well-known algorithms for program integration, like the Horowitz, Prins, and Reps’s algorithm (HPR), can be formulated in terms of intuitionistic implication on the complete Heyting algebra constructed on dependency graphs. On the other side the reduced relative power operation exploits linear implications on a given quantale [20], which is a generalization of complete Heyting algebras [21, 27]. The analogy and the relation between these two constructions deserves further research.

10. REFERENCES

[1] Ballance, R. A., Maccabe, A. B., and Ottenstein, K. J. The program dependence web: A representation supporting control-,data-, and demand-driven interpretation of imperative languages. In Proc. of the ACM SIGPLAN Conf. on Programming Language Design and Implementation (1990), pp. 257–271.

[2] Bossi, A., Gabbrielli, M., Levi, G., and Meo, M. C. A compositional semantics for logic programs. Theor. Comput. Sci. 122, 1-2 (1994), 3–47.

[3] Cartwrite, R., and Felleisen, M. The semantics of program dependence. In Proc. of the ACM SIGPLAN Conf. on Programming Language Design and Implementation (1989), pp. 13–27.

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

[5] Conway, J. H. Regular algebra and finite machines. Chapman and Hall, 1971.

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

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

[8] Cousot, P. Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Theor. Comput. Sci. (2000). To appear, extended version of [7].

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

[10] Cousot, P., and Cousot, R. Abstract interpretation and application to logic programs. J. Logic Program. 13, 2-3 (1992), 103–179.

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

[12] Desharnais, J., Möller, B., and Tchier, F. Kleene under a demonic star. In Proc. of the 9th Internat. Conf. on Algebraic Methodology and Software Technology (AMAST ’00) (2000), vol. 1816 of Lecture Notes in Computer Science, pp. 355–370.

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

[14] Gaifman, H., and Shapiro, E. Fully abstract compositional semantics for logic programs. In Conference Record of the 16th ACM Symp. on Principles of Programming Languages (POPL ’89) (1989), ACM Press, New York, pp. 134–142.

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

[16] Giacobazzi, R., and Mastroeni, I. A characterization of symmetric semantics by domain complementation. In Proc. of the 2nd international conference in principles and practice of declarative programming PPDP’00 (2000), ACM press, pp. 115–126.

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

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

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

[20] Giacobazzi, R., Ranzato, F., and Scozzari, F. Building complete abstract interpretations in a linear logic-based setting. In 5th International Symp. SAS (1998), G. Levi, Ed., vol. 1503, pp. 215–229.

[21] Giacobazzi, R., and Scozzari, F. A logical model for relational abstract domains. ACM Trans. Program. Lang. Syst. 20, 5 (1998), 1067–1109.

[22] Just, W., and Weese, M. Discovering modern set theory. I: The basics, vol. 8 of Graduate studies in mathematics. American mathematical society, 1996.

[23] Kennaway, J. R., Klop, J. W., Sleep, M. R., and Vries, F. J. Transfinite reductions in orthogonal term rewriting systems. Information and computation 119, 1 (1995), 18–38.

[24] Nielson, F. Tensor products generalize the relational data flow analysis method. In Proc. of the 4th Hungarian Computer Science Conf. (1985), M. Arató, I. Kátai, and L. Varga, Eds., pp. 211–225.

[25] Reps, T. Algebraic properties of program integration. Sci. Comput. Program. 17 (1991), 139–215.

[26] Reps, T., and Turnidge, T. Program specialization via program slicing. In Proceedings of the Dagstuhl seminar on Partial evaluation (1996), O. Danvy, R. Glueck, and P. Thiemann, Eds., Springer-Verlag, pp. 409–429.

[27] Rosenthal, K. I. Quantales and their Applications. Pitman Research Notes in Mathematics. Longman Scientific & Technical, London, 1990.

[28] Scozzari, F. Logical optimality of groundness analysis. In Proceedings of International Static Analysis Symposium, SAS’97 (1997), P. V. Hentenryck, Ed., vol. 1302 of Lecture Notes in Computer Science, Springer-Verlag, pp. 83–97.

[29] Selke, R. P. A rewriting semantics for program dependence graphs. In Conference Record of the 16th ACM Symp. on Principles of Programming Languages (POPL ’89) (1989), ACM Press, New York, pp. 12–24.

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

[31] Smyth, M. B. Topology. In Handbook of logic in computer science, vol. 1. Clarendon press - Oxford, 1992.

[32] Weiser, M. Program slicing. IEEE Transactions on software engineering SE-10, 4 (1984), 352–357.

[33] Winskel, G. The formal semantics of programming languages: an introduction. MIT press, 1993.