软件开发过程需要保证程序满足正确性规约。目前主要有软件测试、模型检验等技术用于程序的正确性保证。软件测试通过测试用例集来描述正确性规约,在测试用例集上执行目标程序以判断结果是否符合预期；模型检验通过自动机、Petri Net等对软件系统进行建模,判断软件系统运行过程是否会出错。但是测试方法只能保证程序在一定覆盖度下满足规约,无法证明程序正确,而模型检验方法使用分析程序状态来判断是否会有不安全的错误情况,存在状态空间爆炸的问题。它们不适合针对计算处理过程的程序验证。为了准确地验证和数据处理计算相关程序性质,相关研究者提出了使用逻辑推理系统如Hoare Logic对程序进行静态验证的方法：分析人员用包含自定义递归函数的逻辑公式描述程序程序的状态,并使用逻辑系统的推理规则分析程序状态在语句执行前后的变化。分析人员还可以使用约束求解器等工具辅助推导更多的性质。研究人员对Hoare Logic进行扩展得到Separation Logic和Scope Logic,更是使得逻辑系统具有了处理指针别名的能力。然而基于逻辑系统人工推导性质的过程十分复杂,涉及多种推理规则的结合使用。尤其是当处理循环语句和递归数据结构时,人工分析更是容易发生错漏,所以该方法对分析人员的经验和能力有较为苛刻的要求。为了使得基于逻辑系统的程序验证过程更加准确和高效,本文提出了如下的方法：·提出了一种在Scope Logic上进行交互式的程序验证的方法。多种分析技术之间通过程序点的逻辑公式进行协作。分析人员可以与分析过程进行交互,手工进行程序性质的验证,也可以自行指定多种分析技术结合进行程序性质的分析。分析技术只要满足相关约束,即可参与交互程序验证的过程。交互式的程序验证可以保证灵活性,可以提高程序验证的自动化程度。·提出了使用数据流分析结合Scope Logic对程序性质进行自动分析的方法。分析人员将递归函数公式描述的程序性质取值转化为交半格表示的数据流值,并为数据流值设置随着程序语句传播的过程。数据流算法便可自动化求解最终的程序状态。分析过程自动将结果转成公式,并且自动设置公式的来源和依赖关系。当数据流分析过程满足相关约束时,该数据流分析过程就可以作为一种自动化技术参与交互式程序验证。分析人员保证数据流值半格高度有穷和传播过程的单调,即可保证数据流迭代算法收敛。通过使用该方法进行自动化验证,程序验证的效率得到提高。我们将以上数据流分析的方法在基于Scope Logic的程序分析工具Accumu-lator上集成实现,分析人员可与工具交互,使用不同分析过程验证程序性质。我们使用该工具分析了一系列递归数据结构操作实例,主要包括单链表形状变化的代码,如单链表的插入、删除和翻转等。实验对正确和错误的代码都进行了分析,实验结果表明,分析人员使用我们的方法得到的结果满足Scope Logic的规约,可以有效地与其他技术进行交互,因而可以准确地验证程序性质。