Analysis of pointer programs has already become a hotspot research in the field of programming languages. This paper takes an approach to the problem by doing shape analysis, which uses a shape graph to express points-to and equivalence relations among pointers in a program, and uses a shape graph logic to infer programs. The shape graph logic is an extension to Hoare logic by regarding shape graphs as assertions about pointers directly. First, this paper describes the proposed shape graph and shape graph logic. Then based on the shape graph logic, it designs a method for shape analysis on pointer programs.%指针程序的分析一直是研究热点.本文提出一种基于形状图逻辑的形状分析方法,其中形状分析采用形状图来表达程序中指针的指向和相等关系,并用形状图逻辑来进行推理.形状图逻辑是一种把形状图看成有关指针的断言,并在此基础上对Hoare逻辑进行扩展而得到的程序逻辑.首先介绍所提出的形状图和形状图逻辑；然后在此基础之上,设计一种基于形状图逻辑的形状分析方法.
展开▼
