Relational Decomposition
Relational Decomposition
复制标题
关系分解
DOI：
10.1007/978-3-642-22863-6_6
复制
发表时间：
2011
影响因子：
--
通讯作者：
Lennart Beringer
中科院分区：
文献类型：
--
作者：
Lennart Beringer
我们介绍了关系分解，这是一种将正式减少终止不敏感的关系程序逻辑的技术，即一项执行属性的程序逻辑。概括了自我键合的方法，我们开发了沿着短语结构分解的插值的概念，并将这些插值与一般和关系谓词变压器联系起来。与以前的形式主义相反，关系分解适用于异质对的过渡系统。我们应用方法来证明本顿关系hoare逻辑（RHL）的一种具有对象的语言的变体，并提出了将循环无法锁定的循环的新颖规则。我们还概述了应用程序的非干扰和分离逻辑。
We introduce relational decomposition, a technique for formally reducing termination-insensitive relational program logics to unary logics, that is program logics for one-execution properties. Generalizing the approach of selfcomposition, we develop a notion of interpolants that decompose along the phrase structure, and relate these interpolants to unary and relational predicate transformers. In contrast to previous formalisms, relational decomposition is applicable across heterogeneous pairs of transition systems. We apply our approach to justify variants of Benton's Relational Hoare Logic (RHL) for a language with objects, and present novel rules for relating loops that fail to proceed in lockstep. We also outline applications to noninterference and separation logic.
DOI：
10.1145/1111037.1111045
发表时间：
2006-01
期刊：
--
影响因子：
--
作者：
Sebastian Hunt;David Sands
通讯作者：
Sebastian Hunt;David Sands