Abstract
Completeness is a desirable, although uncommon, property of abstract interpretations, formalizing the intuition that, relatively to the underlying abstract domains, the abstract semantics is as precise as possible. We consider here the most general form of completeness, where concrete semantic functions can have different domains and ranges, a case particularly relevant in functional programming. In this setting, our main contributions are as follows. (i) Under the weak and reasonable hypothesis of dealing with continuous semantic functions, a constructive characterization of complete abstract interpretations is given. (ii) It turns out that completeness is an abstract domain property. By exploiting (i), we therefore provide explicit constructive characterizations for the least complete extension and the greatest complete restriction of abstract domains. This considerably extends previous work by the first two authors, who recently proved results of mere existence for more restricted forms of least complete extension and greatest complete restriction. (iii) Our results permit to generalize, from a natural perspective of completeness, the notion of quotient of abstract interpretations, a tool introduced by Cortesi et al. for comparing the expressive power of abstract interpretations. Fairly severe hypotheses are required for Cortesi et al.'s quotients to exist. We prove instead that continuity of the semantic functions guarantees the existence of our generalized quotients.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
R. Bagnara, P.M. Hill, and E. Zaffanella. Set-sharing is redundant for pair-sharing. In Proc. 4th Int. Static Analysis Symp., LNCS 1302:53–67, 1997.
G. Birkhoff. Lattice Theory. AMS Colloq. Publications vol. XXV, 3rd ed., 1967.
G.L. Burn, C. Hankin, and S. Abramsky. Strictness analysis for higher-order functions. Sci. Comput. Program., 7:249–278, 1986.
A. Cortesi, G. Filé, and W. Winsborough. The quotient of an abstract interpretation. Theor. Comput. Sci., 202(1–2):163–192, 1998.
P. Cousot. Méthodes itératives de construction et d'approximation de points fixes d'opérateurs monotones sur un treillis, analyse sémantique des programmes. PhD thesis, Université Scientifique et Médicale de Grenoble, 1978.
P. Cousot. Completeness in abstract interpretation (Invited Lecture). In Proc. 1995 Joint Italian-Spanish Conference on Declarative Programming, pp. 37–38, 1995.
P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proc. 4th ACM POPL, pp. 238–252, 1977.
P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Proc. 6th ACM POPL, pp. 269–282, 1979.
P. Cousot and R. Cousot. Inductive definitions, semantics and abstract interpretation. In Proc. 19th ACM POPL, pp. 83–94, 1992.
P. Cousot and R. Cousot. Abstract interpretation of algebraic polynomial systems. In Proc. 6th AMAST Conf., LNCS 1349:138–154, 1997.
R. Giacobazzi and F. Ranzato. Refining and compressing abstract domains. In Proc. 24th ICALP, LNCS 1256:771–781, 1997.
R. Giacobazzi and F. Ranzato. Completeness in abstract interpretation: a domain perspective. In Proc. 6th AMAST Conf., LNCS 1349:231–245, 1997.
D. Jacobs and A. Langen. Static analysis of logic programs for independent AND-parallelism. J. Logic Program., 13(2–3):154–165, 1992.
K. Marriott and H. SØndergaard. Precise and efficient groundness analysis for logic programs. ACM Lett. Program. Lang. Syst., 2(1–4):181–196, 1993.
A. Mycroft. Abstract interpretation and optimising transformations for applicative programs. PhD thesis, CST-15-81, Univ. of Edinburgh, 1981.
A. Mycroft. Completeness and predicate-based abstract interpretation. In Proc. ACM PEPM Conf., pp. 179–185, 1993.
U.S. Reddy and S.N. Kamin. On the power of abstract interpretation. Computer Languages, 19(2):79–89, 1993.
R.C. Sekar, P. Mishra, and I.V. Ramakrishnan. On the power and limitation of strictness analysis. J. ACM, 44(3):505–525, 1997.
H. SØndergaard. An application of abstract interpretation of logic programs: occur check reduction. In Proc. ESOP '86, LNCS 213:327–338, 1986.
B. Steffen. Optimal data flow analysis via observational equivalence. In Proc. 14th MFCS Symp., LNCS 379:492–502, 1989.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Giacobazzi, R., Ranzato, F., Scozzari, F. (1998). Complete abstract interpretations made constructive. In: Brim, L., Gruska, J., Zlatuška, J. (eds) Mathematical Foundations of Computer Science 1998. MFCS 1998. Lecture Notes in Computer Science, vol 1450. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0055786
Download citation
DOI: https://doi.org/10.1007/BFb0055786
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64827-7
Online ISBN: 978-3-540-68532-6
eBook Packages: Springer Book Archive