期刊
JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING
卷 79, 期 2, 页码 144-173出版社
ELSEVIER SCIENCE INC
DOI: 10.1016/j.jlap.2009.07.002
关键词
Unifying Theories of Programming; Semantics; Semiring; Kleene algebra; Omega algebra; Fixpoint; Linear recursion
类别
-
We generalise the designs of the Unifying Theories of Programming (UTP) by defining them as matrices over semirings with ideals. This clarifies the algebraic structure of designs and considerably simplifies reasoning about them, for example, since they form a Kleene and omega algebra and a test semiring. We apply our framework to investigate symmetric linear recursion and its relation to tail-recursion. This substantially involves Kleene and omega algebra as well as additional algebraic formulations of determinacy, invariants, domain, pre-image, convergence and Noetherity. Due to the uncovered algebraic structure of UTP designs, all our general results also directly apply to UTP. (C) 2009 Elsevier Inc. All rights reserved.
作者
我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。
推荐
暂无数据