The Correctness of Set-Sharing

Patricia M. Hill
School of Computer Studies
University of Leeds
Leeds, LS2 9JT
United Kingdom

Roberto Bagnara
Dipartimento di Matematica e Informatica
Università di Parma
Parco Area delle Scienze 53/A
I-43124 Parma
Italy

Enea Zaffanella
Servizio IX Automazione
Università di Modena
Italy

Abstract:

It is important that practical data flow analysers are backed by reliably proven theoretical results. Abstract interpretation provides a sound mathematical framework and necessary generic properties for an abstract domain to be well-defined and sound with respect to the concrete semantics. In logic programming, the abstract domain Sharing is a standard choice for sharing analysis for both practical work and further theoretical study. In spite of this, we found that there were no satisfactory proofs for the key properties of commutativity and idempotence that are essential for Sharing to be well-defined and that published statements of the safeness property assumed the occur-check. This paper provides a generalisation of the abstraction function for Sharing that can be applied to any language, with or without the occur-check. The results for safeness, idempotence and commutativity for abstract unification using this abstraction function are given.

Keywords: abstract interpretation, logic programming, occur-check, rational trees, set-sharing.

Available: PDF, 300 DPI, 600 DPI, and 1200 DPI PostScript, DVI, BibTeX entry.

[Page last updated on January 22, 2000, 20:38:36.]

Home | Personal | Papers | Teaching | Links

Home

Personal Info

Papers

Teaching

Links

The Correctness of Set-Sharing

Abstract: