Hostname: page-component-74656f9884-g96k6 Total loading time: 0 Render date: 2026-11-10T04:13:43.831Z Has data issue: false hasContentIssue false
  • English
  • Français

A simple correctness proof for magic transformation

Published online by Cambridge University Press:  04 March 2011

WŁODZIMIERZ DRABENT
WŁODZIMIERZ DRABENT*
Affiliation:
Institute of Computer Science, Polish Academy of Sciences, ul. Ordona 21, Pl – 01-237 Warszawa, Poland and Department of Computer and Information Science, Linköpings Universitet, S – 58183 Linköping, Sweden (e-mail: drabent@ipipan.waw.pl)
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

The paper presents a simple and concise proof of correctness of the magic transformation. We believe that it may provide a useful example of formal reasoning about logic programs. The correctness property concerns the declarative semantics. The proof, however, refers to the operational semantics (LD-resolution) of the source programs. Its conciseness is due to applying a suitable proof method.

Keywords

program correctnesslogic programmingmagic transformationdeclarative semanticsLD-resolutionoperational semantics

Information

Type
Regular Papers
Information
Theory and Practice of Logic Programming , Volume 12 , Issue 6 , November 2012 , pp. 929 - 936
Copyright
Copyright © Cambridge University Press 2011

References

Apt, K. R. 1997. From Logic Programming to Prolog. International series in computer science. Prentice-Hall, New Jersey.Google Scholar
Apt, K. R. and Marchiori, E. 1994. Reasoning about Prolog programs: From modes through types to assertions. Formal Aspects of Computing 6, 6A, 743–765.Google Scholar
Beeri, C. and Ramakrishnan, R. 1991. On the power of magic. Journal of Logic Programming 10, 1–4, 255–299.CrossRefGoogle Scholar
Bossi, A. and Cocco, N. 1989. Verifying correctness of logic programs. In TAPSOFT, Vol. 2, Díaz, J. and Orejas, F., Eds. Lecture notes in computer science, vol. 352. Springer, New York, 96–110.Google Scholar
Bossi, A., Gabbrielli, M., Levi, G. and Martelli, M. 1994. The s-semantics approach: Theory and applications. Journal of Logic Programming 19/20, 149–197.Google Scholar
Clark, K. L. 1979. Predicate Logic as Computational Formalism. Technical Report 79/59, Imperial College, London.Google Scholar
Colussi, L. and Marchiori, E. 1991. Proving correctness of logic programs using axiomatic semantics. In Logic Programming, Proceedings of the Eigth International Conference, Furukawa, K., Ed. MIT Press, Cambridge, MA, 629–642.Google Scholar
Deransart, P. 1993. Proof methods of declarative properties of definite programs. Theoretical Computer Science 118, 2, 99–166.Google Scholar
Drabent, W. 1997. A Floyd-Hoare method for Prolog. Linköping electronic articles in computer and information science 2. URL: http://www.ep.liu.se/ea/cis/1997/013/Google Scholar
Drabent, W. and Małuszyński, J. 1988. Inductive assertion method for logic programs. Theoretical Computer Science 59, 133–155.CrossRefGoogle Scholar
Drabent, W. and Miłkowska, M. 2005. Proving correctness and completeness of normal programs – a declarative approach. Theory and Practice of Logic Programming 5, 6, 669–711.Google Scholar
Mascellani, P. and Pedreschi, D. 2002. The declarative side of magic. In Computational Logic: Logic Programming and Beyond, Kakas, A. C. and Sadri, F., Eds. Lecture notes in computer science, vol. 2408. Springer, New York, 83–108.Google Scholar
Nilsson, U. 1995. Abstract interpretation: A kind of magic. Theoretical Computer Science 142, 1, 125–139.Google Scholar
Nilsson, U. and Małuszyński, J. 1995. Logic, Programming and Prolog, 2nd ed. (Previously published by John Wiley). URL: http://www.ida.liu.se/~ulfni/lpp/Google Scholar
Ramakrishnan, R. 1991. Magic templates: A spellbinding approach to logic programs. Journal of Logic Programming 11, 3&4, 189–216.CrossRefGoogle Scholar