A Structural Proof of the Soundness of Rely/guarantee Rules
A Structural Proof of the Soundness of Rely/guarantee Rules
复制标题
信赖/担保规则健全性的结构证明
DOI：
10.1093/logcom/exm030
复制
发表时间：
2007
影响因子：
0.7
通讯作者：
Coleman J
中科院分区：
文献类型：
--
作者：
Coleman J
各种形式的依赖/保证条件已被用来记录和推理干扰的方式，提供组合开发方法的并发程序。本文阐述了这一套规则，并证明了它们的合理性。底层并发语言允许细粒度的交错和嵌套并发;它由操作语义定义;依赖/保证规则与该语义（包括终止）一致的证明是由结构归纳。一个关键引理，它将由于程序的一部分脱离上下文而产生的额外干扰所引起的状态联系起来，使得不必对计算历史进行归纳就可以进行证明。这个引理还提供了一种思考依赖/保证条件下辅助变量的可表达性问题的方法。
Various forms of rely/guarantee conditions have been used to record and reason about interference in ways that provide compositional development methods for concurrent programs. This article illustrates such a set of rules and proves their soundness. The underlying concurrent language allows fine-grained interleaving and nested concurrency; it is defined by an operational semantics; the proof that the rely/guarantee rules are consistent with that semantics (including termination) is by a structural induction. A key lemma which relates the states which can arise from the extra interference that results from taking a portion of the program out of context makes it possible to do the proofs without having to perform induction over the computation history. This lemma also offers a way to think about expressibility issues around auxiliary variables in rely/guarantee conditions.
登录
查看更多内容
安全地分裂原子
影响因子：
1.1
作者：
Cliff B. Jones
通讯作者：
Cliff B. Jones
DOI：
--
发表时间：
2007
期刊：
Formal Methods and Hybrid Real-Time Systems
影响因子：
--
作者：
Cliff B. Jones;I. Hayes;M. A. Jackson
通讯作者：
M. A. Jackson
根据控制系统的环境规格确定控制系统的规格
DOI：
--
发表时间：
2003
期刊：
FME
影响因子：
--
作者：
I. Hayes;M. Jackson;Cliff B. Jones
通讯作者：
Cliff B. Jones
关于PL/I的形式化描述
DOI：
--
发表时间：
1969
期刊：
影响因子：
--
作者：
P. Lucas;K. Walk
通讯作者：
K. Walk
VDM 中的程序规范和验证
DOI：
--
发表时间：
1987
期刊：
影响因子：
--
作者：
Cliff B. Jones
通讯作者：
Cliff B. Jones