Sophisticated analysis algorithms are used in program development environments today to help in deriving information on the static and behavioral properties of programs. Two approaches are adopted for the specification of such algorithms. The operational approach, though practical, has no formal foundation for correctness proofs and is implementation-dependent. The semantics-driven approach has a theoretical foundation based on denotational semantics, but is not supported by practical tools.

This paper enhances the semantics-driven approach to cater to implementation issues. It describes a Structured Program Analysis Refinement Environment (SPARE), which interacts with users in an extended denotational specification language that is flexible and concise. Algorithms can be developed in a modular and structured manner, with implementation details hidden from users. The environment supports the rapid prototyping and testing of analysis algorithms through automatic implementations. The performance of the system is enhanced by incremental evaluation. Correctness proofs can be produced as a result of the denotational nature of the specifications, but they are not covered in the paper.

The paper provides a vivid illustration showing that the gap between theory and practice can indeed be bridged. A small drawback is that the discussion of denotational semantics and other formal notions may be too condensed for the average reader. It would have been useful, for instance, if the authors had announced as early as possible that a glossary of terms is provided in Appendix B.