近年来,计算机软件系统在日常生活和工作中的地位越来越重要,而计算机软件规模也日渐庞大,其安全问题也因此而受到更多的重视。在一些安全攸关的领域,软件的高可信已经变得十分必要。提高软件可信程度的一个重要方法就是形式程序验证。在典型的形式程序验证过程中,程序员通常需要手工书写函数前后条件以及循环不变式,给程序员带来了极大的不便。同时,循环不变式的自动推断问题又迟迟没有解决。这都是形式程序验证在工业界的应用进展缓慢的原因。研究自动推断循环不变式的方法,不仅对程序验证,而且对程序分析等领域也具有重要的意义。对指针程序而言,数据结构的形状分析给循环不变式的推断乃至程序验证提供很多有用的信息。本文使用一种新的方式来解决指针程序分析验证中的困难及循环不变式的自动推断问题。我们设计了一个形状系统,要求程序员声明各种递归结构类型参与构建的数据结构的形状,并声明指针变量所指向的形状,以换取编译器或其他软件工具检查程序是否有形状错误,帮助排除所构建的形状偏离程序员期望的程序。与此同时,我们还设计了一种基于形状图逻辑的形状分析方法,为程序验证提供指针相关的循环不变形状图和函数前后条件形状图。形状图是表达程序所操作的声明指针和动态分配的结构体中域指针的指向的一种图形,它不仅准确地表达了指针之间的相等关系,还能提供其他有用信息,例如可用来查询访问路径的别名。循环不变形状图是循环不变式中关于指针部分的形状图表示,描述了循环不变式中指针之间的相等关系等信息。形状图逻辑把形状图看作程序中指针信息断言的一种图形表示,并在此基础上对Hoare逻辑进行扩展,可用于对操作易变数据结构的指针程序的分析和验证。基于形状图逻辑,采用先形状分析,后程序验证的方法,我们实现了一个程序验证器。该验证器能够验证本文所定义的各种形状的程序,并且不需要程序员提供有关数据结构形状的函数前后条件和循环不变式,但需要程序员提供非指针型数据的函数前后条件和循环不变式。本文所设计实现的方法在一定程度上解决了循环不变式自动推断的难题,为程序验证减轻了负担。