Verifying event-driven programs using ramified frame properties
Verifying event-driven programs using ramified frame properties
复制标题
使用分支帧属性验证事件驱动程序
DOI：
10.1145/1708016.1708025
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
Jonathan Aldrich
中科院分区：
文献类型：
--
作者：
N. Krishnaswami;L. Birkedal;Jonathan Aldrich
诸如GUIS或电子表格之类的交互式程序通常在动态创建的对象网络上保持依赖性信息。也就是说，每个命令对象不仅跟踪其自身不变的对象取决于取决于其不变的对象，还可以跟踪所有依赖它的对象，以便在更改时通知它们。
这些双向链接对验证构成了严重的挑战，因为它们的正确性依赖于对象图上的全局不变性。
我们展示了如何使用动态生成的双向依赖性信息进行模块化验证程序。关键的想法是区分命令的足迹和不变的国家取决于足迹。为此，我们定义了更新的特定应用程序语义，并介绍了分支操作员的概念，以解释本地变化如何改变我们对堆的其余部分的了解。我们通过功能性反应性编程的案例研究来说明这种证明风格的适用性，并正式证明对实施极为命令的推理是合理的，就好像是纯粹的。
Interactive programs, such as GUIs or spreadsheets, often maintain dependency information over dynamically-created networks of objects. That is, each imperative object tracks not only the objects its own invariant depends on, but also all of the objects which depend upon it, in order to notify them when it changes.
These bidirectional linkages pose a serious challenge to verification, because their correctness relies upon a global invariant over the object graph.
We show how to modularly verify programs written using dynamically-generated bidirectional dependency information. The critical idea is to distinguish between the footprint of a command, and the state whose invariants depends upon the footprint. To do so, we define an application-specific semantics of updates, and introduce the concept of a ramification operator to explain how local changes can alter our knowledge of the rest of the heap. We illustrate the applicability of this style of proof with a case study from functional reactive programming, and formally justify reasoning about an extremely imperative implementation as if it were pure.