9512.net

甜梦文库

甜梦文库

当前位置：首页 >> >> # Data-flow analysis for constraint logic-based languages

Finite-Tree Analysis for Constraint Logic-Based Languages

Roberto Bagnara1 , Roberta Gori2 , Patricia M. Hill3 , and Enea Za?anella1

1

2

Department of Mathematics, University of Parma, Italy. {bagnara,zaffanella}@cs.unipr.it Department of Computer Science, University of Pisa, Italy. gori@di.unipi.it 3 School of Computing, University of Leeds, U. K. hill@comp.leeds.ac.uk

Abstract. Logic languages based on the theory of rational, possibly in?nite, trees have much appeal in that rational trees allow for faster uni?cation (due to the omission of the occurs-check) and increased expressivity. Note that cyclic terms can provide a very e?cient representation of grammars and other useful objects. Unfortunately, the use of in?nite rational trees has problems. For instance, many of the built-in and library predicates are ill-de?ned for such trees and need to be supplemented by run-time checks whose cost may be signi?cant. Moreover, some widelyused program analysis and manipulation techniques are only correct for those parts of programs working over ?nite trees. It is thus important to obtain, automatically, a knowledge of those program variables (the ?nite variables ) that, at the program points of interest, will always be bound to ?nite terms. For these reasons, we propose here a new data-?ow analysis that captures such information. We present a parametric domain where a simple component for recording ?nite variables is coupled with a generic domain (the parameter of the construction) providing sharing information. The sharing domain is abstractly speci?ed so as to guarantee the correctness of the combined domain and the generality of the approach.

1

Introduction

The intended computation domain of most logic-based languages1 includes the algebra (or structure) of ?nite trees. Other (constraint) logic-based languages, such as Prolog II and its successors [10, 12], SICStus Prolog [36], and Oz [34], refer to a computation domain of rational trees. A rational tree is a possibly in?nite tree with a ?nite number of distinct subtrees and, as is the case for ?nite trees,

This work has been partly supported by MURST project “Certi?cazione automatica di programmi mediante interpretazione astratta.” Some of this work was done during visits of the fourth author to Leeds, funded by EPSRC under grant M05645. That is, ordinary logic languages, (concurrent) constraint logic languages, functional logic languages and variations of the above.

1

where each node has a ?nite number of immediate descendants. These properties will ensure that rational trees, even though in?nite in the sense that they admit paths of in?nite length, can be ?nitely represented. One possible representation makes use of connected, rooted, directed and possibly cyclic graphs where nodes are labeled with variable and function symbols as is the case of ?nite trees. Applications of rational trees in logic programming include graphics [18], parser generation and grammar manipulation [10, 21], and computing with ?nitestate automata [10]. Other applications are described in [20] and [23]. Going from Prolog to CLP, [31] combines constraints on rational trees and record structures, while the logic-based language Oz allows constraints over rational and feature trees [34]. The expressive power of rational trees is put to use, for instance, in several areas of natural language processing. Rational trees are used in implementations of the HPSG formalism (Head-driven Phrase Structure Grammar) [32], in the ALE system (Attribute Logic Engine) [8], and in the ProFIT system (Prolog with Features, Inheritance and Templates) [19]. While rational trees allow for increased expressivity, they also come equipped with a surprising number of problems. As we will see, some of these problems are so serious that rational trees must be used in a very controlled way, disallowing them in any context where they are “dangerous”. This, in turn, causes a secondary problem: in order to disallow rational trees in selected contexts one must ?rst detect them, an operation that may be expensive. The ?rst thing to be aware of is that almost any semantics-based program manipulation technique developed in the ?eld of logic programming —whether it be an analysis, a transformation, or an optimization— assumes a computation domain of ?nite trees. Some of these techniques might work with the rational trees but their correctness has only been proved in the case of ?nite trees. Others are clearly inapplicable. Let us consider a very simple Prolog program: list([]). list([ |T]) :- list(T). Most automatic and semi-automatic tools for proving program termination and for complexity analysis agree on the fact that list/1 will terminate when invoked with a ground argument. Consider now the query ?- X = [a|X], list(X). and note that, after the execution of the ?rst rational uni?cation, the variable X will be bound to a rational term containing no variables, i.e., the predicate list/1 will be invoked with X ground. However, if such a query is given to, say, SICStus Prolog, then the only way to get the prompt back is by pressing ^C. The problem stems from the fact that the analysis techniques employed by these tools are only sound for ?nite trees: as soon as they are applied to a system where the creation of cyclic terms is possible, their results are inapplicable. The situation can be improved by combining these termination and/or complexity analyses by a ?niteness analysis providing the precondition for the applicability of the other techniques. 2

The implementation of built-in predicates is another problematic issue. Indeed, it is widely acknowledged that, for the implementation of a system that provides real support for the rational trees, the biggest e?ort concerns proper handling of built-ins. Of course, the meaning of ‘proper’ depends on the actual built-in. Built-ins such as copy_term/2 and ==/2 maintain a clear semantics when passing from ?nite to rational trees. For others, like sort/2, the extension can be questionable:2 both raising an exception and answering Y = [a] can be argued to be “the right reaction” to the query ?- X = [a|X], sort(X, Y). Other built-ins do not tolerate in?nite trees in some argument positions. A good implementation should check for ?niteness of the corresponding arguments and make sure “the right thing” —failing or raising an appropriate exception— always happens. However, such behavior appears to be uncommon. A small experiment we conducted on six Prolog implementations with queries like ?- X = 1+X, Y is X. ?- X = [97|X], name(Y, X). ?- X = [X|X], Y =.. [f|X]. resulted in in?nite loops, memory exhaustion and/or system thrashing, segmentation faults or other fatal errors. One of the implementations tested, SICStus Prolog, is a professional one and implements run-time checks to avoid most cases where built-ins can have catastrophic e?ects.3 The remaining systems are a bit more than research prototypes, but will clearly have to do the same if they evolve to the stage of production tools. Again, a data-?ow analysis aimed at the detection of those variables that are de?nitely bound to ?nite terms would allow to avoid a (possibly signi?cant) fraction of the useless run-time checks. Note that what has been said for built-in predicates applies to libraries as well. Even though it may be argued that it is enough for programmers to know that they should not use a particular library predicate with in?nite terms, it is clear that the use of a “safe” library, including automatic checks which ensure that such predicates are never called with an illegal argument, will result in more robust systems. With the appropriate data-?ow analyses, safe libraries do not have to be ine?cient libraries. Another serious problem is the following: the ISO Prolog standard term ordering cannot be extended to rational trees [M. Carlsson, Personal communication, October 2000]. Consider the rational trees de?ned by A = f(B, a) and B = f(A, b). Clearly, A == B does not hold. Since the standard term ordering is total, we must have either A @< B or B @< A. Assume A @< B. Then f(A, b) @< f(B, a), since the ordering of terms having the same principal functor is inherited by the ordering of subterms considered in a left-to-right fashion. Thus B @< A must hold, which is a contradiction. A dual contradiction

2

3

Even though sort/2 is not required to be a built-in by the standard, it is o?ered as such by several implementations. SICStus 3.8.5 still loops on ?- X = [97|X], name(Y, X).

3

is obtained by assuming B @< A. As a consequence, applying one of the Prolog term-ordering predicates to one or two in?nite terms may cause inconsistent results, giving rise to bugs that are exceptionally di?cult to diagnose. For this reason, any system that extends ISO Prolog with rational trees ought to detect such situations and make sure they are not ignored (e.g., by throwing an exception or aborting execution with a meaningful message). However, predicates such as the term-ordering ones are likely to be called a signi?cant number of times, since they are often used to maintain structures implementing ordered collections of terms. This is another instance of the e?ciency issue mentioned above. In this paper, we present a parametric abstract domain for ?nite-tree analysis, denoted by H × P . This domain combines a simple component H (the ?niteness component), recording the set of de?nitely ?nite variables, with a generic domain P (the parameter of the construction), providing sharing information. The term “sharing information” is to be understood in its broader meaning, which includes variable aliasing, groundness, linearity, freeness and any other kind of information that can improve the precision on these components, such as explicit structural information. Several domain combinations and abstract operators, characterized by di?erent precision/complexity trade-o?s, have been proposed to capture these properties (see [5] for an account of some of them). By giving a generic speci?cation for this parameter component, in the style of the open product construct proposed in [14], it is possible to de?ne and establish the correctness of the abstract operators on the ?nite-tree domain independently from any particular domain for sharing analysis. The paper is structured as follows. The required notations and preliminary concepts are given in Section 2. The ?nite-tree domain is then introduced in Section 3: Section 3.1 provides the speci?cation of the parameter domain P ; Section 3.2 de?nes the abstraction function for the ?niteness component H ; Section 3.3 de?nes the abstract uni?cation operator for H × P . A description of some ongoing work on the subject is given in Section 4 where a possible instance of the parameter P is also speci?ed. We conclude in Section 5. A longer version of this paper with proofs of the results presented here is available as a technical report [1].

2

2.1

Preliminaries

In?nite Terms and Substitutions

For a set S , ?(S ) is the powerset of S , whereas ?f (S ) is the set of all the ?nite subsets of S . Let Sig denote a possibly in?nite set of function symbols, ranked over the set of natural numbers. It is assumed that Sig contains at least one function symbol having rank 0 and one having rank greater than 0. Let Vars denote a denumerable set of variables, disjoint from Sig . Then Terms denotes the free algebra of all (possibly in?nite) terms in the signature Sig having variables in Vars . Thus a term can be seen as an ordered labeled tree, possibly having 4

some in?nite paths and possibly containing variables: every inner node is labeled with a function symbol in Sig with a rank matching the number of the node’s immediate descendants, whereas every leaf is labeled by either a variable in Vars or a function symbol in Sig having rank 0 (a constant). If t ∈ Terms then vars(t) and mvars(t) denote the set and the multiset of variables occurring in t, respectively. We will also write vars(o) to denote the set of variables occurring in an arbitrary syntactic object o. If a occurs more than once in a multiset M we write a M . Suppose s, t ∈ Terms : s and t are independent if vars(s) ∩ vars(t) = ?; if y ∈ vars(t) and ? y mvars(t) we say that variable y occurs linearly in t, more brie?y written using the predication occ lin(y, t); t is said to be ground if vars(t) = ?; t is free if t ∈ Vars ; t is linear if, for all y ∈ vars(t), we have occ lin(y, t); ?nally, t is a ?nite term (or Herbrand term ) if it contains a ?nite number of occurrences of function symbols. The sets of all ground, linear and ?nite terms are denoted by GTerms , LTerms and HTerms , respectively. As we have speci?ed that Sig contains function symbols of rank 0 and rank greater than 0, GTerms ∩ HTerms = ? and GTerms \ HTerms = ?. A substitution is a total function σ : Vars → HTerms that is the identity almost everywhere; in other words, the domain of σ , dom(σ ) =

def

x ∈ Vars σ (x) = x ,

is ?nite. Given a substitution σ : Vars → HTerms , we overload the symbol ‘σ ’ so as to denote also the function σ : HTerms → HTerms de?ned as follows, for each term t ∈ HTerms : ? ? if t is a constant symbol; ?t, def σ (t) = σ (t), if t ∈ Vars ; ? ? f σ (t1 ), . . . , σ (tn ) , if t = f (t1 , . . . , tn ). If x ∈ Vars and t ∈ HTerms \ {x}, then x → t is called a binding. The set of all bindings is denoted by Bind . Substitutions are denoted by the set of their bindings, thus a substitution σ is identi?ed with the (?nite) set x → σ (x) x ∈ dom(σ ) . We denote by vars(σ ) the set of variables occurring in the bindings of σ . A substitution is said to be circular if, for n > 1, it has the form {x1 → x2 , . . . , xn?1 → xn , xn → x1 }, where x1 , . . . , xn are distinct variables. A substitution is in rational solved form if it has no circular subset. The set of all substitutions in rational solved form is denoted by RSubst . If t ∈ HTerms , we write tσ to denote σ (t) and t[x/s] to denote t{x → s}. The composition of substitutions is de?ned in the usual way. Thus τ ? σ is the substitution such that, for all terms t ∈ HTerms , (τ ? σ )(t) = τ σ (t) 5

and has the formulation τ ?σ = x → xστ x ∈ dom(σ ), x = xστ ∪ x → xτ x ∈ dom(τ ) \ dom(σ ) .

As usual, σ 0 denotes the identity function (i.e., the empty substitution) and, when i > 0, σ i denotes the substitution (σ ? σ i?1 ). For each σ ∈ RSubst , s ∈ HTerms , the sequence of ?nite terms σ 0 (s), σ 1 (s), σ 2 (s), . . . converges to a (possibly in?nite) term, denoted σ ∞ (s) [25, 29]. Therefore, the function rt : HTerms × RSubst → Terms such that rt(s, σ ) = σ ∞ (s) is well de?ned. Note that, in general, this function is not a substitution: while having a ?nite domain, its “bindings” x → t can map a domain variable x into a term t ∈ Terms \ HTerms .

def

2.2

Equations

An equation is of the form s = t where s, t ∈ HTerms . Eqs denotes the set of all equations. A substitution σ may be regarded as a ?nite set of equations, that is, as the set { x = t | x → t ∈ σ }. We say that a set of equations e is in rational solved form if s → t (s = t) ∈ e ∈ RSubst . In the rest of the paper, we will often write a substitution σ ∈ RSubst to denote a set of equations in rational solved form (and vice versa). Languages such as Prolog II, SICStus and Oz are based on RT , the theory of rational trees [10, 11]. This is a syntactic equality theory (i.e., a theory where the function symbols are uninterpreted), augmented with a uniqueness axiom for each substitution in rational solved form. Informally speaking these axioms state that, after assigning a ground rational tree to each non-domain variable, the substitution uniquely de?nes a ground rational tree for each of its domain variables. Thus, any set of equations in rational solved form is, by de?nition, satis?able in RT . Note that being in rational solved form is a very weak property. Indeed, uni?cation algorithms returning a set of equations in rational solved form are allowed to be much more “lazy” than one would usually expect. We refer the interested reader to [27, 28, 30] for details on the subject. Given a set of equations e ∈ ?f (Eqs ) that is satis?able in RT , a substitution σ ∈ RSubst is called a solution for e in RT if RT ?(σ → e), i.e., if every model of the theory RT is also a model of the ?rst order formula ?(σ → e). If in addition vars(σ ) ? vars(e), then σ is said to be a relevant solution for e. Finally, σ is a most general solution for e in RT if RT ?(σ ? e). In this paper, the set of all the relevant most general solution for e in RT will be denoted by mgs(e). 6

2.3

The Concrete Domain

Throughout the paper, we assume a knowledge of the basic concepts of abstract interpretation theory [15, 16]. For the purpose of this paper, we assume a concrete domain constituted by pairs of the form (Σ, V ), where V is a ?nite set of variables of interest and Σ is a (possibly in?nite) set of substitutions in rational solved form. De?nition 1. (The concrete domain.) Let D = ?(RSubst ) × ?f (Vars ). If (Σ, V ) ∈ D , then (Σ, V ) represents the (possibly in?nite) set of ?rst-order formulas ?? . σ σ ∈ Σ, ? = vars(σ ) \ V where σ is interpreted as the logical conjunction of the equations corresponding to its bindings. Concrete domains for constraint languages would be similar. If the analyzed language allows the use of constraints on various domains to restrict the values of the variable leaves of rational trees, the corresponding concrete domain would have one or more extra components to account for the constraints (see [2] for an example). The concrete element {x → f (y )} , {x, y } expresses a dependency between x and y . In contrast, {x → f (y )} , {x} only constrains x. The same concept can be expressed by saying that in the ?rst case the variable name ‘y ’ matters, but it does not in the second case. Thus, the set of variables of interest is crucial for de?ning the meaning of the concrete and abstract descriptions. Despite this, always specifying the set of variables of interest would signi?cantly clutter the presentation. Moreover, most of the needed functions on concrete and abstract descriptions preserve the set of variables of interest. For these reasons, we assume the existence of a set VI ∈ ?f (Vars ) that contains, at each stage of the analysis, the current variables of interest.4 As a consequence, when the context makes it clear that Σ ∈ ?(RSubst ), we will write Σ ∈ D as a shorthand for (Σ, VI ) ∈ D .

def

3

An Abstract Domain for Finiteness Analysis

Finite-tree analysis applies to logic-based languages computing over a domain of rational trees where cyclic structures are allowed. In contrast, analyses aimed at occurs-check reduction [17, 35] apply to programs that are meant to compute on a domain of ?nite trees only, but have to be executed over systems that are either designed for rational trees or intended just for the ?nite trees but omit the occurs-check for e?ciency reasons. Despite their di?erent objectives, ?nite-tree and occurs-check analyses have much in common: in both cases, it is important to detect all program points where cyclic structures can be generated.

4

This parallels what happens in the e?cient implementation of data-?ow analyzers. In fact, almost all the abstract domains currently in use do not need to represent explicitly the set of variables of interest. In contrast, this set is maintained externally and in a unique copy, typically by the ?xpoint computation engine.

7

Note however that, when performing occurs-check reduction, one can take advantage of the following invariant: all data structures generated so far are ?nite. This property is maintained by transforming the program so as to force ?niteness whenever it is possible that a cyclic structure could have been built.5 In contrast, a ?nite-tree analysis has to deal with the more general case when some of the data structures computed so far may be cyclic. It is therefore natural to consider an abstract domain made up of two components. The ?rst one simply represents the set of variables that are guaranteed not to be bound to in?nite terms. We will denote this ?niteness component by H (from Herbrand ). De?nition 2. (The ?niteness component.) The ?niteness component is the set H = ?(VI ) partially ordered by reverse subset inclusion. The second component of the ?nite-tree domain should maintain any kind of information that may be useful for computing ?niteness information. It is well-known that sharing information as a whole, therefore including possible variable aliasing, de?nite linearity, and de?nite freeness, has a crucial role in occurs-check reduction so that, as observed before, it can be exploited for ?nite-tree analysis too. Thus, a ?rst choice for the second component of the ?nite-tree domain would be to consider one of the standard combinations of sharing, freeness and linearity as de?ned, e.g., in [5, 6, 22]. However, this would tie our speci?cation to a particular sharing analysis domain, whereas the overall approach seems to be inherently more general. For this reason, we will de?ne a ?nite-tree analysis based on the abstract domain schema H ×P , where the generic sharing component P is a parameter of the abstract domain construction. This approach can be formalized as an application of the open product operator [14]. 3.1 The parameter component P

def

Elements of P can encode any kind of information. We only require that substitutions that are equivalent in the theory RT are identi?ed in P . De?nition 3. (The parameter component.) The parameter component P is an abstract domain related to the concrete domain D by means of the concretization function γP : P → ?(RSubst ) such that, for all p ∈ P , σ ∈ γP (p ) ∧ RT ?(σ ? τ ) =? τ ∈ γP (p ).

The interface between H and P is provided by a set of predicates and functions that satisfy suitable correctness criteria. Note that, for space limitations, we will only specify those abstract operations that are useful to de?ne abstract uni?cation on the combined domain H × P . The other operations needed for a full description of the analysis, such as renamings, upper bound operators and projections, are very simple and, as usual, do not pose any problems.

5

Such a requirement is typically obtained by replacing the uni?cation with a call to unify with occurs check/2. As an alternative, in some systems based on rational trees it is possible to insert, after each problematic uni?cation, a ?niteness test for the generated term.

8

De?nition 4. (Abstract operators on P .) Let s, t ∈ HTerms be ?nite terms. For each p ∈ P , we de?ne the following predicates: s and t are independent in p if and only if indp : HTerms 2 → Bool holds for (s, t), where indp (s, t) =? ?σ ∈ γP (p ) : vars rt(s, σ ) ∩ vars rt(t, σ ) = ?; s and t share linearly in p if and only if share linp : HTerms 2 → Bool holds for (s, t), where share linp (s, t) =? ?σ ∈ γP (p ) : ?y ∈ vars rt(s, σ ) ∩ vars rt(t, σ ) : occ lin y, rt(s, σ ) ∧ occ lin y, rt(t, σ ) ; t is ground in p if and only if groundp : HTerms → Bool holds for t, where groundp (t) =? ?σ ∈ γP (p ) : rt(t, σ ) ∈ GTerms ; t is ground-or-free in p if and only if gfreep : HTerms → Bool holds for t, where gfreep (t) =? ?σ ∈ γP (p ) : rt(t, σ ) ∈ GTerms ∨ rt(t, σ ) ∈ Vars ; s and t are or-linear in p if and only if or linp : HTerms 2 → Bool holds for (s, t), where or linp (s, t) =? ?σ ∈ γP (p ) : rt(s, σ ) ∈ LTerms ∨ rt(t, σ ) ∈ LTerms ; s is linear in p if and only if linp : HTerms → Bool holds for s, where linp (s) ?? or linp (s, s). For each p ∈ P , the following functions compute subsets of the set of variables of interest: the function share same varp : HTerms × HTerms → ?(VI ) returns a set of variables that may share with the given terms via the same variable. For each s, t ∈ HTerms, ? ? ? ? ?σ ∈ γP (p ) . ? ? share same varp (s, t) ? y ∈ VI ; ?z ∈ vars rt(y, σ ) . ? ? ? ? z ∈ vars rt(s, σ ) ∩ vars rt(t, σ ) the function share withp : HTerms → ?(VI ) yields a set of variables that may share with the given term. For each t ∈ HTerms, share withp (t) =

def def

y ∈ VI

y ∈ share same varp (y, t) . 9

The function amguP : P ×Bind → P correctly captures the e?ects of a binding on an element of P . For each (x → t) ∈ Bind and p ∈ P , let p = amguP p , x → t . For all σ ∈ γP (p ), if τ ∈ mgs σ ∪ {x = t} , then τ ∈ γP (p ). As it will be shown in Section 4.1, some of these generic operators can be directly mapped into the corresponding abstract operators de?ned for well-known sharing analysis domains. However, the speci?cation given in De?nition 4, besides being more general than a particular implementation, also allows for a modular approach when proving correctness results.

def

3.2

The abstraction function for H

When the concrete domain is based on the theory of ?nite trees, idempotent substitutions provide a ?nitely computable strong normal form for domain elements, meaning that di?erent substitutions describe di?erent sets of ?nite trees.6 In contrast, when working on a concrete domain based on the theory of rational trees, substitutions in rational solved form, while being ?nitely computable, no longer satisfy this property: there can be an in?nite set of substitutions in rational solved form all describing the same set of rational trees (i.e., the same element in the “intended” semantics). For instance, the substitutions

n

σn = {x → f (· · · f ( x) · · · )} for n = 1, 2, . . . , all map the variable x into the same rational tree (which is usually denoted by f ω ). Ideally, a strong normal form for the set of rational trees described by a substitution σ ∈ RSubst can be obtained by computing the limit σ ∞ . The problem is that we may end up with σ ∞ ∈ / RSubst , as σ ∞ can map domain variables to in?nite rational terms. This poses a non-trivial problem when trying to de?ne a “good” abstraction function, since it would be really desirable for this function to map any two equivalent concrete elements to the same abstract element. As shown in [24], the classical abstraction function for set-sharing analysis [13, 26], which was de?ned for idempotent substitutions only, does not enjoy this property when applied, as it is, to arbitrary substitutions in rational solved form. A possibility is to look for a more general abstraction function that allows to obtain the desired property. For example, in [24] the sharing-group operator sg of [26] is replaced by an occurrence operator, occ, de?ned by means of a ?xpoint computation. We now provide a similar ?xpoint construction de?ning the ?niteness operator.

6

As usual, this is modulo the possible renaming of variables.

10

De?nition 5. (Finiteness functions.) For each n ∈ N, the ?niteness function hvarsn : RSubst → ?(Vars ) is de?ned, for each σ ∈ RSubst, by hvars0 (σ ) = Vars \ dom(σ ) and, for n > 0, by hvarsn (σ ) = hvarsn?1 (σ ) ∪ y ∈ dom(σ ) vars(yσ ) ? hvarsn?1 (σ ) . For each σ ∈ RSubst and each i ≥ 0, we have hvarsi (σ ) ? hvarsi+1 (σ ) and also that Vars \ hvarsi (σ ) ? dom(σ ) is a ?nite set. By these two properties, the following ?xpoint computation is well de?ned and ?nitely computable. De?nition 6. (Finiteness operator.) For each σ ∈ RSubst, the ?niteness operator hvars : RSubst → ?(Vars ) is given by hvars(σ ) = hvars (σ ) where

def def def def

= (σ ) ∈ N is such that hvars (σ ) = hvarsn (σ ) for all n ≥ .

The following proposition shows that the hvars operator precisely captures the intended property. Proposition 1. If σ ∈ RSubst and x ∈ Vars then x ∈ hvars(σ ) ?? rt(x, σ ) ∈ HTerms . Example 1. Consider σ ∈ RSubst , where σ = x1 → f (x2 ), x2 → g (x5 ), x3 → f (x4 ), x4 → g (x3 ) . Then, hvars0 (σ ) = Vars \ {x1 , x2 , x3 , x4 }, hvars1 (σ ) = Vars \ {x1 , x3 , x4 }, hvars2 (σ ) = Vars \ {x3 , x4 } = hvars(σ ). Thus, x1 ∈ hvars(σ ), although vars(x1 σ ) ? dom(σ ). The abstraction function for H can then be de?ned in the obvious way. De?nition 7. (The abstraction function for H .) The abstraction function αH : RSubst → H is de?ned, for each σ ∈ RSubst, by αH (σ ) = VI ∩ hvars(σ ). The concrete domain D is related to H by means of the abstraction function αH : D → H such that, for each Σ ∈ ?(RSubst ), αH (Σ ) =

def def

αH (σ ) σ ∈ Σ .

11

Since the abstraction function αH is additive, the concretization function is given by its adjoint [15]: γH (h ) =

def

σ ∈ RSubst αH (σ ) ? h .

With these de?nitions, we have the desired result: equivalent substitutions in rational solved form have the same ?niteness abstraction. Theorem 1. If σ, τ ∈ RSubst and RT 3.3 Abstract uni?cation on H × P ?(σ ? τ ), then αH (σ ) = αH (τ ).

The abstract uni?cation for the combined domain H × P is de?ned by using the abstract predicates and functions as speci?ed for P as well as a new ?niteness predicate for the domain H . De?nition 8. (Abstract uni?cation on H × P .) A term t ∈ HTerms is a ?nite tree in h if and only if the predicate htermh : HTerms → Bool holds for t, def where htermh (t) = vars(t) ? h. The function amguH : (H × P ) × Bind → H captures the e?ects of a binding on an H element. Let h , p ∈ H × P and (x → t) ∈ Bind . Then amguH h , p , x → t = h , where ? h ∪ vars(t), ? ? ? ? ? h ∪ {x}, ? ? ? ? ? h, ? ? ? ? ? ? ? ? ? h, ? ? ? ? if htermh (x) ∧ groundp (x); if htermh (t) ∧ groundp (t); if htermh (x) ∧ htermh (t) ∧ indp (x, t) ∧ or linp (x, t); if htermh (x) ∧ htermh (t) ∧ gfreep (x) ∧ gfreep (t); if htermh (x) ∧ htermh (t) ∧ share linp (x, t) ∧ or linp (x, t); if htermh (x) ∧ linp (x); if htermh (t) ∧ linp (t); otherwise.

def

h =

def

? h \ share same varp (x, t), ? ? ? ? ? ? ? ? ? ? ? ? ? ? h \ share withp (x), ? ? ? ? ? h \ share withp (t), ? ? ? h \ share withp (x) ∪ share withp (t) ,

The abstract uni?cation function amgu : (H × P ) × Bind → H × P , for any h , p ∈ H × P and (x → t) ∈ Bind , is given by amgu h , p , x → t =

def

amguH h , p , x → t , amguP (p , x → t) .

12

In the computation of h (the new ?niteness component resulting from the abstract evaluation of a binding) there are eight cases based on properties holding for the concrete terms described by x and t. 1. In the ?rst case, the concrete term described by x is both ?nite and ground. Thus, after a successful execution of the binding, any concrete term described by t will be ?nite. Note that t could have contained variables which may be possibly bound to cyclic terms just before the execution of the binding. 2. The second case is symmetric to the ?rst one. Note that these are the only cases when a “positive” propagation of ?niteness information is correct. In contrast, in all the remaining cases, the goal is to limit as much as possible the propagation of “negative” information, i.e., the possible cyclicity of terms. 3. The third case exploits the classical results proved in research work on occurscheck reduction [17, 35]. Accordingly, it is required that both x and t describe ?nite terms that do not share. The use of the implicitly disjunctive predicate or linp allows for the application of this case even when neither x nor t are known to be de?nitely linear. For instance, as observed in [17], this may happen when the component P embeds the domain Pos for groundness analysis.7 4. The fourth case exploits the observation that cyclic terms cannot be created when unifying two ?nite terms that are either ground or free. Groundor-freeness [5] is a safe, more precise and inexpensive replacement for the classical freeness property when combining sharing analysis domains. 5. The ?fth case applies when unifying a linear and ?nite term with another ?nite term possibly sharing with it, provided they can only share linearly (namely, all the shared variables occur linearly in the considered terms). In such a context, only the shared variables can introduce cycles. 6. In the sixth case, we drop the assumption about the ?niteness of the term described by t. As a consequence, all variables sharing with x become possibly cyclic. However, provided x describes a ?nite and linear term, all ?nite variables independent from x preserve their ?niteness. 7. The seventh case is symmetric to the sixth one. 8. The last case states that term ?niteness is preserved for all variables that are independent from both x and t. Note that this case is only used when none of the other cases apply. The following result, together with the assumption on amguP as speci?ed in De?nition 4, ensures that abstract uni?cation on the combined domain H × P is correct. Theorem 2. Let h , p ∈ H × P and (x → t) ∈ Bind , where {x}∪ vars(t) ? VI . Let also σ ∈ γH (h ) ∩ γP (p ) and h = amguH h , p , x → t . Then τ ∈ mgs σ ∪ {x = t}

7

=? τ ∈ γH (h ).

def

Let t be y . Let also P be Pos . Then, given the Pos formula φ = (x ∨ y ), both indφ (x, y ) and or linφ (x, y ) satsify the conditions in De?nition 4. Note that from φ we cannot infer that x is de?nitely linear and neither that y is de?nitely linear.

13

4

4.1

Ongoing and Further Work

An instance of the parameter domain P

As discussed in Section 3, several abstract domains for sharing analysis can be used to implement the parameter component P . One could consider the wellknown set-sharing domain of Jacobs and Langen [26]. In such a case, all the non-trivial correctness results have already been established in [24]: in particular, the abstraction function provided in [24] satis?es the requirement of De?nition 3 and the abstract uni?cation operator has been proven correct with respect to rational-tree uni?cation. Note however that, since no freeness and linearity information is recorded in the plain set-sharing domain, some of the predicates of De?nition 4 need to be grossly approximated. Therefore, a better choice would be to consider the abstract domain SFL [5] (see also [6]) that represents possible sharing. This domain incorporates the set-sharing domain of Jacobs and Langen with de?nite freeness and linearity information; the information being encoded by two sets of variables, one satisfying the property of freeness and the other, the property of linearity. De?nition 9. (The set-sharing domain SH .) The set SH is de?ned by SH = ?(SG ), where SG = ?(VI ) \ {?} is the set of sharing groups. SH is ordered by subset inclusion. De?nition 10. (The domain SFL.) Let F = ?(VI ) and L = ?(VI ) be partially ordered by reverse subset inclusion. The domain SFL is de?ned by the def Cartesian product SFL = SH × F × L ordered by ‘≤S ’, the component-wise extension of the orderings de?ned on the sub-domains. Note that a complete de?nition, besides explicitly dealing with the set of relevant variables VI , would require the addition of a bottom element ⊥ representing the semantics of those program fragments that have no successful computations. In the next de?nition we introduce a few well-known operations on the setsharing domain SH . These will be used to de?ne the operations on the domain SFL. De?nition 11. (Abstract operators on SH .) For each sh ∈ SH and each V ? VI , the extraction of the relevant component of sh with respect to V is given by the function rel : ?(VI ) × SH → SH de?ned as rel(V, sh ) = { S ∈ sh | S ∩ V = ? }. For each sh ∈ SH and each V ? VI , the function rel : ?(VI ) × SH → SH gives the irrelevant component of sh with respect to V . It is de?ned as rel(V, sh ) = sh \ rel(V, sh ). 14

def def def def def def

The function (·) : SH → SH , called star-union, is given, for each sh ∈ SH , by

n

sh =

def

S ∈ SG ?n ≥ 1 . ?T1 , . . . , Tn ∈ sh . S =

i=1

Ti .

For each sh 1 , sh 2 ∈ SH , the function bin : SH × SH → SH , called binary union, is given by bin(sh 1 , sh 2 ) = { S1 ∪ S2 | S1 ∈ sh 1 , S2 ∈ sh 2 }. It is now possible to de?ne the implementation, on the domain SFL, of all the predicates and functions speci?ed in De?nition 4. De?nition 12. (Abstract operators on SFL.) For each d = sh , f, l ∈ SFL, for each s, t ∈ HTerms, where vars(s) ∪ vars(t) ? VI , let Rs = rel vars(s), sh and Rt = rel vars(t), sh . Then indd (s, t) = Rs ∩ Rt = ? ; groundd (t) = vars(t) ? VI \ vars(sh ) ; occ lind (y, t) = groundd (y ) ∨ occ lin(y, t) ∧ (y ∈ l) ∧ ?z ∈ vars(t) : y = z =? indd (y, z ) share lind (s, t) = ?y ∈ vars(Rs ∩ Rt ) : y ∈ vars(s) =? occ lind (y, s) ∧ y ∈ vars(t) =? occ lind (y, t); freed (t) = ?y ∈ VI . (y = t) ∧ (y ∈ f ); gfreed (t) = groundd (t) ∨ freed (t); lind (t) = ?y ∈ vars(t) : occ lind (y, t); or lind (s, t) = lind (s) ∨ lind (t); share same vard (s, t) = vars(Rs ∩ Rt ); share withd (t) = vars(Rt ). The function amguS : SFL × Bind → SFL captures the e?ects of a binding on an element of SFL. Let d = sh , f, l ∈ SFL and (x → t) ∈ Bind , where Vxt = {x} ∪ vars(t) ? VI . Let Rx = rel {x}, sh and Rt = rel vars(t), sh . Let also sh = rel(Vxt , sh ) ∪ bin Sx , St , Sx =

def def def def def def def def def def def def def

;

Rx , Rx ,

if freed (x) ∨ freed (t) ∨ lind (t) ∧ indd (x, t) ; otherwise; 15

St =

Rt , if freed (x) ∨ freed (t) ∨ lind (x) ∧ indd (x, t) ; Rt , otherwise; ? f, if freed (x) ∧ freed (t); ? ? ? ?f \ vars(R ), if freed (x); def x f = ? f \ vars(Rt ), if freed (t); ? ? ? f \ vars(Rx ∪ Rt ), otherwise;

def

l = VI \ vars(sh ) ∪ f ∪ l ; ? l \ vars(Rx ) ∩ vars(Rt ) , ? ? ? ?l \ vars(R ), def x l = ? l \ vars( R ), t ? ? ? l \ vars(Rx ∪ Rt ), Then amguS d , x → t = sh , f , l .

def

def

if lind (x) ∧ lind (t); if lind (x); if lind (t); otherwise.

It is worth noting that, when observing the term ?niteness property, set-sharing is strictly more precise than pair-sharing, since a set-sharing domain is strictly more precise when computing the functions share same varp and share linp .8 This observation holds regardless of the pair-sharing variant considered, including ASub [9, 35], PSD [3] and ShPSh [33]. It remains for us to establish that the relations and functions given in Definition 12 satisfy all the requirements of De?nitions 3 and 4. This will require a proof of the correctness, with respect to rational uni?cation, of the abstract operators de?ned on the domain SFL, thereby generalizing and extending the results proved in [24] for the set-sharing domain of Jacobs and Langen. Note that the domain SFL is not the target of the generic speci?cation given in De?nition 4; more powerful sharing domains can also satisfy this schema, including all the enhanced combinations considered in [5]. For instance, as the predicate gfreed de?ned on SFL does not fully exploit the disjunctive nature of its generic speci?cation gfreep , the precision of the analysis may be improved by adding a domain component explicitly tracking ground-or-freeness, as proposed in [5]. The same argument applies to the predicate or lind , with respect to or linp , when considering the combination with the groundness domain Pos . In order to provide an experimental evaluation of the proposed ?niteness analysis, we are implementing H × P where the P component is the SFL domain extended with some of the enhancements described in [5]. One of these

8

For the expert: consider the abstract evaluation of the binding x → y and the description h , d ∈ H × SFL, where h = {x, y, z } and d = sh , f, l is such that sh = {x, y }, {x, z }, {y, z } , f = ? and l = {x, y, z }. Then z ∈ / share same vard (x, y ) so that we have h = {z }. In contrast, when using a pair-sharing domain such as PSD , the element d is equivalent to d = sh , f, l , where sh = sh ∪ {x, y, z } . Hence we have z ∈ share same vard (x, y ) and h = ?. Thus, in sh the information provided by the lack of the sharing group {x, y, z } is redundant when observing pairsharing and groundness, but it is not redundant when observing term ?niteness.

16

enhancements uses information about the actual structure of terms. It has been shown in [2] that this structural information, provided by integrating the generic Pattern(·) construction with SFL, can have a key role in improving the precision of sharing analysis and, in particular, allowing better identi?cation where cyclic structures may appear. Thus, it is expected that structural information captured using Pattern(H × P ) can improve the precision of ?nite-tree analysis; both with respect to the parametric component P and the ?niteness component H itself. 4.2 Term-Finiteness Dependencies

The parametric domain H × P captures the negative aspect of term-?niteness, that is, the circumstances under which ?niteness can be lost. When a binding has the potential for creating one or more rational terms, the operator amguH removes from h all the variables that may be bound to non-?nite terms. However, term-?niteness has also a positive aspect: there are cases where a variable is guaranteed to be bound to a ?nite term and this knowledge can be propagated to other variables. Guarantees of ?niteness are provided by several built-ins like unify_with_occurs_check/2, var/1, name/2, all the arithmetic predicates, and so forth. SICStus Prolog also provides an explicit acyclic_term/1 predicate. The term-?niteness information provided by the h component of H × P does not capture the information concerning how ?niteness of one variable a?ects the ?niteness of other variables. This kind of information, usually termed relational information, is very important as it allows the propagation of positive ?niteness information. An important source of relational information comes from dependef def def dencies. Consider the terms t1 = f (x), t2 = g (y ), and t3 = h(x, y ): it is clear that, for each assignment of rational terms to x and y , t3 is ?nite if and only if t1 and t2 are so. We can capture this by the Boolean formula t3 ? (t1 ∧ t2 ). The reasoning is based on the following facts: 1. t1 , t2 , and t3 are ?nite terms, so that the ?niteness of their instances depends only on the ?niteness of the terms that take the place of x and y . 2. t3 covers both t1 and t2 , that is, vars(t3 ) ? vars(t1 ) ∪ vars(t2 ); this means that, if an assignment to the variables of t3 produces a ?nite instance of t3 , that very same assignment will necessarily result in ?nite instances of t1 and t2 . Conversely, an assignment producing non-?nite instances of t1 or t2 will forcibly result in a non-?nite instance of t3 . 3. Similarly, t1 and t2 , taken together, cover t3 . The important point to notice is that the indicated dependency will continue to hold for any further simultaneous instantiation of t1 , t2 , and t3 . In other words, such dependencies are preserved by forward computations (since they proceed by consistently instantiating program variables). Consider the abstract binding x → t where t is a ?nite term such that vars(t) = {y1 , . . . , yn }. After this binding has been successfully performed, the destinies of x and t concerning term-?niteness are tied together forever. This tie can be described by the dependency formula x ? (y1 ∧ · · · ∧ yn ), 17 (1)

meaning that x will be bound to a ?nite term if and only if, for each i = 1, . . . , n, yi is bound to a ?nite term. While the dependency expressed by (1) is a correct description of any computation state following the application of the binding x → t, it is not as precise as it could be. Suppose that x and yk are indeed the same variable. Then (1) is logically equivalent to x → (y1 ∧ · · · ∧ yk?1 ∧ yk+1 ∧ · · · ∧ yn ). (2)

Correct: whenever x is bound to a ?nite term, all the other variables will be bound to ?nite terms. The point is that x has just been bound to a non-?nite term, irrevocably: no forward computation can change this. Thus, the implication (2) holds vacuously. The precise and correct description for the state of a?airs caused by the cyclic binding is, instead, the negated atom ?x, whose intuitive reading is “x is not (and never will be) ?nite.” Following the intuition outlined above, in [4] we have studied a domain, whose carrier is the set of all Boolean functions, for representing and propagating ?niteness dependencies. We believe that coupling this new domain with H × P can greatly improve the precision of the analysis.

5

Conclusion

Several modern logic-based languages o?er a computation domain based on rational trees. On the one hand, the use of such trees is encouraged by the possibility of using e?cient and correct uni?cation algorithms and by an increase in expressivity. On the other hand, these gains are countered by the extra problems rational trees bring with themselves and that can be summarized as follows: several built-ins, library predicates, program analysis and manipulation techniques are only well-de?ned for program fragments working with ?nite trees. In this paper we propose an abstract-interpretation based solution to the problem of detecting program variables that can only be bound to ?nite terms. The rationale behind this is that applications exploiting rational trees tend to do so in a very controlled way. If the analysis we propose proves to be precise enough, then we will have a practical way of taking advantage of rational trees while minimizing the impact of their disadvantages.

References

1. R. Bagnara, R. Gori, P. M. Hill, and E. Za?anella. Finite-tree analysis for constraint logic-based languages. Quaderno 251, Dipartimento di Matematica, Universit` a di Parma, 2001. Available at http://www.cs.unipr.it/~bagnara/. 2. R. Bagnara, P. M. Hill, and E. Za?anella. E?cient structural information analysis for real CLP languages. In M. Parigot and A. Voronkov, editors, Proceedings of the 7th International Conference on Logic for Programming and Automated Reasoning (LPAR 2000), volume 1955 of Lecture Notes in Computer Science, pages 189–206, Reunion Island, France, 2000. Springer-Verlag, Berlin.

18

3. R. Bagnara, P. M. Hill, and E. Za?anella. Set-sharing is redundant for pair-sharing. Theoretical Computer Science, 2001. To appear. 4. R. Bagnara, E. Za?anella, R. Gori, and P. M. Hill. Boolean functions for ?nite-tree dependencies. Quaderno 252, Dipartimento di Matematica, Universit` a di Parma, 2001. Available at http://www.cs.unipr.it/~bagnara/. 5. R. Bagnara, E. Za?anella, and P. M. Hill. Enhanced sharing analysis techniques: A comprehensive evaluation. In M. Gabbrielli and F. Pfenning, editors, Proceedings of the 2nd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, pages 103–114, Montreal, Canada, 2000. Association for Computing Machinery. 6. M. Bruynooghe, M. Codish, and A. Mulkers. A composite domain for freeness, sharing, and compoundness analysis of logic programs. Technical Report CW 196, Department of Computer Science, K.U. Leuven, Belgium, July 1994. 7. J. A. Campbell, editor. Implementations of Prolog. Ellis Horwood/Halsted Press/Wiley, 1984. 8. B. Carpenter. The Logic of Typed Feature Structures with Applications to Uni?cation-based Grammars, Logic Programming and Constraint Resolution, volume 32 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, New York, 1992. 9. M. Codish, D. Dams, and E. Yardeni. Derivation and safety of an abstract uni?cation algorithm for groundness and aliasing analysis. In K. Furukawa, editor, Logic Programming: Proceedings of the Eighth International Conference on Logic Programming, MIT Press Series in Logic Programming, pages 79–93, Paris, France, 1991. The MIT Press. 10. A. Colmerauer. Prolog and in?nite trees. In K. L. Clark and S. ? A. T¨ arnlund, editors, Logic Programming, APIC Studies in Data Processing, volume 16, pages 231–251. Academic Press, New York, 1982. 11. A. Colmerauer. Equations and inequations on ?nite and in?nite trees. In Proceedings of the International Conference on Fifth Generation Computer Systems (FGCS’84), pages 85–99, Tokyo, Japan, 1984. ICOT. 12. A. Colmerauer. An introduction to Prolog-III. Communications of the ACM, 33(7):69–90, 1990. 13. A. Cortesi and G. Fil? e. Sharing is optimal. Journal of Logic Programming, 38(3):371–386, 1999. 14. A. Cortesi, B. Le Charlier, and P. Van Hentenryck. Combinations of abstract domains for logic programming: Open product and generic pattern construction. Science of Computer Programming, 38(1–3), 2000. 15. P. Cousot and R. Cousot. Abstract interpretation: A uni?ed lattice model for static analysis of programs by construction or approximation of ?xpoints. In Proceedings of the Fourth Annual ACM Symposium on Principles of Programming Languages, pages 238–252, 1977. 16. P. Cousot and R. Cousot. Abstract interpretation frameworks. Journal of Logic and Computation, 2(4):511–547, 1992. 17. L. Crnogorac, A. D. Kelly, and H. S?ndergaard. A comparison of three occur-check analysers. In R. Cousot and D. A. Schmidt, editors, Static Analysis: Proceedings of the 3rd International Symposium, volume 1145 of Lecture Notes in Computer Science, pages 159–173, Aachen, Germany, 1996. Springer-Verlag, Berlin. 18. P. R. Eggert and K. P. Chow. Logic programming, graphics and in?nite terms. Technical Report UCSB DoCS TR 83-02, Department of Computer Science, University of California at Santa Barbara, 1983.

19

19. G. Erbach. ProFIT: Prolog with Features, Inheritance and Templates. In Proceedings of the 7th Conference of the European Chapter of the Association for Computational Linguistics, pages 180–187, Dublin, Ireland, 1995. 20. M. Filgueiras. A Prolog interpreter working with in?nite terms. In Campbell [7], pages 250–258. 21. F. Giannesini and J. Cohen. Parser generation and grammar manipulation using Prolog’s in?nite trees. Journal of Logic Programming, 3:253–265, 1984. 22. W. Hans and S. Winkler. Aliasing and groundness analysis of logic programs through abstract interpretation and its safety. Technical Report 92–27, Technical University of Aachen (RWTH Aachen), 1992. 23. S. Haridi and D. Sahlin. E?cient implementation of uni?cation of cyclic structures. In Campbell [7], pages 234–249. 24. P. M. Hill, R. Bagnara, and E. Za?anella. Soundness, idempotence and commutativity of set-sharing. Theory and Practice of Logic Programming, 2001. To appear. Available at http://arXiv.org/abs/cs.PL/0102030. 25. B. Intrigila and M. Venturini Zilli. A remark on in?nite matching vs in?nite uni?cation. Journal of Symbolic Computation, 21(3):2289–2292, 1996. 26. D. Jacobs and A. Langen. Accurate and e?cient approximation of variable aliasing in logic programs. In E. L. Lusk and R. A. Overbeek, editors, Logic Programming: Proceedings of the North American Conference, MIT Press Series in Logic Programming, pages 154–165, Cleveland, Ohio, USA, 1989. The MIT Press. 27. J. Ja?ar, J-L. Lassez, and M. J. Maher. Prolog-II as an instance of the logic programming scheme. In M. Wirsing, editor, Formal Descriptions of Programming Concepts III, pages 275–299. North-Holland, 1987. 28. T. Keisu. Tree Constraints. PhD thesis, The Royal Institute of Technology, Stockholm, Sweden, May 1994. 29. A. King. Pair-sharing over rational trees. Journal of Logic Programming, 46(1– 2):139–155, 2000. 30. M. J. Maher. Complete axiomatizations of the algebras of ?nite, rational and in?nite trees. In Proceedings, Third Annual Symposium on Logic in Computer Science, pages 348–357, Edinburgh, Scotland, 1988. IEEE Computer Society. 31. K. Mukai. Constraint Logic Programming and the Uni?cation of Information. PhD thesis, Department of Computer Science, Faculty of Engineering, Tokio Institute of Technology, 1991. 32. C. Pollard and I. A. Sag. Head-Driven Phrase Structure Grammar. University of Chicago Press, Chicago, 1994. 33. F. Scozzari. Abstract domains for sharing analysis by optimal semantics. In J. Palsberg, editor, Static Analysis: 7th International Symposium, SAS 2000, volume 1824 of Lecture Notes in Computer Science, pages 397–412, Santa Barbara, CA, USA, 2000. Springer-Verlag, Berlin. 34. Gert Smolka and Ralf Treinen. Records for logic programming. Journal of Logic Programming, 18(3):229–258, 1994. 35. H. S?ndergaard. An application of abstract interpretation of logic programs: Occur check reduction. In B. Robinet and R. Wilhelm, editors, Proceedings of the 1986 European Symposium on Programming, volume 213 of Lecture Notes in Computer Science, pages 327–338. Springer-Verlag, Berlin, 1986. 36. Swedish Institute of Computer Science, Programming Systems Group. SICStus Prolog User’s Manual, release 3 #0 edition, 1995.

20

赞助商链接

- A hierarchy of constraint systems for data-flow analysis of constraint logic-based language
- Flow Logics for Constraint Based Analysis
- Constraint systems for pattern analysis of constraint logic-based languages
- Data Flow Analysis for CCS
- A Temporal Logic for Data-Flow VHDL
- A practical and flexible flow analysis for higher-order languages
- Abstract Finite-Tree Analysis for Constraint Logic-Based Languages The Complete Unabridged
- Real-time Analysis of Flow Data for Network Attack Detection
- Constraint-based termination analysis of logic programs
- Semantics-based program analysis for logic-based languages using XSB

更多相关文章：
更多相关标签：