理论计算机科学电子笔记98(2004)3-4www.elsevier.com/locate/entcs操作指针的程序(特邀演讲)安德斯·默勒1丹麦奥胡斯大学,金砖国家摘要这个演讲概述了各种验证使用指针操作数据结构的程序正确性的方法。保留字: 分离逻辑,参数形状分析,指针断言逻辑讲座大纲关于使用指针操作数据结构的程序的正确性的推理是众所周知的困难:通过指针的破坏性更新可以产生复杂的结构,堆具有无限的大小,并且数据结构不变量通常仅在操作的开始和结束时保持正确性属性包括一般要求,例如不存在空指针解引用、悬空指针和泄漏内存,但也包括更专门的要求,例如过程的部分正确性。这个演讲将描述三种验证程序操作指针的方法。首先,我们研究Reynolds,O'Hearn和其他人[ 2 ]的分离逻辑这是霍尔逻辑的扩展,引入了一个“分离合取”运算符,断言其子公式对堆的不相交部分成立。然后,我们考虑Sagiv、Reps和Wilhelm [3]的参数形状分析此方法基于数据流1电子邮件:amoeller@brics.dk1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi:10.1016/j.entcs.2003.10.002凌晨4Møller / Electronic Notes in Theoretical Computer Science 98(2004)3-4分析和三值逻辑。堆被建模为一个逻辑结构,属性用具有传递闭包的一阶逻辑表示最后,我们描述了Møller和Schwartzbach [1]的指针断言逻辑基于有限树上一元二阶逻辑的可判定性结果,该技术使用“图形类型”对堆结构进行建模,这些方法都有一个共同的目标,即对程序中使用指针时出现的复杂的有限状态系统进行建模;然而,它们具有不同的适用范围,不同的自动化程度和不同的可伸缩性。幻灯片可在http://www.brics.dk/~amoeller/talks/infinity.pdf上获得。引用[1] Møller,A.和M.I. Schwartzbach,指针断言逻辑引擎,在:Proc. ACM SIGPLAN编程语言设计与实现会议,PLDI '01,2001,pp。 221- 231[2] 雷诺兹,J.C.,Separation logic:A logic for shared mutable data structures,in:Proc. 17thAnnual IEEE Symposium on Logic in Computer Science,LICS55比74[3] Sagiv,S.,T. W.代表和R。Wilhelm,Parameter shape analysis via 3-valued logic,ACM Transactions on Programming Languages and Systems24(2002),pp.217-298.