Proving partial correctness of guarded horn clauses programs

Masaki Murakami

doi:10.1007/3-540-19426-6_14

Proving partial correctness of guarded horn clauses programs

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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.

Original language	English
Title of host publication	Logic Programming 1987 - Proceedings of the 6th Conference
Editors	Hozumi Tanaka, Koichi Furukawa, Tetsunosuke Fujisaki
Publisher	Springer Verlag
Pages	215-235
Number of pages	21
ISBN (Print)	9783540194262
DOIs	https://doi.org/10.1007/3-540-19426-6_14
Publication status	Published - 1988
Externally published	Yes
Event	6th Conference on Logic Programming, 1987 - Tokyo, Japan Duration: Jun 22 1987 → Jun 24 1987

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	315 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	6th Conference on Logic Programming, 1987
Country/Territory	Japan
City	Tokyo
Period	6/22/87 → 6/24/87

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1007/3-540-19426-6_14

Cite this

Murakami, M. (1988). Proving partial correctness of guarded horn clauses programs. In H. Tanaka, K. Furukawa, & T. Fujisaki (Eds.), Logic Programming 1987 - Proceedings of the 6th Conference (pp. 215-235). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 315 LNCS). Springer Verlag. https://doi.org/10.1007/3-540-19426-6_14

Proving partial correctness of guarded horn clauses programs. / Murakami, Masaki.

Logic Programming 1987 - Proceedings of the 6th Conference. ed. / Hozumi Tanaka; Koichi Furukawa; Tetsunosuke Fujisaki. Springer Verlag, 1988. p. 215-235 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 315 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Murakami, M 1988, Proving partial correctness of guarded horn clauses programs. in H Tanaka, K Furukawa & T Fujisaki (eds), Logic Programming 1987 - Proceedings of the 6th Conference. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 315 LNCS, Springer Verlag, pp. 215-235, 6th Conference on Logic Programming, 1987, Tokyo, Japan, 6/22/87. https://doi.org/10.1007/3-540-19426-6_14

Murakami M. Proving partial correctness of guarded horn clauses programs. In Tanaka H, Furukawa K, Fujisaki T, editors, Logic Programming 1987 - Proceedings of the 6th Conference. Springer Verlag. 1988. p. 215-235. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/3-540-19426-6_14

Murakami, Masaki. / Proving partial correctness of guarded horn clauses programs. Logic Programming 1987 - Proceedings of the 6th Conference. editor / Hozumi Tanaka ; Koichi Furukawa ; Tetsunosuke Fujisaki. Springer Verlag, 1988. pp. 215-235 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{792789ef69fd4b40a74e80bd45939a3f,

title = "Proving partial correctness of guarded horn clauses programs",

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.",

author = "Masaki Murakami",

note = "Publisher Copyright: {\textcopyright} 1988, Springer-Verlag.; 6th Conference on Logic Programming, 1987 ; Conference date: 22-06-1987 Through 24-06-1987",

year = "1988",

doi = "10.1007/3-540-19426-6_14",

language = "English",

isbn = "9783540194262",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "215--235",

editor = "Hozumi Tanaka and Koichi Furukawa and Tetsunosuke Fujisaki",

booktitle = "Logic Programming 1987 - Proceedings of the 6th Conference",

}

TY - GEN

T1 - Proving partial correctness of guarded horn clauses programs

AU - Murakami, Masaki

PY - 1988

Y1 - 1988

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85034823595&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85034823595&partnerID=8YFLogxK

U2 - 10.1007/3-540-19426-6_14

DO - 10.1007/3-540-19426-6_14

M3 - Conference contribution

AN - SCOPUS:85034823595

SN - 9783540194262

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 215

EP - 235

BT - Logic Programming 1987 - Proceedings of the 6th Conference

A2 - Tanaka, Hozumi

A2 - Furukawa, Koichi

A2 - Fujisaki, Tetsunosuke

PB - Springer Verlag

T2 - 6th Conference on Logic Programming, 1987

Y2 - 22 June 1987 through 24 June 1987

ER -

Proving partial correctness of guarded horn clauses programs

Abstract

Publication series

Conference

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this