程序正确性证明ppt课件.ppt

程序正确性证明 主要内容 程序正确性简介程序测试程序正确性证明 内容线索 程序正确性简介程序测试程序正确性证明 程序的正确性 所谓一段程序是正确的 是指这段程序能准确无误地完成编写者所期望赋予它的功能 或者说 对任何一组允许的输入信息 程序执行后能得到一组和这组输入信息相对应的正确的输出信息 通俗地说 做了它该做的事 没有做它不该做的事 程序正确性的严格定义分为三种类型部分正确性终止性完全正确性 如何保证程序的正确性 要求1 从编程时就应该尽量地避免和减少错误的发生2 当程序编好后要尽量找出错误 纠正错误避免错误的方法1 程序的结构要简单2 采用标准的软件设计工具 标准的算法手册以及有效的程序设计方法发现错误的方法1 利用测试工具2 利用程序的验证系统 内容线索 程序正确性简介程序测试程序正确性证明 程序测试 测试是程序的执行过程 目的在于发现错误 一个好的测试用例在于能发现至今未发现的错误 一个成功的测试是发现了至今未发现的错误的测试 测试的原则1 应当 尽早地和不断地进行软件测试 2 测试用例应由测试输入数据和对应的预期输出结果组成 3 程序员应避免检查自己的程序 4 在设计测试用例时 应当包括合理的输入条件和不合理的输入条件 5 充分注意测试中的群集现象 即测试后程序中残存的错误数目与该程序中已发现的错误数目成正比 6 严格执行测试计划 排除测试的随意性 7 应当对每一个测试结果做全面检查 8 妥善保存测试计划 测试用例 出错统计和最终分析报告 为维护提供方便 内容线索 程序正确性简介程序测试程序正确性证明简介Floyd不变式断言法Hoare规则公理方法Dijkstra最弱前置条件方法 正确性证明 测试只能发现程序错误 但不能证明程序无错 即所谓 挂一漏万 原因 测试并没有也不可能包含所有数据 只是选择了一些具有代表性的数据 所以它具有局限性 正确性证明是通过数学技术来确定软件是否正确 也就是说 是否符合其规格说明 正确性证明的发展 正确性证明的方法 为了证明一个程序的完全正确性 通常采用的方法是分别证明该程序的部分正确性和终止性 主要方法有 关于部分正确性证明的方法Floyd的不变式断言法 Manna的子目标断言法Hoare的公理化方法 关于终止性证明的方法Floyd的良序集方法 Manna等人的不动点方法Knuth的计数器方法关于完全正确性证明的方法Hoare的公理化方法的推广 Manna Pnueli Burstall的间发断言方法Dijkstra最弱前置谓词变换方法以及强验证方法 预备知识 前置 输入 断言 输入应满足的条件后置 输出 断言 输入出应满足的条件程序规范 程序的前置断言和程序的后置断言组成程序的状态 程序执行到某一时刻 程序中所有变量的一组取值初始状态 所有变量的取值使程序的前置断言为真的状态终止状态 所有变量的取值使程序的后置断言为真的状态程序的执行可以看作是程序状态的变迁 预备知识 1 完全正确性断言 程序S的执行开始于满足P的状态 则该执行必定能在有限的时间内终止 且终止的状态满足Q 则称完全正确性断言 记为 P S Q 2 部分正确性断言 程序S的执行开始于满足P的状态 若此执行能在有限的时间内终止 则终止时的状态满足Q 则称部分正确性断言 记为 P S Q 程序正确性概念定义1 如果对于每一个使得P 为真的输入 程序S计算都终止 称程序S对P是终止的 定义2 对于满足P 为真 且能够使程序S计算终止的每个 如果Q P 为真 则称程序S对于P和Q是部分正确的 记为 P S Q 定义3 对于满足P 为真的每个 如果程序S能够计算终止 且Q P 为真 则称程序S对于P和Q是完全正确的 记为 P S Q 不变式断言法 R W Floyd 1967年提出证明一个程序的部分正确性步骤 1 建立断言输入断言 x 前提条件 初始状态输出断言 x z 最终结论 终止状态满足的条件循环不变式 在每次循环的前后均为真的谓词 2 建立检验条件检验条件 程序运行通过该通路时应满足的条件 3 证明检验条件适合对象 程序流程图 i x y Ri x y i x ri x y 输入断言 输出断言 y 一组中间变量x 输入变量x y 蕴含符 即 ri x y 通过该通路后y的值 通过此路径的条件 实例 设x1 x2是正整数 求它们的最大公约数z gcd x1 x2 我们知道 对于任意正整数y1 y2 有下列关系 1 若y1 y2 gcd y1 y2 gcd y1 y2 y2 2 若y2 y1 gcd y1 y2 gcd y1 y2 y1 1 若y1 y2 gcd y1 y2 y1 y2 开始 x1 x2 y1 y2 y1 y2 y1 y2 y1 y2 y1 y2 y1 y2 A x B P x y y1 z G 结束 C x z D E T F F T 证明 1 建立断言 x x1 0 x2 0 x z z gcd x1 x2 P x y x1 0 x2 0 y1 0 y2 0 gcd y1 y2 gcd x1 x2 2 建立检验条件通路1 A B 通路2 B D B通路3 B E B 通路4 B G C为每一条通过 建立检验条件通路1 A B无条件 R1 x y 恒真 结果y取值为x 检验条件为 x P x y 即 x1 0 x2 0 x1 0 x2 0 y1 0 y2 0 gcd x1 x2 gcd x1 x2 证明 通路2 B D BR2 x y y1 y2 y1 y2 r2 x y y1 y2 y2 P x y 输入输出均为P x y 检验条件为 P x y y1 y2 y1 y2 P x y1 y2 y2 将断言P x y 代入 即得 x1 0 x2 0 y1 0 y2 0 gcd y1 y2 gcd x1 x2 y1 y2 y1 y2 x1 0 x2 0 y1 y2 0 y2 0 gcd y1 y2 y2 gcd x1 x2 通路3 B E B类似地 得到 P x y y1 y2 y1 y2 P x y1 y2 y1 通路4 B G C类似地 得到 P x y y1 y2 x z 证明 3 证明检验条件通路1 x1 0 x2 0 x1 0 x2 0 gcd x1 x2 gcd x1 x2 显然通路2 x1 0 x2 0 y1 0 y2 0 gcd y1 y2 gcd x1 x2 y1 y2 y1 y2 x1 0 x2 0 y1 y2 0 y2 0 gcd y1 y2 y2 gcd x1 x2 检验条件前项成立时 y1 y2为真 而y1 y2 0为真且gcd y1 y2 y2 gcd y1 y2 gcd x1 x2 检验条件为真通路3 P x y y1 y2 y1 y2 P x y1 y2 y2 y1 y1 y2为真 y1 y2 0为真 gcd y1 y2 y1 gcd y1 y2 gcd x1 x2 检验条件为真通路4 P x y y1 y2 x z y1 y2 gcd y1 y2 y1 y2 检验条件为真 同步练习 开始 0 0 1 y1 y2 y3 y2 x y1 1 y3 2 y1 y3 A x B P x y y1 z 结束 C x z D T F y2 y3 y2 B 内容线索 程序正确性简介程序测试程序正确性证明简介Floyd不变式断言法Hoare规则公理方法Dijkstra最弱前置条件方法 程序正确性验证 Hoare公理学方法 1990年IEEE计算机先驱奖1980年图灵奖英国牛津大学计算机科学家查尔斯 霍尔 CharlesAntonyRichardHoare 发明Quicksort算法 CASE语句1963年实现了Algol语言1969年1月 在Comm OfACM上发表 AnAxiomaticbasisforComputerProgramming 提出公理语义学操作系统的MonitorACM在1983年评出在近25年在CACM上发表的25篇里程碑式的论文25篇 2人2篇 Hoare是其一 Hoare公理学方法 在Floyd的归纳法断言基础上 C A R Hoare于1969年发表了 计算机程序设计的公理基础 一文 提出了另一种程序验证的方法 他的成功在于使用了简洁的符号和提出了定义程序语义的公理系统 Hoare公理系统和Hoare逻辑是十多年来引人注目的重要工作 Hoare系统是一个关于形如 P S Q 的断言的逻辑系统 P S Q 是为了区别于完全正确的 P S Q 断言的部分正确性断言的表示方法 这是方法是针对WHILE型程序提出的 Hoare公理学方法 部分正确性证明 1 WHILE型程序WHILE型程序是由一个有限的语句序列组成 每个语句之间的分号隔开 即 B0 B1 Bn其中 B0是程序中唯一的开始语句 STARTy f x Bi 1 i n 是下列语句之一 程序正确性验证 Hoare公理学方法 1 赋值语句 y g x y 2 条件语句 ifRthenF1elseF2或ifRthenF13 复合 BeginF1 F2 FnEnd4 循环语句 whileRdoF15 停机语句 Z h x y HALT其中 语句R是逻辑表达式 F1 F2 Fn是上列语句中的任何一种 程序正确性验证 Hoare公理学方法 例如 计算Z sqrt x 的程序 START y1 y2 y3 0 1 1 While y2 x do y1 y2 y3 y1 1 y2 y3 2 y3 2 Z y1 HALT 程序正确性验证 Hoare公理学方法 2 不变式演绎系统 Hoare系统1 基本概念 1 不变式语句 P F Q 其中 P Q是逻辑表达式 F是一个程序段 它的含义是 如果执行F以前P成立 且执行终止 则执行F后Q成立 这时不变式语句为真 有时也称为归纳表达式 程序正确性验证 Hoare公理学方法 1 基本概念 2 推理规则A1 A2 AnB其中 B是一个不变式语句 Ai i 1 2 n 是一个逻辑表达式或者是其它的不变式语句 它的含义 为了推导后项为真 只需证明前项A1 A2 An为真 2 不变式演绎系统 Hoare系统 程序正确性验证 Hoare公理学方法 2 不变式演绎系统 Hoare系统1 基本概念 3 定理 采用上述记号 一个程序F关于其输入断言P x 和输出断言Q x z 的部分正确性可以表示为 P x F Q x z 因而 证明程序F的部分正确性 就可以归结为证明这一归纳表达式为真 程序正确性验证 Hoare公理学方法 2 Hoare系统的公理及其推理规则 1 赋值公理 P x g x y y g x y P x y 2 条件规则 P R F1 Q P R F2 Q P ifRthenF1elseF2 Q 或者 P R F1 Q P R Q P ifRthenF1 Q 3 While规则P I I R F I I R Q P whileRdoF Q 程序正确性验证 Hoare公理学方法 2 Hoare系统的公理及其推理规则 4 并置规则 P F1 P1 P1 F2 Q P F1 F2 Q 5 结论规则P R R F Q P F Q 或者 P F R R Q P F Q 注 程序设计总是和具体的应用领域相关 程序F是针对某一具体的论域的 g x y 和R是论域中的项或谓词 另外P Q R I也是论域上的谓词公式 因此 上述公理和推理规则可以看作是对论域理论的扩充 程序正确性验证 Hoare公理学方法 3 派生规则 1 赋值规则P x y Q x g x y P x y y g x y Q x y 2 重复赋值规则P x y Q x gn x gn 1 x g2 x g1 x y P x y y g1 x y y g2 x y y gn x y Q x y 3 变形并置规则 P F1 Q R F2 S Q R P F1 F2 S 程序正确性验证 Hoare公理学方法 4 证明过程证明程序部分正确性的公理学方法就是依据以上的公理和推理规则 一般有两种形式 1 正向 证明 从某些公理出发 使用规则 直到最后获得结果 根据给出的不变式断言 建立一些引理 根据引理和赋值公理 对程序中的每一个赋值语句Fi导出相应的不变式语句 Ri Fi Qi 再根据这些不变式语句和上述的推理规则逐步地组成越来越长的程序段 一直到推演出 P x F Q x z 为止 程序正确性验证 Hoare公理学方法 4 证明过程 2 反向 证明 先用规则 把总目标分成若干子目标 最后寻根于公理 从不变式语句 P x F Q x z 出发 利用有关的规则将它逐步分解 一直到将所有的语句推演为逻辑表达式 即检验条件 然后 证明这些逻辑表达式成立 这样就证明了程序的部分正确性 程序正确性验证 Hoare公理学方法 3 举例 例1 证明z sqrt x 的程序的部分正确性 START P x x 0 y1 y2 y3 0 1 1 While y2 x do p x y y12 xandy2 y1 1 2andy3 2 y1 1 y1 y2 y3 y1 1 y2 y3 2 y3 2 Z y1 Q x z z2 x z 1 2 HALT 程序正确性验证 Hoare公理学方法 正向证明 1 首先建立引理 引理1 P x P x 0 1 1 1 引理2 P x y y2 x P x y1 1 y2 y3 2 y3 2 2 引理3 P x y y2 x Q x y1 3 需要 并且可以证明他们是正确的 2 根据赋值公理有 P x 0 1 1 y1 y2 y3 0 1 1 P x y 4 得 P x y1 y2 y3 0 1 1 P x y 5 式1 4 结论 P x y1 1 y2 y3 2 y3 2 y1 y2 y3 y1 1 y2 y3 2 y3 2 P x y 6 得 P x y y2 x y1 y2 y3 y1 1 y2 y3 2 y3 2 P x y 7 程序正确性验证 Hoare公理学方法 4 取I为P x y Q为P x y y2 x 有 P I P x y y2 x Q 8 得 P x y While y2x 9 While规则 5 根据并置规则 有 x 0 y1 y2 y3 0 1 1 While y2x 10 程序正确性验证 Hoare公理学方法 6 Q x y1 Z y1 Q x z 赋值公理 得 P x y y2 x Z y1 Q x z 11 7 由 10 11 得 x 0 y1 y2 y3 0 1 1 While y2 x do y1 y2 y3 y1 1 y2 y3 2 y3 2 Z y1 Q x z 证明完毕 程序正确性验证 Hoare公理学方法 正向证明的讨论 引理就是不变式断言法中的检验条件但是 推理过程可以由建立的引理和赋值公理及推理规则 形成完整的程序 如果程序正确的话 Hoare已经将PASCAL语言全部公理化 并建立了一个公理化验证系统 程序正确性验证 Hoare公理学方法 例2 利用Hoare公理化方法证明程序的部分正确性START P X x0 0 y0 0 x0 0 y0 0 x y x0 y0 whilexneq0do p x y x 0 y 0 x0 0 y0 0 gcd x y gcd x0 y0 ify xtheny y x elses x y x y s y gcd x0 y0 z y Q x z z gcd x0 y0 HALT 程序正确性验证 Hoare公理学方法 反向证明 要证明程序A的部分正确性 只要证明 Goal1 P x BodyA Q x z 1 1 P x x y x0 y0 p x y 1 1 1P x p x0 y0 1 1 2 p x y whilex 0doify xtheny y xelses x y x y s y gcd x0 y0 1 3 y gcd x0 y0 z y Q x z 1 3 1y gcd x0 y0 Q x y 2 程序正确性验证 Hoare公理学方法 1 2 p x y whilex 0doify xtheny y xelses x y x y s y gcd x0 y0 1 2 1 p x y x 0 ify xtheny y xelses x y x y s p x y 1 2 1 1 p x y x 0 y x y y x p x y 1 2 1 1 1 p x y x 0 y x p x y x 3 1 2 1 2 p x y x 0 y x s x y x y s p x y 1 2 1 2 1 p x y x 0 y x p y x 4 1 2 2 p x y x 0 y gcd x0 y0 5 最后 只要证明上面最后得到的5个谓词表达式为真即可 程序正确性验证 Hoare公理学方法 反向证明过程讨论 反向证明过程开始于寻找一条适当规则W1 W2 WnW把证明目标W分解为子目标W1 W2 Wn 然后又把子目标Wi用同样的方法再细分 直至最后的子目标或归根于公理或问底于论域的定理 这个过程的每一步可用图表示为 WW1W2W3 Wn 程序正确性验证 Hoare公理学方法 练习1 用反向证明方法证明例1 2 用正向证明方法证明例2 小结 Floyd的断言归纳法证明部分正确性Floyd的良序集断言法证明终止性Hoare的公理学方法证明部分正确性 证明终止性的良序集方法 R W Floyd在1967年提出的良序集的概念1 偏序集设有一个非空集合W和一个定义在W上的二元关系 且这个关系满足下列性质 a 传递性 a b c W 如果a b b c 则有a cb 反对称性 a b W 如果a b 则有b ac 反自反性 a W a a称W为具有关系 的偏序集 记为 W 例 具有小于关系 的0到1之间的实数集合A1是偏序集具有关系 的全体整数的集合B1是偏序集 证明终止性的良序集方法 2 良序集定义 设 W a1 a2 称 W 是一个良序集 例 若N是自然数的集合 那么 N 是良序集 而上面的 A 和 B 不是良序集 若W是非负整数对的集合 在其上定义字典顺序 即 如果xi xj或者xi xjandyi yj则说 xi yi xj yj 这样规定的 W 是良序集 证明终止性的良序集方法 如果 W 是良序集 则 Wn n 也是良序集 这里Wn是W元素的所有n元组的集合 而n 是Wn上的正规字典序 例 具有小于关系的自然数集合N 即 N 是良序集 因此 自然数的所有序偶的集合 N2 2 也是良序集 具有小于关系的字母表 A B Z 是良序集 因此长度为3的字符串的集合 3 3 也是良序集 2 良序集 续 证明终止性的良序集方法 1 选择一个割点集合 去截断程序的各个循环部分 并在每一个截点i处建立一个中间断言qi x y 这样程序被分成若干个通路 同时规定每一通路都不含中间截断点 2 选取一个良序集 W 并且在每一个截断点i处定义一个终止表达式Ei x y 2 利用良序集方法证明程序的终止性设程序S的输入断言为P x 利用良序集方法证明S关于P x 是终止的 可按以下5个步骤进行 证明终止性的良序集方法 2 利用良序集方法证明程序的终止性 续 3 证明所选取的断言是 良断言 即 对于每一个从程序入口到断点j的通路a有 P x Ra x y qj x ra x y 对于每个有断点i到断点j的通路b有 qi x y Rb x y qj x rb x y 4 证明终止表达式是 良函数 即 对于每一个断言i有 qi x y Ei x y W 5 证明终止条件成立 即 对于每一条从断点i到j 且是每个循环的一部分的通路a有 qi x y Ra x