ALGEBRAIC LAWS FOR NONDETERMINISM AND CONCURRENCY

被引:753
作者
HENNESSY, M
MILNER, R
机构
[1] Univ of Edinburgh, Edinburgh, Scotl, Univ of Edinburgh, Edinburgh, Scotl
关键词
COMPUTER METATHEORY - LOGIC DESIGN - Computer Applications - MATHEMATICAL TECHNIQUES - Algebra;
D O I
10.1145/2455.2460
中图分类号
TP3 [计算技术、计算机技术];
学科分类号
0812 ;
摘要
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 be observation congruent if they are, in all program contexts, equivalent. The behavior of 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.
引用
收藏
页码:137 / 161
页数:25
相关论文
共 11 条
[1]  
Gordon M., 1979, DENOTATIONAL DESCRIP
[2]  
HENNESSY M, 1979, LECTURE NOTES COMPUT, V74, P108
[3]  
HENNESSY MCB, 1980, LECTURE NOTES COMPUT, V85, P299, DOI DOI 10.1007/3-540-10003-2
[4]   CONCURRENT PROCESSES AND THEIR SYNTAX [J].
MILNE, G ;
MILNER, R .
JOURNAL OF THE ACM, 1979, 26 (02) :302-321
[5]  
MILNER R, 1978, LECT NOTES COMPUTER, V64, P71
[6]  
MILNER R, 1980, LECTURE NOTES COMPUT, V92
[7]  
Plotkin G. D., 1976, SIAM Journal on Computing, V5, P452, DOI 10.1137/0205035
[8]  
Pnueli A., 1977, 18th Annual Symposium on Foundations of Computer Science, P46, DOI 10.1109/SFCS.1977.32
[9]  
Pratt V.R., 1976, FOCS, P109, DOI [10.1109/SFCS.1976.27, DOI 10.1109/SFCS.1976.27]
[10]  
SMYTH M, 1978, J COMPUT SYST SCI, V15, P23