|
The Correctness of Set-Sharing
Patricia M. Hill
Roberto Bagnara
Enea Zaffanella
Abstract:It is important that practical data flow analysers are backed by reliably proven theoretical results. Sharing is an abstract domain that is a standard choice for sharing analysis for both practical work and further theoretical study. In spite of this, we found that there are 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.
Available: PDF, 300 DPI, 600 DPI, and 1200 DPI PostScript, DVI, BibTeX entry. [Page last updated on December 10, 1999, 11:30:49.] |
|||||
bagnara@cs.unipr.it |
Home | Personal | Papers | Teaching | Links |