Complete Abstract Interpretations made Constructive

Completeness is a desirable, although uncommon, property in abstract interpretation, 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 continuous semantic functions, a constructive characterization of the least complete extension and the greatest complete restriction of an abstract interpretation is given. The existence of more restricted forms of similar abstractions was recently proved by the first two authors. (ii) In projection-based program analysis, our results show that the so-called least backward abstractions of co-continuous semantic functions always exist and can be constructively characterized. This improves considerably over previous works in the field. (iii) Our results generalize the notion of quotient of abstract domains, 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.