Algebraic specification and proof of a distributed recovery algorithm
type: Item
instance of: scholarly article
title: Algebraic specification and proof of a distributed recovery algorithm
zbMATH Open document ID: 0621.68008
DOI: 10.1007/BF01786251
author: Jifeng He
author: Tony Hoare
published in: Distributed Computing
publication date: 1987-01-01T00:00:00Z
review text: 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'' [\textit{C. A. R. Hoare}, Prentice-Hall (Englewood Cliffs 1985)] and the proofs of correctness are conducted wholly by application of algebraic laws (together with the unique fixed point theorem).
Mathematics Subject Classification ID: 68P05
Mathematics Subject Classification ID: 68N25
Mathematics Subject Classification ID: 68Q60
zbMATH DE Number: 4007702
zbMATH Keywords: deterministic process
zbMATH Keywords: Communicating Sequential Processes
zbMATH Keywords: proofs of correctness
zbMATH Keywords: fixed point
MaRDI profile type: Publication
cites work: Can programming be liberated from the von Neumann style?
cites work: A Transformation System for Developing Recursive Programs
cites work: Q3777424
cites work: Time, clocks, and the ordering of events in a distributed system
description: scientific article; zbMATH DE number 4007702