A Proof System for Communicating Sequential Processes

被引：139

作者：

Apt, Krzysztof R. ^{[1
]}

Francez, Nissim ^{[2
]}

De Roever, Willem P. ^{[3
]}

机构：

[1] Faculty of Economics, University of Rotterdam, P.O. Box 1738, Rotterdam,3000 DR, Netherlands

[2] Department of Computer Science, Technion-Israel Institute of Technology, Haifa, Israel

[3] Department of Computer Science, University of Utrecht, P.O. Box 80.002, Utrecht,3508 TA, Netherlands

来源：

ACM Transactions on Programming Languages and Systems | 1980年 / 2卷 / 03期

基金：

美国国家科学基金会;

关键词：

Programmable logic controllers;

D O I：

10.1145/357103.357110

中图分类号：

学科分类号：

摘要：

An axiomatic proof system is presented for proving partial correctness and absence of deadlock (and failure) of communicating sequential processes. The key (meta) rule introduces cooperation between proofs, a new concept needed to deal with proofs about synchronization by message passing. CSP's new convention for distributed termination of loops is dealt with. Applications of the method involve correctness proofs for two algorithms, one for distributed partitioning of sets, the other for distributed computation of the greatest common divisor of n numbers. © 1980 ACM.

引用

页码：359 / 385