Algebraic specification and proof of a distributed recovery algorithm

He Jifeng; C. A.R. Hoare

doi:10.1007/BF01786251

Algebraic specification and proof of a distributed recovery algorithm

He Jifeng
, C. A.R. Hoare^*

^*Corresponding author for this work

University of Oxford

Research output: Contribution to journal › Article › peer-review

17 Scopus citations

Abstract

An algebraic specification is given of an algorithm for recovery from catastrophe by a deterministic process. A second version of the algorithm also includes check-points. The algorithms are formulated in the notations of Communicating Sequential Processes (Hoare 1985) and the proofs of correctness are conducted wholly by application of algebraic laws (together with the unique fixed point theorem).

Original language	English
Pages (from-to)	1-12
Number of pages	12
Journal	Distributed Computing
Volume	2
Issue number	1
DOIs	https://doi.org/10.1007/BF01786251
State	Published - Mar 1987
Externally published	Yes

Access to Document

10.1007/BF01786251

Cite this

@article{567cba51a4e24d39b225586a1a10dfb7,

title = "Algebraic specification and proof of a distributed recovery algorithm",

abstract = "An algebraic specification is given of an algorithm for recovery from catastrophe by a deterministic process. A second version of the algorithm also includes check-points. The algorithms are formulated in the notations of Communicating Sequential Processes (Hoare 1985) and the proofs of correctness are conducted wholly by application of algebraic laws (together with the unique fixed point theorem).",

author = "He Jifeng and Hoare, \{C. A.R.\}",

year = "1987",

month = mar,

doi = "10.1007/BF01786251",

language = "英语",

volume = "2",

pages = "1--12",

journal = "Distributed Computing",

issn = "0178-2770",

publisher = "Springer Verlag",

number = "1",

}

TY - JOUR

T1 - Algebraic specification and proof of a distributed recovery algorithm

AU - Jifeng, He

AU - Hoare, C. A.R.

PY - 1987/3

Y1 - 1987/3

N2 - An algebraic specification is given of an algorithm for recovery from catastrophe by a deterministic process. A second version of the algorithm also includes check-points. The algorithms are formulated in the notations of Communicating Sequential Processes (Hoare 1985) and the proofs of correctness are conducted wholly by application of algebraic laws (together with the unique fixed point theorem).

AB - An algebraic specification is given of an algorithm for recovery from catastrophe by a deterministic process. A second version of the algorithm also includes check-points. The algorithms are formulated in the notations of Communicating Sequential Processes (Hoare 1985) and the proofs of correctness are conducted wholly by application of algebraic laws (together with the unique fixed point theorem).

UR - https://www.scopus.com/pages/publications/0023215004

U2 - 10.1007/BF01786251

DO - 10.1007/BF01786251

M3 - 文章

AN - SCOPUS:0023215004

SN - 0178-2770

VL - 2

SP - 1

EP - 12

JO - Distributed Computing

JF - Distributed Computing

IS - 1

ER -

Algebraic specification and proof of a distributed recovery algorithm

Abstract

Access to Document

Other files and links

Fingerprint

Cite this