Separation and information hiding
Separation and information hiding
复制标题
DOI：
10.1145/964001.964024
复制
发表时间：
2004-01
期刊：
影响因子：
--
通讯作者：
P. O'Hearn;Hongseok Yang;J. C. Reynolds
中科院分区：
文献类型：
--
作者：
P. O'Hearn;Hongseok Yang;J. C. Reynolds
我们利用分离逻辑的最新形式体系来研究信息隐藏的证明规则。从本质上讲，我们使用分离合取来将模块的内部资源与模块的客户端所访问的资源区分开来。逻辑连接词的使用产生了一种动态划分形式，借此我们可以追踪堆存储部分的所有权在程序组件之间的转移。它还使我们能够在存在可能有别名的嵌入地址的可变数据结构的情况下强制实施分离。
We investigate proof rules for information hiding, using the recent formalism of separation logic. In essence, we use the separating conjunction to partition the internal resources of a module from those accessed by the module's clients. The use of a logical connective gives rise to a form of dynamic partitioning, where we track the transfer of ownership of portions of heap storage between program components. It also enables us to enforce separation in the presence of mutable data structures with embedded addresses that may be aliased.