1 Introduction↩︎

In any theory, the study of limit cases is a powerful means of exposing its conceptual structure. They mark the boundary between possibility and impossibility, distinguish essential assumptions from accidental ones, and provide idealized reference points for understanding more practical instances. Complete abstract interpretations play this role within abstract interpretation.

Abstract interpretation is a general theory for specifying approximate semantics of programming languages [1], including program analysis, program logics, and program transformations as special cases. This is achieved by designing an approximate (abstract) interpreter from the semantics of a given computational system (e.g., a programming language) and an abstraction of its state space. The abstraction, specified by the so called abstract domain, later denoted \(A\), plays a key role in the abstract interpretation construction. It specifies precisely what information has to be retained and what can be abstracted away, with the specific goal that interpreting in the simplified abstract domain yet keeps as much information as possible to achieve our goals, e.g., proving program correctness.

By construction, abstract interpretation is sound [1], meaning that if the approximate abstract interpretation of a program is correct with respect to a specification then also its concrete semantics satisfies the specification. The converse is rare and corresponds to the limit, and ideal, situation where no loss of precision is cumulated in the abstract interpretation with respect to what can be obtained by abstracting the concrete computation. When this happens we have completeness [2], [3]. Completeness clarifies which aspects of a computation can be abstracted away while preserving the ability to reason precisely about its properties. In program verification, program analysis and program logics completeness guarantees the absence of false positives, therefore making it possible to have a perfect matching between concrete and approximate correctness proofs. It is about three decades that completeness has been studied as a field by its own [4]. It has been extensively studied in the context of abstraction refinement for program analysis [3], [5], [6], information flow security by (abstract) non-interference [7], code protection [8], semantic properties of abstract interpreters, such as extensionality and referential transparency [9], in the combination of correctness and incorrectness logics of programs [10], [11], in the coordination of inductive and co-inductive-up-to techniques for proving properties of greatest fixed point computations [12] and, recently, in the context of the design of best correct approximations (bca) of predicate transformers [13].

1.1 The problem↩︎

On one side standard computability is a theory of sets and functions indexed on programs enjoying all beautiful properties such as extensionality and referential transparency [14]. On the other side it has been proved that abstract interpretation is inherently intensional in nature [9], i.e., its quality strictly depends upon the way the code is written. This is indeed a direct consequence of the lack of compositionality [13] which is guaranteed only when we can suppress intermediate abstractions in the composition of abstract functions, as it happens when the outer function is complete locally to the output of the inner one. It is precisely completeness in this localized version that plays a central role in reconciling computability theory with abstract interpretation.

Local completeness is a weaker form of completeness introduced in [10] and further developed in [6], [11] in the contexts of LCL (Local Completeness Logic), combining correctness and incorrectness logic, and AIR (Abstract Interpretation Refinement), generalizing CEGAR-style refinement to arbitrary abstract domains. Unlike global completeness, traditionally studied in the literature (e.g., see [3]), which requires completeness with respect to all possible inputs, local completeness requires completeness only for a fixed input property. When it holds along a computation trace in the intermediate junctions of post/pre conditions, it guarantees that no loss of precision is propagated along that trace. This localized perspective has proved particularly useful for analyzing the precision of abstract interpreters defined inductively over the syntax of programs. Contrary to global completeness studied in [15], local completeness does not have a recursion-theoretic characterization. Our contribution, which is primarily theoretical in nature, wants to fill this gap.

1.2 Main contribution↩︎

We first analyze decidable abstract domains as uniform transformations. For decidable abstract domains, whose elements represent decidable program properties as commonly used in program analysis and verification, we show that uniformity precisely separates dynamic from static program analysis. Here, uniformity is the ability to compute effectively the abstract property associated with a concrete set from any program enumerating that set, independently of how the set is generated or used. This establishes the boundary between merely abstracting the result of an interpreter and performing abstract interpretation.

In this context we study the complexity in the arithmetical hierarchy of the classes of all programs admitting an abstract semantics which is locally complete for a given input property \(I\) in a fixed abstract domain \(A\). We prove that when \(A\) is not trivial, i.e., it is not the identical abstraction or the abstraction which collapses all properties into a single don’t know value, this class, later denoted \({\mathbb{C}}(A,I)\), is bi-productive, i.e., it is productive as well as its complement, the latter under mild hypothesis. Only when \(I=\varnothing\) the complement class \(\raisebox{0ex}[1ex][1ex]{\overline{{\mathbb{C}}(A,I)}}\), called the incompleteness class, is computably enumerable. In particular we prove that for continuous abstract domains and input property \(I\neq\varnothing\) the classes \({\mathbb{C}}(A,I)\) and \(\raisebox{0ex}[1ex][1ex]{\overline{{\mathbb{C}}(A,I)}}\) are respectively in \(\Pi^0_2\) and \(\Sigma^0_2\) in the arithmetic hierarchy.

The above results show the intrinsic difficulties associated with completeness and incompleteness persist even in their weaker—local, formulation. Since productive sets are by definition not computably enumerable, neither local completeness nor local incompleteness admits an effective enumeration that fulfills respectively \({\mathbb{C}}(A,I)\) and \(\raisebox{0ex}[1ex][1ex]{\overline{{\mathbb{C}}(A,I)}}\). Actually these results show that these two classes are recursively inseparable, namely no decidable set \(C\) that contains all elements of \({\mathbb{C}}(A,I)\) while excluding all elements of \(\raisebox{0ex}[1ex][1ex]{\overline{{\mathbb{C}}(A,I)}}\); that is, no computable yes/no procedure can perfectly separate the positive cases in \({\mathbb{C}}(A,I)\) from the negative cases in \(\raisebox{0ex}[1ex][1ex]{\overline{{\mathbb{C}}(A,I)}}\). While productivity rules out any effective enumeration of these classes as sets of programs, we prove that \({\mathbb{C}}(A,I)\) admits a computably enumerable (and hence also a decidable) covering. The idea here is that we do not try to enumerate exactly all and only the programs in \({\mathbb{C}}(A,I)\). Instead, we provide a fix-point characterization in terms of effective program transformations¹ of a representative family of programs whose semantic behavior covers the entire class. The covering is allowed to miss many programs, as long as it still contains enough representatives to capture all relevant behaviors in \({\mathbb{C}}(A,I)\). The proof follows the structure of similar proofs in abstract computational complexity (e.g., see [16]): here to be cancelled by an effective program transformation are the cases of incompleteness.

1.3 Related works↩︎

The most related paper is [15] where the authors firstly analyzed the problem of completeness from the perspective of the programs for which an abstract domain is complete instead of the abstract domains that induce completeness for a given program, as previously extensively done in the literature. This naturally leads to the notion of completeness class. We extend their approach to the weaker case of local completeness and we prove that local and global completeness share the same complexity in the arithmetic hierarchy. Moreover we characterize a c.e. (computably enumerable) covering of the class of local complete programs for a non trivial abstract domain and prove the complexity of transformations mapping arbitrary programs to the complement class of locally incomplete programs. The covering provides the very first characterization of completeness in fix-point form, while the transformation making programs locally incomplete provides an effective lower bound to code obfuscating transformations.

In [17] the author presents an important practice-oriented (and personal) account of completeness in static analysis by abstract interpretation, distinguishing the completeness of an abstract domain from the completeness of the method used to compute invariants. The author affirms that completeness matters because incompleteness methods may be hard to control and unpredictable: for example, widening can fail to find invariants that exist in the chosen abstract domain, and small or seemingly irrelevant program changes may alter the analysis outcome. The author concludes that complete methods, when available, provide robustness, unique well-defined results, better testability, and clearer complexity questions. With respect to [17] we consider only imprecise transfer functions and the lack of compositionality due to combinations of abstractions as possible sources of incompleteness. Interestingly the productivity of \({\mathbb{C}}(A,I)\) is consistent with the undecidability of the existence of suitable invariants. This connection opens interesting future developments on the expressivity of abstract domains to represent program invariants.

In [18] the authors studied semantic transformations that minimally modify a semantic function to make it globally complete for a fixed abstract domain. These results can be seen as a model-based attempt to cover the class of all predicate transformers that are globally complete. The limit of that approach is in its pure model-based nature: it transforms the semantics to achieve completeness, not the code that computes that semantics. We instead attack the problem from a recursion-theoretic perspective, namely by means of program transformations. By characterizing effective program transformations that remove local incompleteness we are able to precisely identify a computably enumerable covering of \({\mathbb{C}}(A,I)\), hence achieving local completeness by code repair.

2 Preliminaries↩︎

In this section we introduce some mathematical notation and background in recursion theory and abstract interpretation. For the first the reader can refer to [14], [19], [20]. For the latter see [1], [2], [21].

2.1 Sets and functions↩︎

Throughout this work, \(\omega\) will denote the set of all natural numbers and \(\aleph_0\) its cardinality. Given two sets \(S\) and \(T\), \(\wp(S)\) denotes the powerset of \(S\), \(S \smallsetminus T\) denotes the set-difference between \(S\) and \(T\), \(\raisebox{0ex}[1ex][1ex]{\overline{S}}\) denotes the complement of \(S\) with respect to the relevant universe of discourse, and \(S \subsetneq T\) denotes strict inclusion. We use exponents to represent the repeated Cartesian product of a set with itself, so \(S \times S = S^2\) and \(S^{n+1} = S^n \times S\) for all \(n \geq 2\).

A function \(f\) is introduced \(f:S\rightarrow T\) if \(f\) is a total function from \(S\) to \(T\) or \(f: ST\) if it is a partial function. For any \(x \in S\), we write \(f(x){\downarrow}\) to signify that \(f\) is defined for the particular \(x\) and \(f(x){\uparrow}\) to signify that \(f(x)\) is not defined. The domain and range of \(f\) are, respectively, the sets \[\textit{dom}(f) \raisebox{0ex}[1ex][1ex]{\:\triangleq\:}\{x \in S ~|~ f(x){\downarrow}\}~~and~~\textit{rng}(f)\raisebox{0ex}[1ex][1ex]{\:\triangleq\:}\{f(x) ~|~ x \in S\cap \textit{dom}(f)\}.\] Given a set \(X\subseteq S\), the image of \(f\) on \(X\) is \[\raisebox{0ex}[1ex][1ex]{f}(X) \raisebox{0ex}[1ex][1ex]{\:\triangleq\:}\{f(x)~|~x\in X\cap \textit{dom}(f)\}.\] Two partial functions \(f,g: ST\) are extensionally equivalent, denoted \(f\cong g\), if \(\textit{dom}(f)=\textit{dom}(g)\) and \(f(x) = g(x)\) for all \(x \in \textit{dom}(f) = \textit{dom}(g)\).

Occasionally, we define functions using \(\lambda\)-notation \(\lambda x \st f(x)\); often, this notation is used when we want to emphasize the arguments of the function. For any two functions \(f : S T\) and \(g : T U\), \(g \circ f : S U\), we write \((\fcomp{f}{g})(x)\) to denote the composition of \(f\) and \(g\) where \((\fcomp{f}{g})(x){\downarrow}\) when both \(g(x){\downarrow}\) and \(f(g(x)){\downarrow}\); otherwise, \((f \circ g)(x){\uparrow}\).

2.2 Basic Order Theory↩︎

A set \(L\) endowed with a partial order relation \(\leq\) is called a poset and is denoted \(\langle L,\leq \rangle\). A chain of the poset \(\langle L,\leq \rangle\) is a sequence of elements in \(L\) totally-ordered under the relation \(\leq\). A poset \(\langle L,\leq \rangle\) is a lattice whenever binary least upper bounds (lubs) \(x \vee y\) and greatest lower bounds (glbs) \(x \wedge y\) exist for all \(x,y \in L\). A lattice \(\langle L,\leq \rangle\) is complete if every subset \(X \subseteq L\) (including the empty set) has a unique lub \(\bigvee X\) and glb \(\bigwedge X\). We write \(\langle L, \leq, \vee, \wedge, \top, \bot \rangle\) to denote the complete lattice \(L\) with partial order \(\leq\), lub \(\vee\), glb \(\wedge\), greatest element (top) \(\top\), and least element (bottom) \(\bot\). A poset \(\langle L,\leq \rangle\) is an \(\omega\)-cpo if \(L\) contains the lubs of all \(\omega\)-chains—chains that can be indexed by the natural numbers.

If \(\langle L,\leq \rangle\) is a poset and \(f,g:S \rightarrow L\), then \(f\) and \(g\) can be ordered with respect to the poset; we write \(f \sqsubseteq g\) if \(f(x) \leq g(x)\) for all \(x \in S\). If \(L\) is a (complete) lattice then \(\langle S\rightarrow L,\sqsubseteq \rangle\) is a (complete) lattice; the operators \(\sqcup\) and \(\sqcap\) are used to denote, respectively, the lub or glb of \(L\) or any of its chains or subsets. A function \(f : L_1 \rightarrow L_2\) between complete lattices is additive (co-additive) if for all \(Y \subseteq L_1\), \(f(\vee_{L_1} Y ) = \vee_{L_2} f(Y)\) (\(f(\wedge_{L_1} Y ) = \wedge_{L_2} f(Y ))\). Also, \(f\) is continuous (co-continuous) when \(f\) preserves lubs (glbs) of chains in \(L_1\). Recall that any monotone function \(f:L \rightarrow L\) on a complete lattice \(L\) always has least and greatest fix-points, denoted \({\sf lfp\/}(f)\) and \({\sf gfp\/}(f)\) respectively. If \(f:L \rightarrow L\) is continuous then \({\sf lfp\/}(f)=\bigvee_{n\in\omega}f^n(\bot)\) where \(f^n\) is defined inductively so that \(f^0(x)\raisebox{0ex}[1ex][1ex]{\:\triangleq\:}x\) and \(f^{n+1}(x)\raisebox{0ex}[1ex][1ex]{\:\triangleq\:}f(f^n(x))\) for all \(n \in \omega\).

2.3 Basic recursion theory↩︎

2.3.1 Computable functions.↩︎

Partial computable functions are (possibly partially-defined) functions that can be computed by a Turing Machine. We assume a surjective enumeration \(\mathscr{L}\), also called a programming system, of partial computable functions of \(n\) arguments and \(m\) outputs for any \(n,m\in\omega\). For any \(e\in\omega\), the function \(\raisebox{0ex}[1ex][1ex]{\varphi^{n\, m}_{e}}\) denotes a partial computable function of index \(e\) taking \(n\) arguments and producing \(m\) outputs. Here, \(e\) represents the code of a unique Turing machine that computes \(\raisebox{0ex}[1ex][1ex]{\varphi^{n\, m}_{e}}\). Following standard convention, we assume the partial functions \(\raisebox{0ex}[1ex][1ex]{\varphi^{n\, m}_{e}}\) are defined over the infinite denumerable domains \(\mathbb{D}^n\) and \(\mathbb{D}^m\) (i.e., for all \(n\in\omega:\,|\mathbb{D}^n|=\aleph_0\)) where \(\mathbb{D}\) includes a representation of all natural numbers and the programming system \(\mathscr{L}\) (i.e., \(\omega\subseteq \mathbb{D}\) and \(\mathscr{L}\subseteq\mathbb{D}\)). Under the convention, the partial computable functions are \(\raisebox{0ex}[1ex][1ex]{\varphi^{n\, m}_{e}}: \mathbb{D}^n \mathbb{D}^m\), for all \(e\in\mathscr{L}\) and all \(n,m\in\omega\). In practice, we omit \(n\) and/or \(m\) when the number of arguments and outputs of function is irrelevant or clear from context.

A programming system \(\mathscr{L}\) is considered acceptable if it is universal; that is, if it includes a partial computable function \(\mathsf{U}:\mathscr{L}\times\mathbb{D}\mathbb{D}\) such that if \(\{\psi_i\}_{i\in\omega}\) is an enumeration of all partial computable functions then \(\mathsf{U}(i,x)=\psi_{i}(x)\), and there exists a total computable function \(t:\omega\rightarrow\mathscr{L}\) such that \(\varphi_{t(i)}=\psi_{i}\). Because acceptable enumerations are isomorphic by Rogers’ isomorphism, we can identify the index \(e\in \mathscr{L}\) as the corresponding program in the given programming system \(\mathscr{L}\), which is usually a programming language. Hence \(\raisebox{0ex}[1ex][1ex]{\varphi^{\, }_{e}}\) is the function (semantics) computed by the program \(e\in\mathscr{L}\). A set of programs \(S\subseteq\mathscr{L}\) is an extensional property of \(\mathscr{L}\) if \(e\in S~\wedge~\raisebox{0ex}[1ex][1ex]{\varphi^{\, }_{e}}\cong\raisebox{0ex}[1ex][1ex]{\varphi^{\, }_{i}}~\Rightarrow~i\in S\). Two sets \(A,B\subseteq\mathscr{L}\) are extensionally equivalent if \(\{\raisebox{0ex}[1ex][1ex]{\varphi^{\, }_{e}} ~|~ e\in A\}=\{\raisebox{0ex}[1ex][1ex]{\varphi^{\, }_{e}} ~|~ e\in B\}\). \(A\) is a covering (a.k.a, representation) of \(B\) when \(A\) and \(B\) are extensionally equivalent and \(A\subsetneq B\).

2.3.2 Computability.↩︎

A set \(S\subseteq \mathbb{D}\) is computably enumerable (c.e.) if there exists a partial computable function \(\raisebox{0ex}[1ex][1ex]{\varphi^{\, }_{e}}\) such that \(S=\textit{dom}(\raisebox{0ex}[1ex][1ex]{\varphi^{\, }_{e}})\). It is known that \(S\) is c.e. iff \(S = \raisebox{0ex}[1ex][1ex]{\varphi^{\, }_{e}}(\mathbb{D})\raisebox{0ex}[1ex][1ex]{\:\triangleq\:}\textit{rng}(\raisebox{0ex}[1ex][1ex]{\varphi^{\, }_{e}})\) for some total computable function \(\raisebox{0ex}[1ex][1ex]{\varphi^{\, }_{e}}\). For a partial computable function \(\raisebox{0ex}[1ex][1ex]{\varphi^{\, }_{e}}\) we denote \(W_e = \textit{dom}(\raisebox{0ex}[1ex][1ex]{\varphi^{\, }_{e}})\). \(S\subseteq \mathbb{D}\) is decidable if and only if \(S\) and \(\raisebox{0ex}[1ex][1ex]{\overline{S}}\) are c.e.. The set of all c.e. sets in \(\mathbb{D}\) is \(\wp^{\text{ce}}(\mathbb{D})\raisebox{0ex}[1ex][1ex]{\:\triangleq\:}\{W_e \in \wp(\mathbb{D}) ~|~ e\in\mathscr{L}\}\). It is known [19] that \(\langle \wp^{\text{ce}}(\mathbb{D}),\subseteq \rangle\) is a distributive lattice with \(\varnothing\) and \(\mathbb{D}\) as, respectively, bottom and top elements and that the set of decidable sets \(\wp^{\text{dec}}(\mathbb{D}) \raisebox{0ex}[1ex][1ex]{\:\triangleq\:}\{S\in \wp(\mathbb{D}) ~|~ S, \raisebox{0ex}[1ex][1ex]{\overline{S}}\in \wp^{\text{ce}}(\mathbb{D})\}\) is a Boolean algebra \(\raisebox{0ex}[1ex][1ex]{\langle \wp^{\text{dec}}(\mathbb{D}),\subseteq \rangle}\). A sequence \(\raisebox{0ex}[1ex][1ex]{\{V_e\}_{e\in\omega}\subseteq\wp^{\text{ce}}(\mathbb{D})}\) is uniformly c.e. if there exists a total computable function \(f:\omega\rightarrow\omega\) such that \(V_e=W_{f(e)}\). Such sequence \(\{W_{f(e)}\}_{e\in\omega}\) is uniformly decidable if the set \(\{(x,e) ~|~ x\in W_{f(e)}\}\) is decidable.

It is known that for any \(n\in\omega\) there exists a primitive computable predicate \({\mathcal{T}}\) of \(n+2\) arguments such that for each \(e\in\mathscr{L}\) and \(x\in\mathbb{D}\): \(\raisebox{0ex}[1ex][1ex]{\varphi^{n\, }_{e}}(x){\downarrow} \Leftrightarrow \exists t.{\mathcal{T}}(e,x,t)\) [22]. Here \({\mathcal{T}}(e,x,t)\) may represent the primitive computable predicate which holds true if the program \(e\in\mathscr{L}\) has terminated its computation in \(t\)-steps in some model of computation for the programming system \(\mathscr{L}\), yet returning the value \(\raisebox{0ex}[1ex][1ex]{\varphi^{n\, }_{e}}(x)\). Given \(e\in\mathscr{L}\) ant \(t\in\omega\) we denote by \({\tt dovetail}(e,t)\subsetneq\mathbb{D}\) the set of all inputs \(x\in \mathbb{D}\) determined in \(t\)-steps of the dovetail procedure such that \(\raisebox{0ex}[1ex][1ex]{\varphi^{\, }_{e}}(x){\downarrow}\). It is known that if \(e\in\mathscr{L}\) then \(W_e=\cup_{t\in\omega}{\tt dovetail}(e,t)\).

Not all elements in \(\wp(\mathbb{D})\) are c.e.: both \(\wp^{\text{ce}}(\mathbb{D})\) and \(\wp^{\text{dec}}(\mathbb{D})\) are denumerable and \(\wp^{\text{dec}}(\mathbb{D})\subsetneq\wp^{\text{ce}}(\mathbb{D})\subsetneq\wp(\mathbb{D})\). A set \(S\in\wp(\mathbb{D})\) is creative if it is c.e. and its complement \(\raisebox{0ex}[1ex][1ex]{\overline{S}}=\mathbb{D}\smallsetminus S\) is productive [23], [24], i.e., there exists a total computable function \(\raisebox{0ex}[1ex][1ex]{\varphi^{\, }_{e}}:\mathscr{L}\rightarrow\mathbb{D}\) such that \(\forall x\in\mathscr{L}. \, W_x\subseteq \raisebox{0ex}[1ex][1ex]{\overline{S}}~\Rightarrow~\raisebox{0ex}[1ex][1ex]{\varphi^{\, }_{e}}(x)\in\raisebox{0ex}[1ex][1ex]{\overline{S}}\smallsetminus W_x\). It is clear that all productive sets are not c.e.. It is also known that, while the complement of a creative set is always productive, the complement of a productive set may be productive, e.g., \(\{e\in \mathscr{L} ~|~ W_e\in\wp^{\text{dec}}(\mathbb{D})\}\) [25]. It is also known that creative sets are complete in \(\wp^{\text{ce}}(\mathbb{D})\), i.e., \(S\in \wp(\mathbb{D})\) is creative iff \(S\in\wp^{\text{ce}}(\mathbb{D})\) and for any \(A\in\wp^{\text{ce}}(\mathbb{D})\), \(A\preceq_f S\). Here for \(A\in \wp(\mathbb{D})\) and \(S\in \wp(\mathbb{D})\), \(A\preceq_f S\) denotes many-to-one reducibility, i.e., the existence of a total computable function \(f:\mathbb{D}\rightarrow\mathbb{D}\) such that for all \(x\in \mathbb{D}\): \(x\in A~\Leftrightarrow~f(x)\in S\). It is known that if \(S\) is productive and \(S\preceq_f X\) then also \(X\) is productive. It is known that \(\raisebox{0ex}[1ex][1ex]{K\raisebox{0ex}[1ex][1ex]{\:\triangleq\:}\{e ~|~ \raisebox{0ex}[1ex][1ex]{\varphi^{\, }_{e}}(e){\downarrow}\}\in\wp^{\text{ce}}(\mathbb{D})}\) is creative and therefore \(\raisebox{0ex}[1ex][1ex]{\raisebox{0ex}[1ex][1ex]{\overline{K}}}\) is productive.

The Kleene arithmetical hierarchy is particularly important to compare properties of programs. We denote by \(\Sigma^0_0=\Pi^0_0=\Delta_0\) the set of all decidable sets, i.e., \(\Sigma^0_0=\Pi^0_0=\Delta_0 = \wp^{\text{dec}}(\mathbb{D})\). For \(n\geq 1\) we define when a set \(A\in \wp(\mathbb{D})\) is arithmetical as follows:

• \(A\in\Sigma^0_n\) if there exists a decidable predicate \(R(x,y_1,\ldots,y_n)\subseteq \mathbb{D}^{n+1}\): \[\begin{align} x\in A~\Leftrightarrow~\exists y_1,\forall y_2\ldots Q y_n.\;& R(x,y_1,\ldots,y_n)\\ &where Q=\exists if n\in 2\omega+1, and Q=\forall if n\in 2\omega. \end{align}\]

• \(A\in\Pi^0_n\) if there exists a decidable predicate \(R(x,y_1,\ldots,y_n)\subseteq \mathbb{D}^{n+1}\): \[\begin{align} x\in A~\Leftrightarrow~\forall y_1,\exists y_2\ldots Q y_n.\;& R(x,y_1,\ldots,y_n)~\\ &where Q=\forall if n\in 2\omega+1, and Q=\exists if n\in 2\omega. \end{align}\]

• \(A\in\Delta_n\) if \(A\in\Sigma^0_n\cap\Pi^0_n\).

We know \(A\in\Sigma^0_n~\Leftrightarrow~\raisebox{0ex}[1ex][1ex]{\overline{A}}\in\Pi^0_n\), \(A\in\Sigma^0_n\cup\Pi^0_n\Rightarrow\forall m>n.\; A\in\Delta_{m}=\Sigma^0_m\cap\Pi^0_m\), \(B\preceq_f A~\wedge~ A\in\Sigma^0_n\Rightarrow B\in\Sigma^0_n\), and \(\raisebox{0ex}[1ex][1ex]{R\in\Sigma^0_{n>0}}~ \Rightarrow~ \{x ~|~ \exists y.\;R(x,y)\}\in\Sigma^0_n\) [20].

2.3.3 Program semantics.↩︎

Although in the following \(\mathscr{L}\) can be any acceptable programming system, we sometimes consider \(\mathscr{L}=\tt Imp\), where \(\tt Imp\) is a simple while-programming language with arithmetic \({\tt Exp}\) and Boolean \({\tt BExp}\) expressions (see [26]), whose syntax is as follows: \[\begin{align} {\tt Exp} \ni a ::= &\; v\in\mathbb{D}\mid x\in \mathit{Var}\mid f(a)\mid W \\ {\tt BExp} \ni b ::= &\; {\tt true}\mid {\tt false} \mid a =a \mid a > a\mid b\wedge b\mid\neg b\mid R\\ {\tt Imp}\ni p ::= &\;{\tt skip}\mid x:=\mathit{a}\mid p;p\mid {\tt if} ~b~ {\tt then} ~p~ {\tt else} ~p \mid {\tt while} ~b~ \{ ~p~\} \end{align}\] where \(f\) ranges over partial computable functions, \(R\) ranges over decidable predicates and \(W\) ranges over arbitrary decidable sets of elements in \(\mathbb{D}\). In this case \(\mathbb{D}\) contains basic values (e.g., integers in \(\mathbb{Z}\), booleans in \(\{{\tt true, false}\}\), finite sets, etc.). Let \(\mathbb{S}\) denotes the set of all stores \(\sigma:\mathit{Var}\rightarrow\mathbb{D}\), i.e., total computable functions that assign values in \(\mathbb{D}\) to finite vectors of variables in \(\mathit{Var}\). When \(S\subseteq\mathbb{S}\) is a set of stores then a predicate transformer semantics of a program \(p\in\tt Imp\) can be inductively defined as usual as follows \({\llbracket p \rrbracket}: \wp(\mathbb{S})\rightarrow\wp(\mathbb{S})\) where: \[\begin{align} {\llbracket {\tt skip} \rrbracket}S &\triangleq S\\ {\llbracket x:=\mathit{a} \rrbracket}S &\triangleq\{\;\sigma[x\mapsto {\llbracket \mathit{a} \rrbracket}\sigma] \mid \sigma \in S\;\}\\ {\llbracket p_1 ; p_2 \rrbracket} S &\triangleq{\llbracket p_2 \rrbracket}({\llbracket p_1 \rrbracket}S)\\ {\llbracket {\tt if}\;\mathit{b}\;{\tt then}\;p_1\;{\tt else}\;p_2 \rrbracket}S &\triangleq{\llbracket p_1 \rrbracket}({\llbracket \mathit{b} \rrbracket}S) \cup {\llbracket p_2 \rrbracket}({\llbracket \neg\mathit{b} \rrbracket}S)\\ {\llbracket {\tt while}\;\mathit{b}\; \{\;p\;\} \rrbracket}S &\triangleq{\llbracket \neg \mathit{b} \rrbracket}\big({\sf lfp\/}(\lambda T.\: S \cup {\llbracket p \rrbracket}({\llbracket \mathit{b} \rrbracket}T))\big). \end{align}\] In this case \({\llbracket b \rrbracket}S=\{\sigma\in S ~|~ \sigma\models b\}\), where \(\sigma\models b\) holds when the store \(\sigma\) viewed as a substitution satisfies \(b\), and \({\llbracket a \rrbracket}S=\{{\llparenthesis a \rrparenthesis}\sigma ~|~ \sigma\in S\}\), where \({\llparenthesis a \rrparenthesis}\sigma\in\mathbb{D}\) is the value that the expression \(a\) can take with store \(\sigma\). We assume the total computable functions \({\tt input}:\mathit{Var}\times\mathbb{D}\rightarrow\mathbb{S}\) and \({\tt out}:\mathit{Var}\times\mathbb{S}\rightarrow\mathbb{D}\) such that \({\tt input}(x,v)\) builds the input store mapping \(x\) to \(v\) and \({\tt out}(x,\sigma) = \sigma(x)\), where \(x\) is some output vector of variables. We assume that the output vector of variables belongs to the set of free variables of the program \(e\), devoted \(FV(e)\), and it will be omitted when this is obvious by the context or not relevant. For any \(e\in\tt Imp\), we have then \(\raisebox{0ex}[1ex][1ex]{\varphi^{\, }_{e}}\raisebox{0ex}[1ex][1ex]{\:\triangleq\:}\lambda x.\,{\tt out}(FV(e),{\llbracket e \rrbracket}(\{{\tt input}(FV(e),x)\}))\).

2.4 Abstract interpretation↩︎

2.4.1 Abstract domains.↩︎

In standard Galois connection based abstract interpretation [1], [2], abstract domains (also called abstractions) are specified by Galois connections/insertions (GCs/GIs for short). Concrete and abstract domains are usually complete lattices, resp.\(\langle C,\leq_C \rangle\) and \(\langle A,\leq_A \rangle\), which are related by abstraction and concretization maps \(\alpha:C\rightarrow A\) and \(\gamma:A \rightarrow C\) that give rise to a GC \((\alpha,C,A,\gamma)\) (\(\langle \alpha,\gamma \rangle\) for short), that is, for all \(a\in A\) and \(c\in C\), \(\alpha(c) \leq_A a \Leftrightarrow c \leq_C \gamma(a)\). A GC is a GI when \(\alpha\circ\gamma=\lambda x.x\). In the following we assume GIs only. Let us recall some basic properties of a GI \((\alpha,C,A,\gamma)\): (1) \(\alpha\) is additive and \(\gamma\) is co-additive; (2) \(\gamma\circ \alpha: C\rightarrow C\) is an upper closure operator, namely, it is a monotone, idempotent and increasing (i.e., \(x \leq \gamma(\alpha(x))\)) function; (3) if \(\mu:C\rightarrow C\) is an upper closure operator then \((\mu,C,\mu(C),\lambda x.x)\) is a GI. If \(\alpha:C\rightarrow A\) is an additive function then it induces a GC \((\alpha,C,A,\alpha^+)\) where the concretization \(\alpha^+:A \rightarrow C\) is defined as right-adjoint of \(\alpha\), i.e., \(\alpha^+(a) \triangleq\vee_C \{c\in C ~|~ \alpha(c) \leq_A a\}\). Dually, if \(\gamma:C\rightarrow A\) is a co-additive function then \((\gamma^-,C,A,\gamma)\) is a GC where \(\gamma^- \triangleq\lambda c. \wedge_A \{a\in A ~|~ c \leq_C \gamma(a)\}\) is the left-adjoint of \(\gamma\).

We use \(\mathop{\mathrm{Abs}}(C)\) to denote all the possible abstractions of a concrete domain \(C\), where \(A\in \mathop{\mathrm{Abs}}(C)\) means that \(A\) is an abstract domain of \(C\) defined by some GI which is left unspecified, and \(\raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}\) is its corresponding upper closure operator. If \(A_1,A_2\in \mathop{\mathrm{Abs}}(C)\) then \(A_1\) is equivalent to \(A_2\), denoted by \(A_1\sim A_2\), when \(\gamma_{A_1}(A_1) = \gamma_{A_2}(A_2)\). The quotient \(\mathop{\mathrm{Abs}}(C)_{/\sim}\) is called the lattice of abstractions because it turns out to be a complete lattice when \(C\) is a cpo [27] w.r.t.the relative precision ordering: \(A_1 \sqsubseteq A_2\) iff for any \(c\in C\), \(\gamma_{A_1}(\alpha_{A_1}(c)) \leq_C \gamma_{A_2}(\alpha_{A_2}(c))\). \(\mathop{\mathrm{Abs}}(C)_{/\sim}\) is indeed isomorphic to the lattice of upper closure operators \(\mathrm{uco}(C)\) on the concrete lattice \(\langle C,\leq_C \rangle\). Thus, \(A_1 \sqsubseteq A_2\) means that \(A_1\) is a more precise abstraction than \(A_2\), or, equivalently, that \(A_2\) abstracts \(A_1\). An abstract domain \(A\in \mathop{\mathrm{Abs}}(C)\) is called trivial when \(A\) is either the least or the greatest abstract domain in \(\langle \mathop{\mathrm{Abs}}(C)_{/\sim},\sqsubseteq \rangle\), respectively \(\raisebox{0ex}[1ex][1ex]{\rho^{}_{A}} = \lambda x.x\) (called the identical abstraction) or \(\raisebox{0ex}[1ex][1ex]{\rho^{}_{A}} = \lambda x.\top_C\), called the top abstraction and denoted \(A=\top\). We say that \(A\) is continuous when \(\raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}\) is continuous.

2.4.2 Soundness and Completeness.↩︎

Let \(f:C\rightarrow C\) be a concrete monotone function—for simplicity we consider unary functions—and let \(\raisebox{0ex}[1ex][1ex]{f^\sharp:A \rightarrow A}\) be a corresponding monotone abstract function defined on \(A\in \mathop{\mathrm{Abs}}(C)\) with GI \(\langle \alpha,\gamma \rangle\). \(\raisebox{0ex}[1ex][1ex]{f^\sharp}\) is a correct (or sound) approximation of \(f\) on \(A\) when \(\raisebox{0ex}[1ex][1ex]{\alpha \circ f \sqsubseteq f^\sharp\circ \alpha}\) holds. If \(\raisebox{0ex}[1ex][1ex]{f^\sharp}\) is correct for \(f\) then it is fix-point correct, that is, \(\alpha({\sf lfp\/}(f)) \leq_A {\sf lfp\/}(\raisebox{0ex}[1ex][1ex]{f^\sharp})\) holds. The abstract function \(\raisebox{0ex}[1ex][1ex]{f^A \raisebox{0ex}[1ex][1ex]{\:\triangleq\:}\alpha \circ f \circ \gamma: A\rightarrow A}\) is called the best correct approximation (bca for short) of \(f\) on \(A\), because it turns out that any abstract function \(\raisebox{0ex}[1ex][1ex]{f^\sharp}\) is a correct approximation of \(f\) iff \(\raisebox{0ex}[1ex][1ex]{f^A \sqsubseteq f^\sharp}\). Hence, \(\raisebox{0ex}[1ex][1ex]{f^A}\) plays the role of the best possible correct approximation of \(f\) on the abstract domain \(A\) [2]. The tuple \(\langle f,A,\raisebox{0ex}[1ex][1ex]{f^\sharp} \rangle\) fully defines an abstract interpretation. It is (globally) complete when \(\raisebox{0ex}[1ex][1ex]{\alpha \circ f = f^\sharp \circ \alpha}\) [2], [3]. When \(\raisebox{0ex}[1ex][1ex]{f^\sharp}\) is an abstract transfer function on \(A\) used by some static program analysis, completeness intuitively encodes an optimal precision for \(\raisebox{0ex}[1ex][1ex]{f^\sharp}\), meaning that the abstract behavior of \(\raisebox{0ex}[1ex][1ex]{f^\sharp}\) on \(A\) exactly matches the abstraction in \(A\) of the concrete behavior of \(f\). If \(\raisebox{0ex}[1ex][1ex]{f^\sharp}\) is complete for \(f\) then least fix-point completeness holds (also called fix-point transfer), i.e., \(\alpha({\sf lfp\/}(f)) = {\sf lfp\/}(\raisebox{0ex}[1ex][1ex]{f^\sharp})\) holds. It turns out that completeness \(\raisebox{0ex}[1ex][1ex]{\alpha \circ f = f^\sharp \circ \alpha}\) holds iff \(\raisebox{0ex}[1ex][1ex]{\alpha\circ f = (\alpha\circ f\circ\gamma)\circ \alpha = f^A \circ \alpha}\) holds. This corresponds precisely to ask that the following equation holds for all \(x\in C\): \[\label{basic-completeness} \raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}(f(\raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}(x)))=\raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}(f(x)).\tag{1}\] When (1 ) holds only for a subset \(S\) of the input domain, i.e., for all \(x\in S\subseteq C\), then \(\langle f,A,\raisebox{0ex}[1ex][1ex]{f^\sharp} \rangle\) is locally complete w.r.t.\(S\) [10]. Of course local completeness is in general a weaker property than completeness. Let us recall that function composition preserves completeness, that is, if \(f\) and \(g\) are complete on \(A\) then \(f\circ g\) is complete on \(A\). It has been recently proved that local completeness plays a key role in guaranteeing that the composition of bca’s is still a bca [13], i.e., \(f_1^{A}\;\circ\normalsizef_2^{A} = (f_1\;\circ\normalsizef_2)^{A}\). In both cases, the possibility of defining a complete approximation \(\raisebox{0ex}[1ex][1ex]{f^\sharp}\) of \(f\) on some \(A\in \mathop{\mathrm{Abs}}(C)\) only depends upon the concrete function \(f\) and on the abstraction \(A\), that is, \(\raisebox{0ex}[1ex][1ex]{f^A}\) is the only possible option as complete approximation of \(f\). Therefore if \(\raisebox{0ex}[1ex][1ex]{f^\sharp}\) is complete this implies that \(\raisebox{0ex}[1ex][1ex]{f^\sharp=f^A}\) while if \(\raisebox{0ex}[1ex][1ex]{f^A}\) is not complete then no abstract interpretation \(\raisebox{0ex}[1ex][1ex]{f^\sharp}\) exists which can be complete.

3 Abstract interpretation in standard recursion theory↩︎

Standard recursion theory is a theory of sets (properties) and functions indexed on elements of a programming system, i.e., programs. In the following we consider abstract interpretation in the context of partial computable functions. In this case \(A\in\mathop{\mathrm{Abs}}(\wp^{\text{ce}}(\mathbb{D}))\), meaning that we are only interested in abstractions of properties of programs, i.e., of properties \(W_e\in \wp^{\text{ce}}(\mathbb{D})\) for some \(e\in\mathscr{L}\). When abstract interpretation is applied to program analysis or automated program verification, the abstraction is intended to associate with each program under inspection a decidable approximation of its often undecidable semantics. This is because the analysis of programs requires decidable answers to undecidable questions such as those expressed as extensional properties of programs and concerning their dynamic behavior.

The notion of decidable abstract interpretation has been studied in [28] for the comparison of the difficulty in analyzing and verifying programs. The notion of decidable abstraction in [28] specifies an abstract domain as a collection of recursive sets (properties) such that the relation of sub-set inclusion is decidable. We follow [28] and define \(A\) decidable when for all \(e\in\mathscr{L}\), \(\raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}(W_e)\) is decidable. Note that among the trivial abstractions only \(A=\{\mathbb{D}\}\), i.e., \(\raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}=\lambda x.\mathbb{D}\), is decidable. \(\raisebox{0ex}[1ex][1ex]{\rho^{}_{A}} = \lambda x.x\) is indeed clearly not decidable. It is also worth noting that decidability does not imply that \(\{\raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}(W_e)\}_{e\in\mathscr{L}}\) is uniformly decidable. This would require that we can decide whether \(x\in\raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}(W_e)\) uniformly on both \(x\in\mathbb{D}\) and \(e\in\mathscr{L}\). Next result proves that the set \(\{(x,i) ~|~ x\in\raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}(W_i)\}\) is decidable if and only if \(\raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}=\lambda x.\mathbb{D}\), i.e., \(A\) is the only trivial decidable abstraction.

Proof. Assume \(\{\raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}(W_e)\}_{e\in\mathscr{L}}\) is uniformly decidable and \(\raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}\neq\lambda x.\mathbb{D}\). This means that \(\{(x,i) ~|~ x\in\raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}(W_i)\}\) is decidable and there exists \(i\in\mathscr{L}\) and \(\dot{x}\in\mathbb{D}\) such that \(\dot{x}\not\in \raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}(W_i)\). Consider the set \(S_{\dot{x}}\raisebox{0ex}[1ex][1ex]{\:\triangleq\:}\{i ~|~ \dot{x}\not\in \raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}(W_i)\}\subseteq\mathscr{L}\). It is clear that \(S_{\dot{x}}\) is an extensional property because if \(e\in S_{\dot{x}}\) then \(\dot{x}\not\in \raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}(W_e)\) and if \(\raisebox{0ex}[1ex][1ex]{\varphi^{\, }_{e}}\cong\raisebox{0ex}[1ex][1ex]{\varphi^{\, }_{j}}\) then \(W_e=W_j\), therefore \(\dot{x}\not\in \raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}(W_j)\), i.e., \(j\in S_{\dot{x}}\). By Rice’s theorem \(S_{\dot{x}}\) is decidable if and only if \(S_{\dot{x}}=\varnothing\) or \(S_{\dot{x}}=\mathscr{L}\), but none of these hold because: (1) the program \(*\) in Fig. 1 is such that \(W_*=\varnothing\) therefore because \(\varnothing\subseteq W_i\) then by monotonicity \(\raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}(W_*)\subseteq \raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}(W_i)\) which implies that \(\dot{x}\not\in \raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}(W_*)\) and therefore \(*\in S_{\dot{x}}\), and (2) the program \(p\) in Fig. 1 is such that \(W_p=\{\dot{x}\}\) which implies that \(\dot{x}\in \raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}(W_p)\), hence \(p\not\in S_{\dot{x}}\). Q.E.D.

 ◻

We introduce the notion of a uniform closure operator as the effective counterpart of an upper closure operator: a transformation on program indices that realizes, at the level of programs, the closure induced by an abstract domain on the underlying semantic objects.

The following proposition proves that continuous and decidable abstract domains induce decidable uniform closure operators on \(\mathscr{L}\).

Uniformity plays a key role in viewing abstract interpretation within computability theory because it expresses the fact that the abstraction function, in our case expressed by the closure operator \(\raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}\), is itself defined by an algorithm (or a finite set of algorithms) that act uniformly and continuously over any input c.e. property. This is the case when \(\raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}\) does not only encode the closure operation induced by a Galois insertion \(\langle \alpha,\gamma \rangle\), i.e., when \(\raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}=\gamma\alpha\), but also the algorithm that computes the abstraction, i.e., that transforms a c.e. property \(W_i\) into its abstraction \(\raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}(W_i)\). In this sense, the hypothesis of continuity precisely corresponds to the effective computability of the abstraction operation. As observed above in Theorem 1, if \(r_{A}\) is a decidable uniform closure operator associated with a decidable abstract domain \(A\), the uniform c.e. sequence \(\{W_{r_{A}(i)}\}_{i\in\mathscr{L}}\) cannot be uniformly decidable unless \(r_{A}\) maps any program \(i\in\mathscr{L}\) into an always terminating program, i.e., \(W_{r_{A}(i)}=\mathbb{D}\), e.g., \(r_{A}(i)={\tt skip}\).

It is important to observe that the construction of the set \(W_{{\tt int}(p,i)}\) corresponds precisely to dynamically checking the computed bounds of the program \(i\). This is indeed achieved by sand-boxing, by the program transformation \({\tt int}\), the code of \(i\) within \(p\), as common practice in dynamic program analysis. This is the case of Daikon, a well-known tool for dynamic detection of approximate program invariants. Daikon infers likely invariants from executions, and these invariants can then be used for documentation, testing, or static checking [29].

It is obvious by Rice’s theorem that the above uniform closure \({\tt int}\) is decidable but not uniformly decidable, i.e., the set \(\{(x,i) ~|~ x\in W_{{\tt int}(p,i)}\}\) is in general not decidable (because for \(x\in\mathbb{D}\) the set \(\{i ~|~ x\in W_{{\tt int}(p,i)}\}\) is extensional). It is worth noting that if we replace \(\raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}(W_i)\) with any upper approximations of \(W_i\) as induced by a decidable abstract interpretation defined on \(A\) (e.g., by employing widening operations on intervals [1]) we cannot have as result a uniform closure operator. Denote the decidable abstract semantics defined by a terminating abstract interpretation on an abstract domain \(A\) as \(\raisebox{0ex}[1ex][1ex]{{\llbracket \cdot \rrbracket}^A:\mathscr{L}\timesA\rightarrowA}\). It is clear that the set \(\raisebox{0ex}[1ex][1ex]{\{(x,i) ~|~ x\in\gamma({\llbracket i \rrbracket}^A(\top_A))\}}\) is now decidable, but any total computable function \(s\) obtainable by s-m-n theorem and mapping \(i\in\mathscr{L}\) into the index \(s(i)\) such that \(\raisebox{0ex}[1ex][1ex]{W_{s(i)}=\gamma({\llbracket i \rrbracket}^A(\top_A))}\) cannot be in general a uniform closure. This is because by monotonicity this would imply that the abstract semantics \(\raisebox{0ex}[1ex][1ex]{{\llbracket i \rrbracket}^A}\) induces an extensional equivalence relation on \(\mathscr{L}\) and we know that this holds for trivial abstractions only [9]. Consequently, a uniform closure operator can only arise from an upper closure operator \(\raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}\), namely uniformity is an intrinsic property of the abstract domain, not of any decidable abstract semantics that can be constructed over it.

Because of these observations, throughout the following discussion, the decidable set \(\raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}(W_i)\), that corresponds to an element of the abstract domain \(A\), is always considered relative to a fixed and known property \(W_i\). \(W_i\) can be a decidable specification for some pre/post condition property or an intermediate property of the computation. The index \(i\) will therefore only denote any known program representing that property.

4 Classes of completeness and incompleteness↩︎

In this section, we characterize the computational properties of the sets of programs for which, given fixed abstract domain \(A\), the corresponding bca is locally complete. This naturally recalls the stronger notion of (global) completeness class firstly introduced in [15] and corresponding to the class of all programs for which a given abstract domain \(A\) is globally complete: \[{\mathbb{C}}(A) \triangleq\{e\in\mathscr{L} ~|~ \forall i\in\mathscr{L}.\, \raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}(\raisebox{0ex}[1ex][1ex]{\varphi^{\, }_{e}}(W_i)) = \raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}(\raisebox{0ex}[1ex][1ex]{\varphi^{\, }_{e}}(\raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}(W_i)))\}.\] It is worth noting that \({\mathbb{C}}(A)\), and hence also \(\raisebox{0ex}[1ex][1ex]{\overline{{\mathbb{C}}(A)}}\), are extensional properties of programs in \(\mathscr{L}\), namely: \(e\in {\mathbb{C}}(A)~\wedge~\raisebox{0ex}[1ex][1ex]{\varphi^{\, }_{e}}\cong\raisebox{0ex}[1ex][1ex]{\varphi^{\, }_{i}}~\Rightarrow~i\in{\mathbb{C}}(A)\). In [15] Giacobazzi et al., proved that for a programming system \(\mathscr{L}\) defined in terms of a simple imperative programming language à la \(\tt Imp\) ::

• \(|{\mathbb{C}}(A)| = \aleph_0\);

• \({\mathbb{C}}(A)\) is decidable if and only if \(A\) is trivial²;

• \(A\) not trivial \(\Rightarrow\) \({\mathbb{C}}(A)\) and \(\raisebox{0ex}[1ex][1ex]{\overline{{\mathbb{C}}(A)}}\) are productive sets, hence non c.e..

By the fundamental isomorphism theorem [30], between any two acceptable programming systems there is an effective, one-to-one, and onto translation, hence because \(\tt Imp\) is an acceptable programming system, any acceptable programming system satisfies the above three properties. In particular if \(*\in\mathscr{L}\) and \({\tt id}\in\mathscr{L}\) denote respectively a program such that for all \(x\in\mathbb{D}:\,\raisebox{0ex}[1ex][1ex]{\varphi^{\, }_{*}}(x){\uparrow}\) and \(\raisebox{0ex}[1ex][1ex]{\varphi^{\, }_{*}}(x)=x\) (e.g., see Fig. 1), then \(*,{\tt id}\in {\mathbb{C}}(A)\).

Things are more complicated when we move from global completeness to the weaker notion of local completeness. We introduce the notion of local completeness class as the set of all programs for which its bca is locally complete with respect a fixed input c.e. property \(W_i\).

The local completeness class above naturally extends to sets of inputs as follows: let \(S\subseteq\mathscr{L}\) then the local completeness class of \(A\) with respect to \(S\) is \[{\mathbb{C}}(A,S)=\bigcap_{i\in S}{\mathbb{C}}(A,i).\] It is immediate to observe that if \(S\subseteq R~\Rightarrow~{\mathbb{C}}(A,R)\subseteq{\mathbb{C}}(A,S)\), and for any \(S\subseteq\mathscr{L}\): \({\mathbb{C}}(A)\subseteq{\mathbb{C}}(A,S)\), and \({\mathbb{C}}(A)={\mathbb{C}}(A,\mathscr{L})\).

The proof of the following theorem follows the structure of the proof of a similar result for the global completeness case in [15] and immediately extends that result to the case of local completeness.

An immediate consequence of this result is that, similar to the case of global completeness, for any input \(W_i\) that is not precisely represented in the abstract domain, i.e., such that \(W_i\neq\raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}(W_i)\), \({\mathbb{C}}(A,i)\) and its complement \(\raisebox{0ex}[1ex][1ex]{\overline{{\mathbb{C}}(A,i)}}\) are decidable if and only if \(A=\top\). Moreover, because \({\mathbb{C}}(A,i)\) is extensional, there always exist infinitely many programs for which the given abstraction is locally incomplete. In view of this observation, because an abstract interpretation is (locally) complete if and only if the corresponding bca is complete (see [3][Lemma 3.1]), any abstract interpretation built on an abstraction \(A\) is locally complete for all programs if and only if \(A=\top\).

Theorem 2 implies that when \(W_i\neq\raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}(W_i)\) and \(A\neq\top\) (which implies that \(A\) is not trivial) both \({\mathbb{C}}(A,i)\) and \(\raisebox{0ex}[1ex][1ex]{\overline{{\mathbb{C}}(A,i)}}\) cannot be acceptable programming systems. On one side its is obvious that \(*,{\tt id}\in {\mathbb{C}}(A,i)\). On the other side Theorem 2 proved that any program \(e\in\mathscr{L}\) such that \[\label{incomplete-prog} \raisebox{0ex}[1ex][1ex]{\varphi^{\, }_{e}}(x)\raisebox{0ex}[1ex][1ex]{\:\triangleq\:}\left\{ \begin{array}{ll} b & if x=a\\ \uparrow &otherwise \end{array} \right .\tag{2}\] with \(a\in \raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}(W_i)\setminus W_i\) and \(b\in\mathbb{D}\setminus\raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}(W_o)\), we have \(e\in\raisebox{0ex}[1ex][1ex]{\overline{{\mathbb{C}}(A,i)}}\). Consider the following total computable function: \[\label{selection} \raisebox{0ex}[1ex][1ex]{\varphi^{\, }_{s}}(a,b,c,x)\raisebox{0ex}[1ex][1ex]{\:\triangleq\:}\left\{ \begin{array}{ll} b & if x=a\\ c &otherwise \end{array} \right .\tag{3}\] When \(a,b,c\) are fixed as above, by the s-m-n theorem we have that there exists a total computable function \(g\) such that \(\raisebox{0ex}[1ex][1ex]{\varphi^{\, }_{g(s,a,b,c)}}(x)\cong\raisebox{0ex}[1ex][1ex]{\varphi^{\, }_{s}}(a,b,c,x)\). It is immediate to prove by the same argument above that if \(c\in W_o\) (i.e., \(W_o\neq\varnothing\)) then \(g(s,a,b,c)\in\raisebox{0ex}[1ex][1ex]{\overline{{\mathbb{C}}(A,i)}}\). This implies that both \({\mathbb{C}}(A,i)\) and \(\raisebox{0ex}[1ex][1ex]{\overline{{\mathbb{C}}(A,i)}}\) do not satisfy the axioms of Wagner’s Uniform Reflexive Structures (URS) [31] that model the essential properties of acceptable gödelizations, hence of acceptable programming systems. In particular for \(\raisebox{0ex}[1ex][1ex]{\overline{{\mathbb{C}}(A,i)}}\) we have that \(*\not\in \raisebox{0ex}[1ex][1ex]{\overline{{\mathbb{C}}(A,i)}}\) hence \(\raisebox{0ex}[1ex][1ex]{\overline{{\mathbb{C}}(A,i)}}\) violates Axiom 1 of URS requiring that the always undefined function has to be represented in any URS. Moreover for \({\mathbb{C}}(A,i)\) we have that if \(a\in \raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}(W_i)\setminus W_i\), \(b\in\mathbb{D}\setminus\raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}(W_o)\) and \(c\in W_o\) then \(g(s,a,b,c)\not\in {\mathbb{C}}(A,i)\) hence \({\mathbb{C}}(A,i)\) violates Axiom 2 of URS requiring that the function \(\lambda a,b,c.\,g(s,a,b,c)\) performing selection for all \(a,b,c\neq *\) has to be represented in any URS. For exactly the same reasons also \(\raisebox{0ex}[1ex][1ex]{\overline{{\mathbb{C}}(A)}}\) and \({\mathbb{C}}(A)\) cannot be acceptable programming systems. This observation implies that no matter if global or local completeness is concerned, neither completeness nor incompleteness classes can be considered as acceptable programming systems (hence languages) for partial computable functions, this independently from the equational theory used to specify the function in 3 , unless for the cases of \({\mathbb{C}}(A,i)\) and \({\mathbb{C}}(A)\) only, \(A\) is trivial, i.e., \({\mathbb{C}}(A,i)={\mathbb{C}}(A)=\mathscr{L}\).

4.1 The hardness of local completeness↩︎

As in the case of global completeness, we can go beyond and prove that \({\mathbb{C}}(A,i)\) is indeed a bi-productive set under some hypothesis on \(i\in\mathscr{L}\) and \(A\).

It is worth noting that the productivity of \({\mathbb{C}}(A,i)\) does not require \(W_i\neq\varnothing\), which is instead required in the proof of case \(\raisebox{0ex}[1ex][1ex]{\raisebox{0ex}[1ex][1ex]{\overline{{\mathbb{C}}(A,i)}}}\). This is because if \(\raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}(\varnothing)\in\wp^{\text{dec}}(\mathbb{D})\) (e.g., when \(A\) is decidable) and \(W_i=\varnothing\) the set \(\raisebox{0ex}[1ex][1ex]{\raisebox{0ex}[1ex][1ex]{\overline{{\mathbb{C}}(A,i)}}}\) is indeed c.e..

4.2 \({\mathbb{C}}(A,i)\) and \(\raisebox{0ex}[1ex][1ex]{\overline{{\mathbb{C}}(A,i)}}\) in the arithmetical hierarchy↩︎

Although abstract interpretation theory ([2]) is defined independently from the assumption of dealing with c.e. properties, this assumption is implicit in most of these works for the obvious reason that when applied to program analysis and verification, properties concern the semantics of programs, which are by definition c.e. sets. With this assumption we were able to prove that when the input property does not represent non-terminating computations, i.e., \(W_i\neq\varnothing\) and \(A\) is not trivial then \({\mathbb{C}}(A,i)\) is bi-productive. This gives a lower bound in the arithmetic hierarchy for \({\mathbb{C}}(A,i)\) and its complement \(\raisebox{0ex}[1ex][1ex]{\overline{{\mathbb{C}}(A,i)}}\). In particular if we consider the predicate: \[\mathscr{C}(e,i) \iff \raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}(\raisebox{0ex}[1ex][1ex]{\varphi^{\, }_{e}}(\raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}(W_i))) = \raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}(\raisebox{0ex}[1ex][1ex]{\varphi^{\, }_{e}}(W_i))\] then clearly \(\mathscr{C}(e,i)\) sits at level \(\geq 2\) in the arithmetical hierarchy, i.e., \(\mathscr{C}(e,i)\in \Sigma_{n}^0\cup\Pi_{n}^0\) with \(n\geq 2\). Instead, when \(W_i=\varnothing\) we proved that \(\raisebox{0ex}[1ex][1ex]{\overline{{\mathbb{C}}(A,i)}}\) is a creative set, i.e., \(\raisebox{0ex}[1ex][1ex]{\overline{{\mathbb{C}}(A,i)}}\) is c.e. and \({\mathbb{C}}(A,i)\) is productive (co-re). This means that when \(W_i=\varnothing\) then \(\raisebox{0ex}[1ex][1ex]{\overline{{\mathbb{C}}(A,i)}}\in\Sigma_1^0\) and \({\mathbb{C}}(A,i)\in\Pi_1^0\).

In order to prove more properties about local completeness classes, such as a tightest inclusion in the arithmetic hierarchy or the possibility of having a c.e. representation of the productive set \({\mathbb{C}}(A,i)\), we need more structure on the construction of the abstraction function, such that the fact that \(\{\raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}(W_i) ~|~ i\in\mathscr{L}\}\) is a uniformly c.e. sequence of recursive sets, as proved in Section 3.

Assume \(A\) be decidable and continuous with decidable corresponding uniform closure \(r_{A}\) and \(h:\mathscr{L}\rightarrow\mathscr{L}\) a total computable function such that \[W_{h(e,i)} \;=\; \raisebox{0ex}[1ex][1ex]{\varphi^{\, }_{e}}(W_{i}) \;=\; \{\raisebox{0ex}[1ex][1ex]{\varphi^{\, }_{e}}(x) ~|~ x \in W_{i} \;\land\; \raisebox{0ex}[1ex][1ex]{\varphi^{\, }_{e}}(x){\downarrow}\}.\] In this case: \[\mathscr{C}_A(e,i) \;\iff\; W_{r_{A}(h(e,\,r_{A}(i)))} \subseteq W_{r_{A}(h(e,\,i)))}.\] It is clear that given a fixed index \(i\in\mathscr{L}\): \[\begin{align} {\mathbb{C}}(A,i) \;&=\; \{e ~|~ \mathscr{C}(e,i)\},\\[1ex] \raisebox{0ex}[1ex][1ex]{\overline{{\mathbb{C}}(A,i)}} \;&=\; \{e ~|~ \neg\mathscr{C}(e,i)\},\\[1ex] {\mathbb{C}}(A) \;&=\; \{e ~|~ \forall i.\; \mathscr{C}(e,i)\}, \\[1ex] \raisebox{0ex}[1ex][1ex]{\overline{{\mathbb{C}}(A)}} \;&=\; \{e ~|~ \exists i.\; \neg\mathscr{C}(e,i)\}. \end{align}\]

It is worth noting that the properties of decidability, continuity and non triviality are shared by the abstract domains of most of the Galois-connection based abstract interpretations [28]. The proof of the following theorem is therefore immediate by Lemma 1 and it places all the non-trivial completeness and incompleteness classes into the arithmetic hierarchy.

5 Computable coverings and program transformations↩︎

The interesting consequence of decidable abstract domains—as those employed in static program analysis, is that it is possible to algorithmically extract a c.e. (and therefore also a decidable) covering of the productive set \({\mathbb{C}}(A,i)\). In general, this cannot be achieved for \(\raisebox{0ex}[1ex][1ex]{\overline{{\mathbb{C}}(A,i)}}\). The reason is that, for every program \(e \in \mathscr{L}\), there may be a potentially infinite family of effective transformations mapping \(e\) to programs \(f(e)\) such that \(f(e) \in \raisebox{0ex}[1ex][1ex]{\overline{{\mathbb{C}}(A,i)}}\). Moreover, different choices of \(f(e)\) may compute different functions \(\raisebox{0ex}[1ex][1ex]{\varphi^{\, }_{f(e)}}\), so there is no canonical effective transformation that uniformly represents all such cases. We show that there exists a transformation that employs a constant growth in program size and minimal computational complexity.

5.1 Computable coverings of \({\mathbb{C}}(A,i)\)↩︎

For \({\mathbb{C}}(A,i)\) it is possible to algorithmically “cancel” the outputs causing incompleteness from any partial computable function, yet obtaining an effective enumeration of a set of programs that represents all partial computable functions computable by programs in \({\mathbb{C}}(A,i)\). This is obtained by removing from the range of \(\raisebox{0ex}[1ex][1ex]{\varphi^{\, }_{e}}\) all those outputs of \(e\) that, coming from the approximation of \(W_i\) according to \(\raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}\), namely from \(\raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}(W_i)\), end up outside the approximation of the range of \(e\) on input \(W_i\), i.e., outside \(\raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}(\raisebox{0ex}[1ex][1ex]{\varphi^{\, }_{e}}(W_i))\). We prove that this program transformation is effective, therefore producing a c.e. cover for \({\mathbb{C}}(A,i)\).

The theorem above says that the local completeness class \({\mathbb{C}}(A,i)\), when it is not straightforward, admits a c.e. cover when \(A\) is a decidable and continuous abstract domain. \(\cC_i\) is a family of programs that fully represent the functions computed by the programs in \({\mathbb{C}}(A,i)\) and these programs can be effectively build by the total computable function \(\lambda e.\,g(q,e):\mathscr{L}\rightarrow\mathscr{L}\) that transforms any, possibly incomplete, program \(e\) into a complete one \(g(q,e)\) by canceling those outputs that produce incompleteness. Here decidability plays a key role because it allows us to decide whether any concrete state \(x\) belongs to the abstract input property \(\raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}(W_i)\). Without this assumption the function \(\raisebox{0ex}[1ex][1ex]{\varphi^{\, }_{g(q,e)}}\) is not computable and hence the map \(e\mapsto g(q,e)\) does not exist.

Interestingly, Theorem 5 gives also the very first fix-point characterization of local completeness: \({\mathbb{C}}(A,i)=\{e ~|~ \raisebox{0ex}[1ex][1ex]{\varphi^{\, }_{e}}\cong\raisebox{0ex}[1ex][1ex]{\varphi^{\, }_{g(q,e)}}\}\). This immediately implies that \({\mathbb{C}}(A,i)\neq\varnothing\), \(|{\mathbb{C}}(A,i)|=\aleph_0\), and \({\mathbb{C}}(A,i)\in\Pi^0_2\).

Because it is known that every c.e. set of indexes of partial computable functions \(S\) admits a decidable subset \(B\subseteq S\) which covers \(S\) [14], and this set \(B\) can be effectively enumerated, then the following corollary follows immediately.

5.2 Making programs incomplete by regular translations↩︎

We cannot in general build a c.e. cover for \(\raisebox{0ex}[1ex][1ex]{\overline{{\mathbb{C}}(A,i)}}\). However Theorem 2 shows that incompleteness can occur in even the simplest of programs. We show that every non-trivial abstraction is incomplete for some program as simple as a decider of a regular language—the simplest in Chomsky’s hierarchy.

To ensure a program is computationally as simple as a regular language decider, it sufficient to construct the program in those very terms. In particular, we will construct a program from the standard model for deciding regular languages, the deterministic finite automata (DFA). We use a standard formulation of DFAs. A DFA is a 5-tuple \(\langle S,Q,F,q_0,\delta\rangle\) where \(S\) is a finite alphabet of symbols, \(Q\) a finite set of states, \(F \subseteq Q\) a subset of states designated as ‘accepting’, \(q_0 \in Q\) the start state, and \(\delta: (Q \times S) \to Q\) the function that defines the state transition rules A DFA can be defined by its characteristic function \(M: S^* \to \{0,1\}\) where \(S^*\) is the set of finite-length strings comprised of symbols in \(S\) with typical elements \(\sigma\). The characteristic function and the 5-tuple can be connected operationally via the helper function \(\hat{\delta}: ( S^* \times Q) \to Q\) defined recursively as usual: \[\begin{cases} \hat{\delta}(\varepsilon, q) = q,\\ \hat{\delta}(x \cdot \sigma, q) = \hat{\delta}(\sigma, \delta(x, q)) \end{cases}\] so that \(M\) can be defined \[M(\sigma) \defeq \begin{cases} 1 & \hat{\delta}(\sigma, q_0) \in F,\\ 0 & \hat{\delta}(\sigma, q_0) \notin F. \end{cases}\] It is known that the set of regular languages is exactly the set of all languages \(L\subseteq S^*\) for which there exists a DFA \(M\) such that for any string \(\sigma\), we have \(\sigma \in L\) if and only if \(M(\sigma) = 1\).

Let \(S\) be an alphabet of symbols used for encoding and \(\tau: \mathbb{D}\to S^*\) a linear time string encoding for \(\mathbb{D}\), then a function \(f_M: \mathbb{D}^3 \to \mathbb{D}\) is a regular function if, for some DFA \(M\), it can be defined \[f_{M}(a,e,x) = \begin{cases} a & M(\tau(x)) = 1,\\ e & M(\tau(x)) = 0 \end{cases}\] A regular program is any program that implements a regular function.

In our context and from the construction of Theorem 2 we can define the following partial computable function as implemented in Fig. 3: \[\raisebox{0ex}[1ex][1ex]{\varphi^{\, }_{p}}(a,b,e,x)=\left\{ \begin{array}{cl} b & if x=a\\ \raisebox{0ex}[1ex][1ex]{\varphi^{\, }_{e}}(x) &otherwise \end{array}\right .\] By the s-m-n theorem there exists a total computable function \(g\) such that for fixed \(a,b\in\mathbb{D}\) and \(e\in\mathscr{L}\), \(\raisebox{0ex}[1ex][1ex]{\varphi^{\, }_{p}}(a,b,e,x) = \raisebox{0ex}[1ex][1ex]{\varphi^{\, }_{g(p,a,b,e)}}(x)\). By what proved in Theorem 2 it is immediate to see that when \(A\) is not straightforward and \(W_o\in\wp^{\text{ce}}(\mathbb{D})\) such that \(b\in\mathbb{D}\setminus\raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}(W_o)\) and \(a\in \raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}(W_i)\setminus W_i\), then for all \(e\in\mathscr{L}\) we have that \(g(p,a,b,e)\in \raisebox{0ex}[1ex][1ex]{\overline{{\mathbb{C}}(A,i)}}\).

It is immediate to note that there exists a DFA \(M_{L}\) that recognizes the regular language \(L=\{\tau(a)\}\) or more in general \(L=\tau(R)\) for any regular language \(R\subseteq \raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}(W_i)\setminus W_i\), such that \(\raisebox{0ex}[1ex][1ex]{\varphi^{\, }_{g(p,a,b,e)}}(x)= f_{M_{L}}(b,\raisebox{0ex}[1ex][1ex]{\varphi^{\, }_{e}}(x),x)\). The function \(g\) mapping \(e\) into \(g(p,a,b,e)\) can therefore be implemented as a regular program, returning a transformed program whose running time has a minimal linear overhead over the complexity of \(e\).

6 Conclusion↩︎

We studied local completeness of abstract interpretations in the standard computability context. In particular we analyzed the complexity of the classes of programs having a locally complete and incomplete abstract interpretation. We first reconciled abstract interpretation with standard computability theory by defining the notion of uniform closure operators as computable program transformations acting as semantic approximations of c.e. sets, and proved that any Galois connection-based abstract domain naturally induces a uniform closure. We then observed, via a simple application of Rice’s theorem, that no such closures can correspond to a uniformly decidable abstraction unless the abstraction is trivial. This provides a precise computability-theoretic account of the familiar distinction between the static and dynamic use of abstractions.

Upon these bases we proved that the classes of locally complete and incomplete abstract interpretations are in general recursively inseparable being both productive sets. Moreover, although a c.e. covering cannot in general be obtained for the incompleteness case, it can be effectively constructed for the completeness case. This result opens a promising direction for future work on the effective identification of representative code blocks for which a given abstraction is complete/precise. In particular, our covering function provides an elegant fix-point characterization of the classes of locally complete programs, paving the road to systematic code repair strategies to improve the precision of abstract interpretations by program transformation. In particular, because local completeness is essential to make abstract interpreters compositional, this result can be used to solve the problem of decomposing a program \(p\) into suitable subprograms \(p_1,\ldots,p_n\) such that the composition of their abstract interpretations minimizes incompleteness, as suggested in [13]. Such blocks could guide targeted refinements toward the portions of code responsible for imprecision, enabling more precise analyses without requiring a global refinement of the abstract domain. We believe that a similar construction can be used to obtain a covering for the class of partially complete abstract interpretations as introduced in [32]. In this case the program transformation can be used to compress the imprecision of the analysis below some given error bound.

Interestingly, the program transformation that provides a fix-point characterization of the covering for the class of locally complete programs in Theorem 5 has a clear correspondence with the Relax rule of LCL [10], a logic guaranteeing local completeness. The Relax rule is a key rule in LCL to ensure that pre/post conditions remain inside specific bounds in order to prove local completeness. This rule constrains the under-approximating post-condition to have the same abstraction as the strongest post-condition, which is needed for preserving local completeness, in a similar way as played by the condition \(x\in \raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}(W_{i})~\wedge~\raisebox{0ex}[1ex][1ex]{\varphi^{\, }_{e}}(x){\downarrow}~\wedge~\raisebox{0ex}[1ex][1ex]{\varphi^{\, }_{e}}(x)\in \raisebox{0ex}[1ex][1ex]{\rho^{}_{A}}(W_{h(e,i)})\) in (5 ). An interesting open question is then whether LCL is sound and complete for the c.e. covering \(\cC_i\) of \({\mathbb{C}}(A,i)\). Other open questions remain such as the role of \({\mathbb{C}}(A,i)\) and \(\raisebox{0ex}[1ex][1ex]{\overline{{\mathbb{C}}(A,i)}}\) respectively in \(\raisebox{0ex}[1ex][1ex]{\Pi^0_2}\) and \(\raisebox{0ex}[1ex][1ex]{\Sigma^0_2}\). In this case we believe that \({\mathbb{C}}(A,i)\) is not \(\raisebox{0ex}[1ex][1ex]{\Pi^0_2}\)-hard.

References↩︎