UNSPECIFIED (1991) P-A LOGIC - A COMPOSITIONAL PROOF SYSTEM FOR DISTRIBUTED PROGRAMS. DISTRIBUTED COMPUTING, 5 (1). pp. 37-54. ISSN 0178-2770

Full text not available from this repository.

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
Date:	1991
Volume:	5
Number:	1
Number of Pages:	18
Page Range:	pp. 37-54
Publication Status:	Published
URI:	http://wrap.warwick.ac.uk/id/eprint/22658

Data sourced from Thomson Reuters' Web of Knowledge

Request changes to a record

Actions (login required)

View Item