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.File | Dimensione | Formato | |
---|---|---|---|
published-paper-springer.pdf
accesso aperto
Tipologia:
Published (publisher's version)
Licenza:
Accesso gratuito
Dimensione
768.7 kB
Formato
Adobe PDF
|
768.7 kB | Adobe PDF | Visualizza/Apri |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.