首页 | 本学科首页   官方微博 | 高级检索  
     


Algebraic specification and proof of a distributed recovery algorithm
Authors:He Jifeng  C. A. R. Hoare
Affiliation:(1) Programming Research Group, Oxford University Computing Laboratory, 8-11 Keble Road, OX1 3QD Oxford, UK
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).He Jifeng received the B.S. degree in mathematics from Fudan University, Shanghai (China), in 1965. Then he taught in the department of mathematics, Shanghai Normal University. In 1972 he moved to East China Normal University where he was a lecturer of computer science. Since September 1986 he has been a professor of computer science at East China Normal University. He is currently working at Oxford University Computing Laboratory. His major research interests are programming language semantics, software engineering and distributed computing.Tony Hoare is Professor of Computation at the University of Oxford. He received his MA from Oxford in Classical Languages, Literature, History and Philosophy. He worked for eight years as programmer, manager and research scientist with a small computer manufacturer. He is the recipient of several honours for his contributions to the study of computer programming languages, and is generally famed for Hoare's Law: inside every large program there is a small program trying to get out.
Keywords:
本文献已被 SpringerLink 等数据库收录!
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号