NPATH is a metric introduced by Brian A. Nejmeh (Communications of the ACM, 31(2):188-200, 1988) that is aimed at overcoming some important limitations of McCabe’s cyclomatic complexity metric. Despite the fact that the declared NPATH objective is to count the number of acyclic execution paths through a function, the definition given for the C language in Nejmeh’s paper fails to do so even for very simple programs. We show that counting the number of acyclic paths in CFG is unfeasible in general. Then we define a new metric for C -like languages, called $A C P A T H$, that allows to quickly compute a very good estimation of the number of acyclic execution paths through the given function. We show that, if the function body does not contain backward gotos and does not contain jumps into a loop from outside the loop (which is the case for all MISRA-compliant programs), then such estimation is actually exact.

Abstract Since the seminal work of Cousot and Halbwachs, the domain of convex polyhedra has been employed in several systems for the analysis and verification of hardware and software components. Although most implementations of the polyhedral operations assume that the polyhedra are topologically closed (i.e., all the constraints defining them are non-strict), several analyzers and verifiers need to compute on a domain of convex polyhedra that are not necessarily closed (NNC). The usual approach to implementing NNC polyhedra is to embed them into closed polyhedra in a higher dimensional vector space and reuse the tools and techniques already available for closed polyhedra. In this work we highlight and discuss the issues underlying such an embedding for those implementations that are based on the double description method, where a polyhedron may be described by a system of linear constraints or by a system of generating rays and points. Two major achievements are the definition of a theoretically clean, high-level user interface and the specification of an efficient procedure for removing redundancies from the descriptions of NNC polyhedra.

$\textup{\textsf{Sharing}}$ , an abstract domain developed by D. Jacobs and A. Langen for the analysis of logic programs, derives useful aliasing information. It is well-known that a commonly used core of techniques, such as the integration of $\textup{\textsf{Sharing}}$ with freeness and linearity information, can significantly improve the precision of the analysis. However, a number of other proposals for refined domain combinations have been circulating for years. One feature that is common to these proposals is that they do not seem to have undergone a thorough experimental evaluation even with respect to the expected precision gains. In this paper we experimentally evaluate: helping $\textup{\textsf{Sharing}}$ with the definitely ground variables found using $\textit{Pos}$ , the domain of positive Boolean formulas; the incorporation of explicit structural information; a full implementation of the reduced product of $\textup{\textsf{Sharing}}$ and $\textit{Pos}$ ; the issue of reordering the bindings in the computation of the abstract $\mgu$ ; an original proposal for the addition of a new mode recording the set of variables that are deemed to be ground or free; a refined way of using linearity to improve the analysis; the recovery of hidden information in the combination of $\textup{\textsf{Sharing}}$ with freeness information. Finally, we discuss the issue of whether tracking compoundness allows the computation of more sharing information.

We present a generic framework for defining and solving interval constraints on any set of domains (finite or infinite) that are lattices. The approach is based on the use of a single form of constraint similar to that of an indexical used by CLP for finite domains and on a particular generic definition of an interval domain built from an arbitrary lattice. We provide the theoretical foundations for this framework and a schematic procedure for the operational semantics. Examples are provided that illustrate how new (compound) constraint solvers can be constructed from existing solvers using lattice combinators and how different solvers (possibly on distinct domains) can communicate and hence, cooperate in solving a problem. We describe the language clp ( L ), which is a prototype implementation of this framework and discuss ways in which this implementation may be improved.

It is well known that freeness and linearity information positively interact with aliasing information, allowing both the precision and the efficiency of the sharing analysis of logic programs to be improved. In this paper, we present a novel combination of set-sharing with freeness and linearity information, which is characterized by an improved abstract unification operator. We provide a new abstraction function and prove the correctness of the analysis for both the finite tree and the rational tree cases. Moreover, we show that the same notion of redundant information as identified in Bagnara et al. (2000) and Zaffanella et al. (2002) also applies to this abstract domain combination: this allows for the implementation of an abstract unification operator running in polynomial time and achieving the same precision on all the considered observable properties.

This paper is concerned with the type analysis of logic programs where, by type, we mean a property closed under instantiation. We define a chain of abstractions from Herbrand constraints to logical formulas via the set of their solutions. Every step of the chain is an instance of abstract interpretation. The use of logical formulas for type analysis is a generalization of the traditional Boolean domains Def and Pos for groundness analysis. In this context, implication is the logical counterpart of the use of linear refinement. While logical formulas can sometime be used for an actual implementation of our domains, in the general case they are infinite objects. Therefore, we apply a final abstraction from possibly infinite logical formulas to (finite) logic programs. Thus, logic programs are themselves used for the type analysis of logic programs. The advantage of our technique with respect to the many frameworks for type analysis present in the literature is that we have developed our domains by using the formal techniques of abstract interpretation and linear refinement. Therefore, their construction is guided by the underlying theory, from which their properties are derived.

It is important that practical data-flow analyzers are backed by reliably proven theoretical results. Abstract interpretation provides a sound mathematical framework and necessary generic properties for an abstract domain to be well-defined and sound with respect to the concrete semantics. In logic programming, the abstract domain Sharing is a standard choice for sharing analysis for both practical work and further theoretical study. In spite of this, we found that there were no satisfactory proofs for the key properties of commutativity and idempotence that are essential for Sharing to be well-defined and that published statements of the soundness of Sharing assume the occurs-check. This paper provides a generalization of the abstraction function for Sharing that can be applied to any language, with or without the occurs-check. Results for soundness, idempotence and commutativity for abstract unification using this abstraction function are proven.

Complementation, the inverse of the reduced product operation, is a technique for systematically finding minimal decompositions of abstract domains. Filé and Ranzato advanced the state of the art by introducing a simple method for computing a complement. As an application, they considered the extraction by complementation of the pair-sharing domain PS from the Jacobs and Langen's set-sharing domain SH. However, since the result of this operation was still SH, they concluded that PS was too abstract for this. Here, we show that the source of this result lies not with PS but with SH and, more precisely, with the redundant information contained in SH with respect to ground-dependencies and pair-sharing. In fact, a proper decomposition is obtained if the non-redundant version of SH, PSD, is substituted for SH. To establish the results for PSD, we define a general schema for subdomains of SH that includes PSD and Def as special cases. This sheds new light on the structure of PSD and exposes a natural though unexpected connection between Def and PSD. Moreover, we substantiate the claim that complementation alone is not sufficient to obtain truly minimal decompositions of domains. The right solution to this problem is to first remove redundancies by computing the quotient of the domain with respect to the observable behavior, and only then decompose it by complementation.

We present verification methods for logic programs with delay declarations. The verified properties are termination and freedom from errors related to built-ins. Concerning termination, we present two approaches. The first approach tries to eliminate the well-known problem of speculative output bindings. The second approach is based on identifying the predicates for which the textual position of an atom using this predicate is irrelevant with respect to termination. Three features are distinctive of this work: it allows for predicates to be used in several modes; it shows that block declarations, which are a very simple delay construct, are sufficient to ensure the desired properties; it takes the selection rule into account, assuming it to be as in most Prolog implementations. The methods can be used to verify existing programs and assist in writing new programs.

Sharing, a domain due to D. Jacobs and A. Langen for the analysis of logic programs, derives useful aliasing information.It is well-known that a commonly used core of techniques, such as the standard integration of Sharing with freeness and linearity information, can signi cantly improve the precision of Sharing.However, a numb e rof other proposals for re ned domain combinations have been circulating for years.One feature that is common to these proposals is that they do not seem to have undergone a thorough experimental evaluation even with respect to the expected precision gains.In this paper, we discuss and/or experimentally evaluate: helping Sharing with de nitely ground variables computed with Pos; the incorporation of explicit structural information into the domain of analysis; more sophisticated ways of integrating Sharing and Pos; the issue of reordering the bindings in the computation of the abstract mgu; an original proposal concerning the addition of a domain recording the set of variables that are deemed to b eground or free; a more re ned way of using linearity to improve the analysis; the issue of whether tracking compoundness allows to compute more precise sharing information; and, nally, the recovery of hidden information in the combination of Sharing with the usual domain for freeness.

This paper presents some supporting transformations for the partial evaluation of logic programs. A logic language is often used to specify a program. If such a specification is to be implemented by means of a logic programming language it is desirable that the programmer should omly have to consider the declarative meaning of the predicates being defined. However, such a program may be very inefficient and the program may have to be transformed to another program which computes the same answers but with improved efficiency. Of the known transformation techniques there is one that is called ‘unfolding’. This performs some of the computation at compile time. In addition, for a particular application, it may be possible to specialize a program so that the transformed program computes the required answers for only a restricted set of goals. Partial evaluation is a program transformation that combines the unfolding and specialization techniques. In order that any answer computed using a partially evaluated program could also have been computed using the original program, it is neccessary that the partial evaluation satisfies certian conditions (called coveredness and independence). Unfortunately, this may prevent the partial evalution achieving its aim of producing a more efficient program. By means of a transformation that dynamically introduces new predicates and their definitions, we show how the restrictions caused by these conditions can be overcome. A partial evaluation will, in general, contain redundant functions and unnecessary repetition of variables. This can cause inefficiency in the use of space and time by the transformed program. The second transformation described here cleans up a partial evaluation removing any unnecessary symbols.

‘In successful pruning it is very necessary to know a certain amount about your subject’s mode of living. In particular it is essential to understand the factors which influence vigour, because pruning is so very much related to and governed by degree of growth. It is for these reasons that the opening pages deal with theoretical information which is of importance if the subject is to be properly understood.’ Simple Pruning, N. Catchpole, W. & H. L. Collingridge Ltd, 1930.