Modal Kleene Algebra and Partial Correctness
| 详细信息 | 推荐本文 | |
- 作者：Bernhard M枚ller ; Georg Struth
- 刊名：Lecture Notes in Computer Science
- 出版时间：2004
- 出版年：2004
- 期刊代码：99_0302-9743
- 类别：cp
- 卷：3116
- 期：1
- 页码：87-90
- 数据来源：sp
摘要
Modal Kleene algebra is Kleene algebra enriched by forward and backward box and diamond operators. We formalize the symmetries of these operators as Galois connections and dualities. We study their properties in the associated semirings of operators. Modal Kleene algebra provides a unifying semantics for various program calculi and enhances efficient cross-theory reasoning in this class, often in a very concise state-free style. This claim is supported by novel algebraic soundness and completeness proofs for Hoare logic.