基于知识的循环不变式生成方法
利用归纳断言方法验证程序正确性的难点是如何找到循环不变式.由程序员直接给出不变式有种种弊端,而现有生成不变式的方法都是根据程序形式,推导出程序变量之间的一些简单的、表面上的关系,却无法找到由数学定理蕴涵着的各个变量之间的深刻关系,因此如何有效的自动生成不变式十分重要.本文主要介绍如何利用程序的输入输出断言以及循环条件,在数学定理的支持下,自动生成循环不变式的方法,用这一方法可以揭示出个变量之间的本质联系.
程序验证 循环不变式 定理证明 归纳断言法 自动生成
王树义 邹伟松 刘恒
大连理工大学计算机科学与工程系
国内会议
大连
中文
38-40
2001-07-01（万方平台首次上网日期，不代表论文的发表时间）