CAJ | 학술논문

利用形状图逻辑和形状系统来解决指针程序的分析和验证中的困难。该方法要求程序员声明各种递归结构体类型参与构建的数据结构的形状，并声明指针变量所指向的形状，以便程序分析工具能建立各程序点的形状图，并以此来支持程序验证。探讨了在指针相等关系静态可确定的情况下，避免在Hoare逻辑上做复杂扩展的指针程序验证方法。
이용형상도라집화형상계통래해결지침정서적분석화험증중적곤난。해방법요구정서원성명각충체귀결구체류형삼여구건적수거결구적형상，병성명지침변량소지향적형상，이편정서분석공구능건립각정서점적형상도，병이차래지지정서험증。탐토료재지침상등관계정태가학정적정황하，피면재Hoare라집상주복잡확전적지침정서험증방법。
Analysis and verification of programs dealing with pointers are still difficult problems so far. This paper uses a shape graph logic and a shape system to solve these problems. Using our method, programmers must declare the shapes that the recursive data structuresintend to build, and the shapes that pointer variables point to. Thus shape graphs can be constructed using an analysis tool and used tosupport the program verification. This paper presents a method for pointer program verification avoiding to make complicated extensions to Hoare logic in the situation that equalities over pointers can be decided statically.