The Library
P-A LOGIC - A COMPOSITIONAL PROOF SYSTEM FOR DISTRIBUTED PROGRAMS
Tools
UNSPECIFIED (1991) P-A LOGIC - A COMPOSITIONAL PROOF SYSTEM FOR DISTRIBUTED PROGRAMS. DISTRIBUTED COMPUTING, 5 (1). pp. 37-54. ISSN 0178-2770.
Research output not available from this repository.
Request-a-Copy directly from author or use local Library Get it For Me service.
Abstract
This paper describes a compositional proof system called P-A logic for establishing weak total correctness and weak divergence correctness of CSP-like distributed programs with synchronous and asynchronous communication. Each process in a network is specified using logical assertions in terms of a presupposition Pre and an affirmation Aff as a triple {Pre} S {Aff}. For purely sequential programs, these triples reduce to the familiar Hoare triples. In distributed programs, P-A triples allow the behaviour of a process to be specified in the context of assumptions about its communications with the other processes in the network. Safety properties of process communications, and progress properties such as finiteness and freedom from divergence can be proved. An extension of P-A logic allowing proof of deadlock freedom is outlined. Finally, proof rules for deriving some liveness properties of a program from its P-A logic specification are discussed; these properties have the form "Q until R", where Q, R are assertions over communication traces. Other liveness properties may be derived from these properties using the rules of temporal logic.
Item Type: | Journal Article | ||||
---|---|---|---|---|---|
Subjects: | Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software | ||||
Journal or Publication Title: | DISTRIBUTED COMPUTING | ||||
Publisher: | SPRINGER VERLAG | ||||
ISSN: | 0178-2770 | ||||
Official Date: | 1991 | ||||
Dates: |
|
||||
Volume: | 5 | ||||
Number: | 1 | ||||
Number of Pages: | 18 | ||||
Page Range: | pp. 37-54 | ||||
Publication Status: | Published |
Data sourced from Thomson Reuters' Web of Knowledge
Request changes or add full text files to a record
Repository staff actions (login required)
View Item |