Hostname: page-component-7c8c6479df-ph5wq Total loading time: 0 Render date: 2024-03-28T13:49:57.644Z Has data issue: false hasContentIssue false

Sequence-based abstract interpretation of Prolog

Published online by Cambridge University Press:  18 December 2001

BAUDOUIN LE CHARLIER
Affiliation:
Institut d'Informatique, University of Namur, 21 rue Grandgagnage, B-5000 Namur, Belgium
SABINA ROSSI
Affiliation:
Dipartimento di Informatica, Università di Venezia, via Torino 155, 30172 Venezia, Italy
PASCAL VAN HENTENRYCK
Affiliation:
Department of Computer Science, Brown University, P.O. Box 1910, Providence RI 02912, USA

Abstract

Abstract interpretation is a general methodology for systematic development of program analyses. An abstract interpretation framework is centered around a parametrized non-standard semantics that can be instantiated by various domains to approximate different program properties. Many abstract interpretation frameworks and analyses for Prolog have been proposed, which seek to extract information useful for program optimization. Although motivated by practical considerations, notably making Prolog competitive with imperative languages, such frameworks fail to capture some of the control structures of existing implementations of the language. In this paper, we propose a novel framework for the abstract interpretation of Prolog which handles the depth-first search rule and the cut operator. It relies on the notion of substitution sequence to model the result of the execution of a goal. The framework consists of (i) a denotational concrete semantics, (ii) a safe abstraction of the concrete semantics defined in terms of a class of post-fixpoints, and (iii) a generic abstract interpretation algorithm. We show that traditional abstract domains of substitutions may easily be adapted to the new framework, and provide experimental evidence of the effectiveness of our approach. We also show that previous work on determinacy analysis, that was not expressible by existing abstract interpretation frameworks, can be seen as an instance of our framework. The ideas developed in this paper can be applied to other logic languages, notably to constraint logic languages, and the theoretical approach should be of general interest for the analysis of many non-deterministic programming languages.

Type
Research Article
Copyright
© 2002 Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)