Completeness and predicate-based abstract interpretation

ABSTRACT

Traditionally, the theory of abstract interpretation has concentrated on the study of when one interpretation is sound (also safe or correct) with respect to another. We consider the dual notion of when one interpretation is complete with respect to another. Under the usual formulation of abstract interpretation, undecidability in general implies that a finitely computable sound abstraction of the standard interpretation is not complete. (For example, if we simplify 643 * (-192) to (+) * (-) using the “rule of signs” we cannot expect to retrieve -123456 from the resulting (1), even though we are certain that the result is negative.) Based on the idea that compilers can only depend on a finite number of program properties, we augment interpretations with predicate symbols specifying properties of interest (thereby replacing algebraic interpretations with logic interpretations). Interpretation J being sound (resp. complete) with respect to I is now phrased as “all questions (formulae) yielding true for J (resp. I) also yield true for I (resp. J)”. The traditional “rule of signs” turns out to be sound and complete for multiplication but only sound for addition. Sometimes abstract interpretations have spurious domain elements. The state minimisation algorithm for finite deterministic automata can be used to produce a canonical (simplest) abstract interpretation which is sound and complete with respect to any given finite abstract interpretation but possibly simpler to compute. A homomorphism always yields a sound and complete abstraction. Moreover, we show that a sound and complete abstraction map is not necessarily a homomorphism, but its composition with the natural map to the canonical interpretation is a homomorphism, One side-effect of our formulation of abstract interpretation is that it de-emphasises the ordering on the abstract domain which is relegated to an (optional) proof basis.

REFERENCES

• 1: Abramsky, S. Abstract interpretation, logical relations and Kan extensions. Journal of logic and computation, vol. 1 (1), 1990.
• 2: P. N. Benton, Strictness Logic and Polymorphic Invariance, Proceedings of the Second International Symposium on Logical Foundations of Computer Science, p.33-44, July 20-24, 1992
• 3: Patrick Cousot , Radhia Cousot, Inductive definitions, semantics and abstract interpretations, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.83-94, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143184]
• 4: Patrick Cousot , Rahida Cousot, Abstract interpretation and application to logic programs, Journal of Logic Programming, v.13 n.2-3, p.103-179, July 1992 [doi>10.1016/0743-1066(92)90030-7]
• 5: Cousot, P. and Cousot, R. Abstract Interpretation Frameworks. Journal o} Logic and Computation, vol. 2:4, 1992.
• 6: Ernoult, C. and Mycroft, A. Untyped strictness analysis, Journal of Functional Programming, to appear. Draft version appears as technical report 269, Cambridge University Computer Laboratory.
• 7: Paul Hudak , Jonathan Young, Higher-order strictness analysis in untyped lambda calculus, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.97-109, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512653]
• 8: Hunt, L.S. P EI~s generalise projections for strictness analysis. Departmental report DOC 90/14, Dept. of Computing, Imperial College, London, 1990
• 9: Thomas P. Jensen, Strictness analysis in logical form, Proceedings of the 5th ACM conference on Functional programming languages and computer architecture, p.352-366, June 1991, Cambridge, Massachusetts, United States
• 10: Alan. Mycroft , Neil. D. Jones, A relational framework for abstract interpretation, on Programs as data objects, p.156-171, April 1986, Copenhagen, Denmark
• 11: Nielson, F. Ab.,~tract interpretation using domain theory. Ph.D. thesis, Edinburgh University, 1984. Available as computer science report CST-31-84.
• 12: F. Nielson, Two-level semantics and abstract interpretation, Theoretical Computer Science, v.69 n.2, p.117-242, Dec. 11, 1989 [doi>10.1016/0304-3975(89)90091-1]
• 13: Reddy, U.S. and Kamin, S.N. On the power of abstract interpretation. Proc. IEEE International Conference on Computer Languages, IEEE press, 1992.
• 14: R. C. Sekar , Prateek Mishra , I. V. Ramakrishnan, On the power and limitation of strictness analysis based on abstract interpretation, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.37-48, January 21-23, 1991, Orlando, Florida, United States [doi>10.1145/99583.99591]
• 15: Bernhard Steffen, Optimal Data Flow Analysis via Observational Equivalence, Proceedings on Mathematical Foundations of Computer Science 1989, p.492-502, August 28-September 01, 1989
• 16: Steffen, B., Jay, C.B. and Mendler, M. Compositional characterisation of program properties. Informatique thgorique et Applications (AFCET), vol. 26, 1992.
• 17: Philip Wadler , R. J. M. Hughes, Projections for strictness analysis, Proc. of a conference on Functional programming languages and computer architecture, p.385-407, October 1987, Portland, Oregon, United States

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

General Terms:
Algorithms, Languages, Theory, Verification