循环不变形状图的自动推断

作者：**; 陈意云; 张志天

来源：电子技术, 2011, (08): 4-6.

• 形状图逻辑
• 循环不变式
• 程序验证
• 形状分析 shape graph logic
• loop invariant
• program verification
• shape analysis

在指针程序的分析和验证过程中,循环不变式的自动推断一直是个研究热点。文章首先介绍所提出的形状图和形状图逻辑,形状图逻辑是一种把形状图看成有关指针的断言,并在此基础上对Hoare逻辑进行扩展而得到的程序逻辑。然后在此基础之上,设计了一种基于形状图逻辑的形状分析方法,并提出了一种基于形状图逻辑的循环不变形状图的推断方法。

• 出版日期2011
• 单位中国科学技术大学苏州研究院; 中国科学技术大学