链接数据结构中可达模式的逻辑
摘要：通过指针和破坏性指针更新操作来操作动态分配对象的程序的不变量表达和检查的一个新的可判定逻辑被定义。这个逻辑的主要特点是能够通过正则表达式从指定节点可达的节点的邻域进行限制。该逻辑在布尔运算（蕴含、否定）下是封闭的，并且具有有限模型属性。关键技术结果是可判定性的证明。我们展示了如何为一些有趣的程序表达前置条件、后置条件和循环不变量。还可以表达数据结构的不交性和底层堆变化的属性。此外，我们的逻辑可以表达任意数据结构和任意数量的指针字段的属性。后者提供了一种自然地指定入口过程的字段与退出时字段之间的后置条件的方式。因此，可以使用这个逻辑自动证明执行底层堆变化的程序的部分正确性。
作者：Greta Yorsh, Alexander Rabinovich, Mooly Sagiv, Antoine Meyer (LIAFA), Ahmed Bouajjani (LIAFA)
论文ID：0705.3610
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-06-13