Blaming the client: on data refinement in the presence of pointers
Blaming the client: on data refinement in the presence of pointers
复制标题
归咎于客户端：在存在指针的情况下对数据进行细化
DOI：
10.1007/s00165-009-0125-8
复制
发表时间：
2010
影响因子：
1
通讯作者：
Filipovic I
中科院分区：
文献类型：
--
作者：
Filipovic I
数据细化是推理程序的常用方法，其基础是确定具体程序确实满足预期抽象模式所强加的所有必需属性。当假设使用指针时，在这种设置中关于程序的推理变得复杂，此外，用于证明数据细化的众所周知的方法，即前向模拟方法，在指针存在时变得不可靠。不健全的原因是模拟的“提升定理”失败：抽象模块和具体模块之间的模拟可以提升到所有客户端程序。结果是，模拟并不意味着具体的模块可以在所有情况下取代抽象模块。我们对这个问题的诊断是，不健全是由于客户端程序的干扰造成的。我们的分析不是将提升模拟的不健全性归咎于模块，而是将责任归咎于引起干扰的客户端程序：当不存在干扰时，健全性就会恢复。从技术上讲，我们提出了一种新颖的仪器化语义，能够检测模块与其客户端之间的干扰。通过使用特殊的模拟关系，即增长关系，并使用仪器化语义解释模拟方法，我们得到了提升定理。然后我们展示在哪些情况下模拟确实意味着改进。
Data refinement is a common approach to reasoning about programs, based on establishing that a concrete program indeed satisfies all the required properties imposed by an intended abstract pattern. Reasoning about programs in this setting becomes complex when use of pointers is assumed and, moreover, a well-known method for proving data refinement, namely the forward simulation method, becomes unsound in presence of pointers. The reason for unsoundness is the failure of the “lifting theorem” for simulations: that a simulation between abstract and concrete modules can be lifted to all client programs. The result is that simulation does not imply that a concrete can replace an abstract module in all contexts. Our diagnosis of this problem is that unsoundness is due to interference from the client programs. Rather than blame a module for the unsoundness of lifting simulations, our analysis places the blame on the client programs which cause the interference: when interference is not present, soundness is recovered. Technically, we present a novel instrumented semantics which is capable of detecting interference between a module and its client. With use of special simulation relations, namely growing relations, and interpreting the simulation method using the instrumented semantics, we obtain a lifting theorem. We then show situations under which simulation does indeed imply refinement.
登录
查看更多内容
谓词转换器的数据细化
影响因子：
1.1
作者：
Paul H. B. Gardiner;Carroll Morgan
通讯作者：
Carroll Morgan
DOI：
10.1145/964001.964024
发表时间：
2004-01
期刊：
Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages
影响因子：
--
作者：
P. O'Hearn;Hongseok Yang;J. C. Reynolds
通讯作者：
P. O'Hearn;Hongseok Yang;J. C. Reynolds
细化和分离上下文
DOI：
10.1007/978-3-540-30538-5_35
发表时间：
2004
期刊：
ArXiv
影响因子：
--
作者：
Ivana Mijajlovic;Noah Torp;P. O'Hearn
通讯作者：
P. O'Hearn
基于状态的所有权、重入和封装
影响因子：
--
作者：
A. Banerjee;D. Naumann
通讯作者：
D. Naumann
通用命令 - 部分正确形式主义的工具
DOI：
10.1093/comjnl/20.2.151
发表时间：
1977
期刊：
Comput. J.
影响因子：
--
作者：
J. Schwarz
通讯作者：
J. Schwarz