随着计算机科学与技术的迅速发展,软件的规模越来越大,软件的可靠性越来越难以保障,如何保障软件的正确性是计算机科学的一个巨大的挑战。程序验证是保障软件正确性、提高软件可信度的可靠方法,其中定理证明这一方法利用逻辑和数学手段,通过演绎推理来验证软件的正确性,这种方法可以极大地提高人们对软件的信心,是近年来的研究热点。定理证明的基本思想是通过某种断言描述程序的形式规约,根据断言对程序进行逻辑演算生成验证条件,借助定理证明工具证明验证条件的正确性,从而证明程序的正确性,保障软件的可信性。但是,提供合适的规约要求验证人员对程序有深刻的理解,对于验证人员来说是一件非常困难的事情,因此,自动生成程序规约是程序验证领域中的重要研究内容,其中关于循环语句以及类库的研究是重中之重。循环语句广泛存在于各类程序中,循环语句的规约在程序验证领域中具有不可替代的作用,循环语句规约的自动生成与验证中的难点主要在于循环不变式的自动生成与检验,然而循环语句复杂多样,不存在统一的方法可以为所有的循环自动生成规约。现在的软件程序大量依赖于类库,类库的行为已经成为软件行为中不可分割的一部分,类库的规约在很多程序分析验证技术中扮演着不可或缺的重要角色,是很多程序分析过程的前提条件。然而类库的源代码通常规模庞大、逻辑复杂,有时甚至根本无法获取,因此,生成类库的规约异常困难。本文针对规约的自动生成与验证问题展开研究,主要工作包括以下几个方面：1.提出了一种综合考虑程序代码和程序规约来构造循环不变式的方法,即基于循环语句已有的断言生成循环不变式。首先通过将循环语句的后置条件以及循环体的断言通过子表达式替换、添加全称量词和寻找递推关系的方式来生成候选的循环不变式,然后对每一个候选的循环不变式,借助定理证明器和最弱前置条件的计算来证明候选循环不变式的正确性以及相关断言的正确性。本文提出的方法所生成的循环不变式既可以描述数据结构的形状性质,也可以描述数据结构所存储的元素之间的关系以及元素与标量变量、常量之间的关系。该方法已经实现并集成到程序验证工具中,实验数据表明,本文提出的方法可以有效地为操作常用数据结构的循环自动生成循环不变式,提高程序验证的自动化程度和效率,减轻验证人员的负担。2.定义了一种描述程序语句摘要的方法,将摘要定义为语句修改的内存以及语句执行结束以后这些内存中存放的新值。基于循环语句的摘要,循环语句可以被转换为一系列抽象的赋值语句,从而可以将带有循环语句的程序转换为不包含循环的程序,从而可以使用分析赋值语句的方法来分析循环语句。提出了自动生成程序语句的摘要的方法,可以有效地为赋值语句、顺序语句、条件语句以及操作常用数据结构的循环语句自动生成摘要,其中循环语句可以嵌套多层循环和分支结构。同时提出了一种根据语句的摘要自动生成程序语句的规约的方法,生成的规约类型包括后置条件、前置条件以及循环不变式。该方法已经实现并集成到程序验证工具中,生成语句摘要的方法所需要的时间和循环的个数成线性关系,相比于以往借助于抽象解释等对循环语句进行分析的方法,我们的方法效率更高。根据摘要所生成的规约可以有效地辅助程序的形式化验证过程,既可以减轻程序验证人员人工提供程序规约的负担同时又可以提高验证程序的效率。3.提出了一种基于文档自动生成类库的代码模型的方法,该方法综合使用了自然语言处理技术和自动化测试技术。所生成的模型模拟了类库的行为,但是模型的代码实现更加简单,从而解决了因为类库源代码缺失导致无法分析的问题以及分析复杂的类库源代码非常困难的问题。有了类库的代码模型,就可以通过对模型进行分析来生成类库的规约,用于证明程序的正确性。开发完成的工具原型可以为Java类库中14个常用类和2个常用接口的326个库函数自动生成代码模型,并将生成的代码模型应用于类库的规约生成、Android污点分析和Java动态切片中。在类库的规约生成中,通过对代码模型的分析可以自动生成类库函数的外部规约,通过对外部规约进行实例化可以生成调用类库函数的程序的规约。在Android污点分析中,使用代码模型可以发现一些使用类库源代码无法发现的信息泄露路径,而且使用代码模型进行分析时,效率上也有所提升。在Java动态切片中,使用代码模型比使用朴素模型所生成的切片更精确而且效率更高。总体结果表明我们的方法可以准确地为类库的行为进行建模,有效地为类库的函数生成规约,并且提高其它程序分析技术的有效性和效率。