School Homepage

Logic Programs as Compact Denotations

Patricia M. Hill
School of Computing
The University of Leeds
Leeds LS2 9JT
England

Fausto Spoto
Dipartimento Scientifico e Tecnologico
Strada Le Grazie
15 Ca' Vignal
37134 Verona
Italy

Abstract:

In this paper, we show how a logic program can provide a compact representation of the abstract denotations used in denotational abstract interpretation where the logic variables express regularity in the abstract behaviour of commands. We show how this representation can be used in the implementation of sign, class and escape analysis for object-oriented programs. We also show that the time and space costs are smaller than those of a ground representation. Moreover, we show that in the case of sign analysis they are comparable to those of an implementation based on binary decision diagrams.

Keywords: Semantics, static analysis, abstract interpretation, debugging.