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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
R. Bagnara, P. M. Hill, and E. Zaffanella. Set-sharing is redundant for pair-sharing. In P. Van Hentenryck, editor, Static Analysis: Proceedings of the 4th International Symposium, volume 1302 of Lecture Notes in Computer Science, pages 53–67, Paris, France, 1997. Springer-Verlag, Berlin.
M. Bruynooghe and M. Codish. Freeness, sharing, linearity and correctness — All at once. In P. Cousot, M. Falaschi, G. Filé, and A. Rauzy, editors, Static Analysis, Proceedings of the Third International Workshop, volume 724 of Lecture Notes in Computer Science, pages 153–164, Padova, Italy, 1993. Springer-Verlag, Berlin. An extended version is available as Technical Report CW 179, Department of Computer Science, K.U. Leuven, September 1993.
K. L. Clark. Negation as failure. In H. Gallaire and J. Minker, editors, Logic and Databases, pages 293–322, Toulouse, France, 1978. Plenum Press.
M. Codish, D. Dams, G. Filé, and M. Bruynooghe. Freeness analysis for logic programs-and correctness? In D. S. Warren, editor, Logic Programming: Proceedings of the Tenth International Conference on Logic Programming, MIT Press Series in Logic Programming, pages 116–131, Budapest, Hungary, 1993. The MIT Press. An extended version is available as Technical Report CW 161, Department of Computer Science, K.U. Leuven, December 1992.
A. Colmerauer. Prolog and Infinite Trees. In K. L. Clark and S. Å. Tärnlund, editors, Logic Programming, APIC Studies in Data Processing, volume 16, pages 231–251. Academic Press, New York, 1982.
A. Colmerauer. Equations and inequations on fiite and infinite trees. In Proceedings of the International Conference on Fifth Generation Computer Systems (FGCS’84), pages 85–99, Tokyo, Japan, 1984. ICOT.
P. M. Hill, R. Bagnara, and E. Zaffanella. The correctness of set-sharing. Technical Report 98.03, School of Computer Studies, University of Leeds, 1998.
D. Jacobs and A. Langen. Accurate and efficient approximation of variable aliasing in logic programs. In E. L. Lusk and R. A. Overbeek, editors, Logic Programming: Proceedings of the North American Conference, MIT Press Series in Logic Programming, pages 154–165, Cleveland, Ohio, USA, 1989. The MIT Press.
D. Jacobs and A. Langen. Static analysis of logic programs for independent AND parallelism. Journal of Logic Programming, 13(2amp;3):291–314, 1992.
J. Jaffar, J-L. Lassez, and M. J. Maher. Prolog-II as an instance of the logic programming scheme. In M. Wirsing, editor, Formal Descriptions of Programming Concepts III, pages 275–299. North Holland, 1987.
T. Keisu. Tree Constraints. PhD thesis, The Royal Institute of Technology, Stockholm, Sweden, May 1994. Also available in the SICS Dissertation Series: SICS/D 16SE.
A. King. A synergistic analysis for sharing and groundness which traces linearity. In D. Sannella, editor, Proceedings of the Fifth European Symposium on Programming, volume 788 of Lecture Notes in Computer Science, pages 363–378, Edinburgh, UK, 1994. Springer-Verlag, Berlin.
A. King and P. Soper. Depth-k sharing and freeness. In P. Van Hentenryck, editor, Logic Programming: Proceedings of the Eleventh International Conference on Logic Programming, MIT Press Series in Logic Programming, pages 553–568, Santa Margherita Ligure, Italy, 1994. The MIT Press.
A. Langen. Static Analysis for Independent And-Parallelism in Logic Programs. PhD thesis, Computer Science Department, University of Southern California, 1990. Printed as Report TR 91-05.
M. J. Maher. Complete axiomatizations of the algebras of finite, rational and infinite trees. In Proceedings, Third Annual Symposium on Logic in Computer Science, pages 348–357, Edinburgh, Scotland, 1988. IEEE Computer Society.
K. Muthukumar and M. Hermenegildo. Compile-time derivation of variable dependency using abstract interpretation. Journal of Logic Programming, 13(2&3):315–347, 1992.
J. A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1):23–41, 1965.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hill, P.M., Bagnara, R., Zaffanella, E. (1998). The Correctness of Set-Sharing. In: Levi, G. (eds) Static Analysis. SAS 1998. Lecture Notes in Computer Science, vol 1503. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49727-7_6
Download citation
DOI: https://doi.org/10.1007/3-540-49727-7_6
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65014-0
Online ISBN: 978-3-540-49727-1
eBook Packages: Springer Book Archive