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.

Complete abstract interpretations made constructive

RANZATO, FRANCESCO;
1998

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.
Mathematical Foundations of Computer Science 1998, 23rd International Symposium, MFCS'98, Brno, Czech Republic
3540648275
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

Caricamento pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11577/182282
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 13
  • ???jsp.display-item.citation.isi??? 9
social impact