Restructuring a Concurrent Refinement Algebra

被引：0

作者：

Hayes, Ian J. ^{[1
]}

Meinicke, Larissa A. ^{[1
]}

Evangelou-Oost, Naso ^{[1
]}

机构：

[1] Univ Queensland, Sch Elect Engn & Comp Sci, Brisbane, Qld 4072, Australia

来源：

RELATIONAL AND ALGEBRAIC METHODS IN COMPUTER SCIENCE, RAMICS 2024 | 2024年 / 14787卷

关键词：

KLEENE ALGEBRA;

D O I：

10.1007/978-3-031-68279-7_9

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

The concurrent refinement algebra has been developed to support rely/guarantee reasoning about concurrent programs. The algebra supports atomic commands and defines parallel composition as a synchronous operation, as in Milner's SCCS. In order to allow specifications to be combined, the algebra also provides a weak conjunction operation, which is also a synchronous operation that shares many properties with parallel composition. The three main operations, sequential composition, parallel composition and weak conjunction, all respect a (weak) quantale structure over a lattice of commands. Further structure involves combinations of pairs of these operations: sequential/parallel, sequential/weak conjunction and parallel/weak conjunction, each pair satisfying a weak interchange law similar to Concurrent Kleene Algebra. Each of these pairs satisfies a common biquantale structure. Additional structure is incorporated in the form of compatible sets of commands, including tests and atomic commands. These facilitate stronger (equality) interchange and distributive laws. This paper describes the result of restructuring the algebra to better exploit these commonalities. The algebra is implemented in Isabelle/HOL.

引用

页码：135 / 155

页数：21

共 27 条

[1]

AARTS C, 1995, INFORM PROCESS LETT, V53, P131, DOI 10.1016/0020-0190(94)00195-5

[2]

Aczel P.H.G., 1983, Private communication to Cliff Jones

[3]

Agular M., 2010, CRM Monograph Series, V29

[4]

Back Ralph-Johan., 1998, Graduate Texts in Computer Science, DOI DOI 10.1007/978-1-4612-1674-2

[5] Designing a semantic model for a wide-spectrum language with concurrency [J].

Colvin, Robert J. ;

Hayes, Ian J. ;

Meinicke, Larissa A. .

FORMAL ASPECTS OF COMPUTING, 2017, 29 (05) :853-875

[6]

Davey BA, 2002, INTRO LATTICES ORDER

[7]

Dijkstra E.W., 1976, A Discipline of Programming

[8]

DIJKSTRA EW, 1975, COMMUN ACM, V18, P453, DOI 10.1145/390016.808417

[9]

Floyd R. W, 1967, Marhematical Aspects of Computer Science, V19, P19

[10]

Hayes I.J., 2021, arXiv, DOI [10.48550/ARXIV.2103.15292, DOI 10.48550/ARXIV.2103.15292]

← 1 2 3 →