A theory of abstract interpretation that is useful for analyzing calculi of computation is addressed in this paper. This is illustrated by formalizing two analyses for the ambient calculus, which can be seen as an extension of a large subset of the &pgr;-calculus, where active processes are allowed to move between sites. A constraint-based formalism based on flow logic is employed, which overcomes the drawback of previous proposals where processes were required to be in “non-standard form.”

The paper is well organized. First, a precise exponential (time and space) analysis is constructed that counts occurrences of ambients. The analysis obtains its precision by combining the powerful, constraint-based representation of ambients and capabilities with the use of specifications written in a flow logic. Then, a notion is formalized about how to induce constraint-based analyses that meet specific criteria regarding complexity and precision. Finally, a less precise, but practical (that is, suitable for implementation) control flow analysis is derived from the counting analysis in a systematic way. As predicted, correctness, as well the existence of least (or best) solutions, are derived from the correctness of the counting analysis using the general theory. Proofs of results are given in the appendix.

Overall, this is an interesting contribution to the existing research in this area. A valuable aspect of this development is in showing that abstract interpretation and constraint-based analyses naturally complement the use of type systems for analyzing calculi of computation. Unavoidably, the constructions and examples seem rather complex, and make for arduous reading. Nevertheless, the paper should be of interest to the specialized reader concerned with the analysis of calculi of computation. The presentation would be improved by including more examples and gentle explanations for non-experienced readers.