Expression Decomposition in a Rely/Guarantee Context
Expression Decomposition in a Rely/Guarantee Context
复制标题
依赖/保证上下文中的表达式分解
DOI：
--
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
Joey W. Coleman
中科院分区：
文献类型：
--
作者：
Joey W. Coleman
本文介绍了一种技术的表达式分解，它允许使用依赖/保证开发规则，不承担原子表达式评估。这种分解提供了一种方法来解决这样一个事实，即相对于单个状态的表达式的逻辑含义和细粒度并发语言中的表达式的语义评估不提供相同的结果;特别是，前者导致单个值，而后者可以导致许多可能的值。依赖/保证开发规则倾向于依赖于使用表达式的情况下表达式的逻辑含义;表达式分解确定在哪里这样做是安全的，并为不安全的地方提供一些工具。
This paper describes a technique of expression decomposition which allows the use of rely/guarantee development rules that do not assume atomic expression evaluation. This decomposition provides a means of addressing the fact that the logical meaning of expressions relative to a single state and the semantic evaluation of expressions in a fine-grained concurrent language do not provide the same results; in particular, the former results in a single value whereas the latter can result in many possible values. Rely/guarantee development rules tend to depend on the logical meaning of expressions in cases where they are used; expression decomposition identifies where it is safe to do so, and provides some tools for where it is not.
信赖/担保规则健全性的结构证明
影响因子：
0.7
作者：
Coleman J
通讯作者：
Coleman J