摘要
在指针程序的分析和验证过程中,循环不变式的自动推断一直是个研究热点。文章首先介绍所提出的形状图和形状图逻辑,形状图逻辑是一种把形状图看成有关指针的断言,并在此基础上对Hoare逻辑进行扩展而得到的程序逻辑。然后在此基础之上,设计了一种基于形状图逻辑的形状分析方法,并提出了一种基于形状图逻辑的循环不变形状图的推断方法。
Automatic inference of Loop-Invariant has been a hot research topic in the field of analysis and verification of pointer programs.In this paper,we first describe the proposed shape graph and shape graph logic,the shape graph logic is an extension to Hoare logic by regarding shape graphs as assertions about pointers directly.Then based on the shape graph logic,we design a method for shape analysis on pointer programs and after that we put forward a method for inferring loop invariant shape graphs associated with pointers.
出处
《电子技术（上海）》
2011年第8期4-6,共3页
Electronic Technology
关键词
形状图逻辑
循环不变式
程序验证
形状分析
shape graph logic
loop invariant
program verification
shape analysis
