ALGEBRAIC LAWS FOR NONDETERMINISM AND CONCURRENCY
ALGEBRAIC LAWS FOR NONDETERMINISM AND CONCURRENCY
复制标题
DOI：
10.1145/2455.2460
复制
发表时间：
1985-01-01
影响因子：
2.5
通讯作者：
MILNER, R
中科院分区：
文献类型：
--
作者：
HENNESSY, M;MILNER, R
由于非确定性并发程序通常可能与其环境重复通信，因此其含义不能自然地呈现为输入/输出函数（正如在语义的指称方法中经常所做的那样）。本文提出了一种替代方案。首先，定义两个程序或程序部分对于所有观察者来说是等效的；那么如果两个程序部分在所有程序上下文中都是等价的，则称它们是观察一致的。程序部分的行为，即其含义，被定义为其观察同余类。本文证明，对于表达有限（终止）行为的一系列简单语言，在每种情况下观察同余都可以用代数公理化。此外，通过添加递归和另一个简单的扩展，这里描述的代数语言成为一种用于编写和指定并发程序以及证明其属性的微积分。
Since a nondeterministic and concurrent program may, in general, communicate repeatedly with its environment, its meaning cannot be presented naturally as an input/output function (as is often done in the denotational approach to semantics). In this paper, an alternative is put forth. First, a definition is given of what it is for two programs or program parts to be equivalent for all observers; then two program parts are said to beobservation congruentif they are, in all program contexts, equivalent. Thebehaviorof a program part, that is, its meaning, is defined to be its observation congruence class.The paper demonstrates, for a sequence of simple languages expressing finite (terminating) behaviors, that in each case observation congruence can be axiomatized algebraically. Moreover, with the addition of recursion and another simple extension, the algebraic language described here becomes a calculus for writing and specifying concurrent programs and for proving their properties.