Reasoning algebraically about loops
Reasoning algebraically about loops
复制标题
关于循环的代数推理
DOI：
--
复制
发表时间：
1997
期刊：
影响因子：
0.6
通讯作者：
Joakim von Wright
中科院分区：
文献类型：
--
作者：
R. Back;Joakim von Wright
抽象的。我们展示了如何在改进演算中形式化不同种类的循环构造，以及如何使用此形式化来得出循环构造的一般转换规则。重点是使用代数方法来推理循环结构的等效性和完善性，而不是根据其执行序列操作有关循环的推理方法。我们应用代数推理技术来得出针对行动系统和保护循环的转换规则的集合。其中包括在实际程序推导中发现重要的转换规则：数据的完善和原子性改进；以及通过口吃过渡的循环的合并，重新排序和数据改进。
Abstract. We show how to formalise different kinds of loop constructs within the refinement calculus, and how to use this formalisation to derive general transformation rules for loop constructs. The emphasis is on using algebraic methods for reasoning about equivalence and refinement of loop constructs, rather than operational ways of reasoning about loops in terms of their execution sequences. We apply the algebraic reasoning techniques to derive a collection of transformation rules for action systems and for guarded loops. These include transformation rules that have been found important in practical program derivations: data refinement and atomicity refinement of action systems; and merging, reordering, and data refinement of loops with stuttering transitions.