Abstract
Certain properties of logic programs are inexpressible in terms of their declarative semantics. On example of such properties would be the actual form of procedure calls and successes which occur during computations of a program. They are often used by programmers in their informal reasoning. In this paper, the inductive assertion method for proving partial correctness of logic programs is introduced and proved sound. The method makes it possible to formulate and prove properties which are inexpressible in terms of the declarative semantics. An execution mechanism using the Prolog computation rule and arbitrary search strategy (eg. OR-parallelism or Prolog backtracking) is assumed. The method may be also used to specify the semantics of some extra-logical built-in procedures for which the declarative semantics is not applicable.
This research has been partially supported by the National Swedish Board for Technical Development, projekt nr STUF 85-3166 and STU 86-3372.
Chapter PDF
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Apt, K.R. and van Emden, M.H., “Contributions to the Theory of Logic Programming”, J.ACM. 29, 3 (July 1982), 841–862
D.L. Bowen, L. Byrd, F.C.N. Pereira, L.M. Pereira and D.H.D. Warren, “Prolog-20 user's manual”, 1984
W.Drabent and J. Małuszyński, Proving runtime properties of logic programs, Research Report LITH-IDA-R-86-23, Linköping University, July 1986
Floyd, R.W., “Assigning Meanings to Programs”, Proc.Symp.Appl.Math., Vol. 19: Mathematical Aspects of Computer Science (J.T.Schwartz, ed.), pp. 19–32, American Mathematical Society, Providence, Rhode Island, 1967
Francez,N., Grumberg,O., Katz,S., Pnuelli,A., “Proving Termination of Prolog Programs” in “Logics of Programs. Proceedings, 1985”, ed. by R.Parikh, Springer Lecture Notes in Computer Science 193, 89–105
Hoare, C.A.R. “An Axiomatic Basis for Computer Programming”, Comm. ACM 12, 10 (Oct. 1969), 576–580,583
Hogger, C.J. “Derivation of Logic Programs”, J.ACM 28, 2 (April 1981), 372–392
Lloyd,J.W. “Foundations of Logic Programming”, Springer-Verlag 1984
Mellish,C.S. “Abstract Interpretation of Prolog Programs”, Third International Conference on Logic Programming, London, July 1986 and “The Automatic Generation of Mode Declarations for Prolog Programs”, DAI Research Paper 163, Dept of Artificial Intelligence, University of Edinburgh, 1981
Tarlecki, A., “A Language of Specified Programs”, Science of Computer Programming 5 (1985) 59–81
Author information
Authors and Affiliations
Corresponding author
Editor information
Rights and permissions
Copyright information
© 1987 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Drabent, W., Małuszyński, J. (1987). Inductive assertion method for logic programs. In: Ehrig, H., Kowalski, R., Levi, G., Montanari, U. (eds) TAPSOFT '87. TAPSOFT 1987. Lecture Notes in Computer Science, vol 250. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0014980
Download citation
DOI: https://doi.org/10.1007/BFb0014980
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-17611-4
Online ISBN: 978-3-540-47717-4
eBook Packages: Springer Book Archive