Abstract
Guarded Horn Clauses (GHC) [Ueda 85] is a parallel programming language based on Horn logic. A verification method of partial correctness for GHC programs is discussed here. The author investigated a Hoare-like axiomatic system for proving partial correctness of GHC programs. This paper presents fragments of the axiomatic system. Programs which generate processes dynamically during the execution or which contain control of nondeterminism by the guard mechanism are verified by these systems.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
[References]
K. L. Clark and S. Gregory, PARLOG: Parallel programming in logic, ACM Trans. on Programming Language and Systems 86, 1986
Y. Kameyama, Axiomatic System for Concurrent Logic Programming Languages, Master's Thesis of the University of Tokyo 1987
T. Kanamori and H. Seki, Verification of Prolog Programs Using an Extension of Execution, Lecture Notes in Comp. Sci., No. 225, 1986
G. Levi and C. Palamidessi, The Declarative Semantics of Logical Read-only Variables, Prc. of Symp. on Logic Programming 85 1985
G. Levi and C. Palamidessi, An Approach to The Declarative Semantics of Synchronization in Logic Language, to appear in Proc. of International Conf. on Logic Programming 87, 1987
M. Murakami and Y. Inagaki, Verification System for Partial Correctness of Communicating Sequential Processes, Systems and Computers in Japan, 1986
M. Murakami, Toward Axiomatic Semantics of Guarded Horn Clauses, 2nd France-Japan Artificial Intelligence and Computer Science Symposium, 1987
V. A. Saraswat, Partial Correctness Semantics for CP [↓, ¦, &], Lecture Notes in Comp. Sci., no. 206, 1985
V. A. Saraswat, GHC: Operational Semantics, Problems, and Relationships with CP (↓, ¦), Prc. of Symp. on Logic Programming 87 1987
N. Saundararajan, Axiomatic Semantics of Communicating Sequential Processes, ACM Trans. on Programming Languages and Systems, Vol. 6, No. 4, 1984
E. Y. Shapiro, Concurrent Prolog: A progress report, Lecture Notes in Comp. Sci. No. 232, 1986
A. Takeuchi, Towards a Semantic Model of GHC, Tec. Rep. of IECE, COMP86-59, 1986
K. Ueda, Guarded Horn Clauses, Tec. Rep. of ICOT, TR-103, 1985
K. Ueda, On Operational Semantics of Guarded Horn Clauses, Tec. Memo of ICOT, TM-0160, 1986
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1988 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Murakami, M. (1988). Proving partial correctness of guarded horn clauses programs. In: Furukawa, K., Tanaka, H., Fujisaki, T. (eds) Logic Programming '87. LP 1987. Lecture Notes in Computer Science, vol 315. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-19426-6_14
Download citation
DOI: https://doi.org/10.1007/3-540-19426-6_14
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-19426-2
Online ISBN: 978-3-540-39267-5
eBook Packages: Springer Book Archive