Developments in concurrent Kleene algebra

作者：Hoare, Tony; van Staden, Stephan; Moeller, Bernhard; Struth, Georg; Zhu, Huibiao^*

来源：Journal of Logical and Algebraic Methods in Programming, 2016, 85(4): 617-636.

DOI：10.1016/j.jlamp.2015.09.012

• Concurrent Kleene algebra
• Laws of programming
• Trace algebra
• Semantic models
• Refinement
• Unifying theories

This report summarises the background and recent progress in the research of its coauthors. It is aimed at the construction of links between algebraic presentations of the principles of programming and the exploitation of concurrency in modern programming practice. The signature and laws of a Concurrent Kleene Algebra (CKA) largely overlap with those of a Regular Algebra, with the addition of concurrent composition and a few simple laws for it. They are re-interpreted here in application to computer programs. The inclusion relation for regular expressions is re-interpreted as a refinement ordering, which supports a stepwise contractual approach to software system design and to program debugging. The laws are supported by a hierarchy of models, applicable and adaptable to a range of different purposes and to a range of different programming languages. The algebra is presented in three tiers. The bottom tier defines traces of program execution, represented as sets of events that have occurred in a particular run of a program; the middle tier defines a program as the set of traces of all its possible behaviours. The top tier introduces additional incomputable operators, which are useful for describing the desired or undesired properties of computer program behaviour. The final sections outline directions in which further research is needed.

• 出版日期2016-6
• 单位华东师范大学