AI 中文总结
研究依赖/保证并发中并行组合的分配律，在抽象同步原子代数中开发分配律并应用于支持相关命令的代数实例，设计出更强等式定律且已在Isabelle/HOL中形式化并证明相关引理。
AI 中文摘要
依赖/保证方法支持并发程序的逐步开发。我们的目标是开发一种理论，以依赖/保证风格对并发程序进行代数推理，其中依赖和保证条件在我们的理论中编码为命令。对于数学而言，分配律对于并发程序的代数操作至关重要。本文研究并行组合的分配律，并展示其如何应用于依赖/保证并发。最一般的分配律只是单向细化，然而，通过限制被分配命令的形式，可以设计出更强的等式定律，适用于保证命令以及依赖和保证命令的适当组合。我们的方法是在更抽象的同步原子代数中开发分配律，然后将其应用于支持依赖和保证命令的该代数实例。该理论已在Isabelle/HOL中形式化，并给出了此处引理的证明。
英文摘要
The rely/guarantee approach supports the stepwise development of concurrent programs. Our goal is to develop a theory for reasoning algebraically about concurrent programs in a rely/guarantee style, where rely and guarantee conditions are encoding as commands within our theory. As for mathematics, distributive laws are essential for algebraic manipulation of concurrent programs. In this paper we investigate distributive laws for parallel composition and show how these can be applied to rely/guarantee concurrency. The most general distributive laws are only refinements in a single direction, however, by restricting the form of the command being distributed, one can devise stronger equality laws, which are applicable to guarantee commands as well as to suitable combinations of rely and guarantee commands. Our approach is to develop the distributive laws in a more abstract synchronous atomic algebra, and then apply them to an instance of that algebra supporting rely and guarantee commands. The theory has been formalised in Isabelle/HOL along with proofs of the lemmas presented here.
Comments26 pages
