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:

This paper shows how logic programs can be used to implement the transition functions of denotational abstract interpretation. The logic variables express regularity in the abstract behaviour of commands. The technique is applied here to sign, class and escape analysis for object-oriented programs. We show that the time and space costs using logic programs are smaller than those of a ground relational representation. Moreover, we show that, in the case of sign analysis, our technique requires less memory and has an efficiency comparable to that of an implementation based on binary decision diagrams.

Keywords: Logic programs, denotational semantics, static analysis, abstract interpretation.