程序正确性证明1.ppt

主要内容 程序正确性简介程序测试程序正确性证明 第5章程序的正确性证明 内容线索 程序正确性简介程序测试程序正确性证明 程序的正确性 所谓一段程序是正确的 是指这段程序能准确无误地完成编写者所期望赋予它的功能 或者说 对任何一组允许的输入信息 程序执行后能得到一组和这组输入信息相对应的正确的输出信息 通俗地说 做了它该做的事 没有做它不该做的事 程序正确性的严格定义分为三种类型部分正确性终止性完全正确性 如何保证程序的正确性 要求1 从编程时就应该尽量地避免和减少错误的发生2 当程序编好后要尽量找出错误 纠正错误避免错误的方法1 程序的结构要简单2 采用标准的软件设计工具 标准的算法手册以及有效的程序设计方法发现错误的方法1 利用测试工具2 利用程序的验证系统 内容线索 程序正确性简介程序测试程序正确性证明 程序测试 测试是程序的执行过程 目的在于发现错误 一个好的测试用例在于能发现至今未发现的错误 一个成功的测试是发现了至今未发现的错误的测试 测试的原则1 应当 尽早地和不断地进行软件测试 2 测试用例应由测试输入数据和对应的预期输出结果组成 3 程序员应避免检查自己的程序 4 在设计测试用例时 应当包括合理的输入条件和不合理的输入条件 5 充分注意测试中的群集现象 即测试后程序中残存的错误数目与该程序中已发现的错误数目成正比 6 严格执行测试计划 排除测试的随意性 7 应当对每一个测试结果做全面检查 8 妥善保存测试计划 测试用例 出错统计和最终分析报告 为维护提供方便 程序测试的过程 程序测试的过程 程序测试的方法 两种常用的测试方法黑盒测试这种方法是把测试对象看做一个黑盒子 测试人员完全不考虑程序内部的逻辑结构和内部特性 只依据程序的需求规格说明书 检查程序的功能是否符合它的功能说明 黑盒测试又叫做功能测试或数据驱动测试 白盒测试此方法把测试对象看做一个透明的盒子 它允许测试人员利用程序内部的逻辑结构及有关信息 设计或选择测试用例 对程序所有逻辑路径进行测试 通过在不同点检查程序的状态 确定实际的状态是否与预期的状态一致 因此白盒测试又称为结构测试或逻辑驱动测试 黑盒测试 黑盒测试方法是在程序接口上进行测试 主要是为了发现以下错误 是否有不正确或遗漏了的功能 在接口上 输入能否正确地接受 能否输出正确的结果 是否有数据结构错误或外部信息 例如数据文件 访问错误 性能上是否能够满足要求 是否有初始化或终止性错误 用黑盒测试发现程序中的错误 必须在所有可能的输入条件和输出条件中确定测试数据 来检查程序是否都能产生正确的输出 但这是不可能的 白盒测试 软件人员使用白盒测试方法 主要想对程序模块进行如下的检查 对程序模块的所有独立的执行路径至少测试一次 对所有的逻辑判定 取 真 与取 假 的两种情况都至少测试一次 在循环的边界和运行界限内执行循环体 测试内部数据结构的有效性等 白盒测试 对一个具有多重选择和循环嵌套的程序 不同的路径数目可能是天文数字 给出一个小程序的流程图 它包括了一个执行20次的循环 包含的不同执行路径数达520条 对每一条路径进行测试需要1毫秒 假定一年工作365 24小时 要想把所有路径测试完 需3170年 白盒测试 语句覆盖判定覆盖条件覆盖判定 条件覆盖条件组合覆盖路径覆盖 内容线索 程序正确性简介程序测试程序正确性证明简介Floyd不变式断言法子目标断言法Hoare规则公理方法 正确性证明 测试只能发现程序错误 但不能证明程序无错 原因 测试并没有也不可能包含所有数据 只是选择了一些具有代表性的数据 所以它具有局限性 正确性证明是通过数学技术来确定软件是否正确 也就是说 是否符合其规格说明 正确性证明的发展 正确性证明的方法 为了证明一个程序的完全正确性 通常采用的方法是分别证明该程序的部分正确性和终止性 主要方法有 关于部分正确性证明的方法Floyd的不变式断言法 Manna的子目标断言法Hoare的公理化方法 关于终止性证明的方法Floyd的良序集方法 Manna等人的不动点方法Knuth的计数器方法关于完全正确性证明的方法Hoare的公理化方法的推广 Manna Pnueli Burstall的间发断言方法Dijkstra最弱前置谓词变换方法以及强验证方法 程序正确性理论 程序功能的精确描述 1 程序规约 对程序所实现功能的精确描述 由程序的前置断言和后置断言两部分组成 2 前置断言 程序执行前的输入应满足的条件 又称为输入断言 3 后置断言 程序执行后的输出应满足的条件 又称为输出断言 预备知识 程序的状态 程序执行到某一时刻 程序中所有变量的一组取值初始状态 所有变量的取值使程序的前置断言为真的状态终止状态 所有变量的取值使程序的后置断言为真的状态程序的执行可以看作是程序状态的变迁 程序规约Q S R是一个逻辑表达式 其取值为真或假 其中取值为真的含义是指 给定一段程序S 若程序开始执行之前Q为真 S的执行将终止 且终止时R为真 则称为 程序S 关于前置断言Q和后置断言R是完全正确的 程序正确性定义 部分正确 若对于每个使得Q i 为真 并且程序S计算终止的输入信息i R i S i 都为真 则称程序S关于Q和R是部分正确的 程序终止 若对于每个使得Q i 为真的输入i 程序S的计算都终止 则称程序S关于Q是终止的 完全正确 若对于每个使得Q i 为真 并且程序S的计算都将终止的输入信息i R i S i 都为真 则称程序S关于Q和R是完全正确的 一个程序的完全正确 等价于该程序是部分正确 同时又是终止的 程序正确性定义 内容线索 程序正确性简介程序测试程序正确性证明简介Floyd不变式断言法Hoare规则公理方法Dijkstra最弱前置条件方法Dijkstra最弱前置条件方法 R W Floyd 1967年提出证明一个程序的部分正确性步骤 1 建立断言前置断言 x 前提条件 初始状态后置断言 x z 最终结论 终止状态满足的条件循环不变式 在循环中选取一个断点 在断点处建立一个适当的断言 使循环每次执行到断点时 断言都为真 2 建立检验条件 将程序分解为不同的通路 为每一个通路建立一个检验条件 该检验条件为如下形式 I R O 其中I为输入断言 R为进入通路的条件 O为输出断言 不变式断言法 2 建立检验条件检验条件 程序运行通过该通路时应满足的条件 i x y Ri x y i x ri x y 输入断言 输出断言 y 一组中间变量x 输入变量x y 蕴含符 即 ri x y 通过该通路后y的值 通过此路径的条件 3 证明检验条件 运用数学工具证明步骤2得到的所有检验条件 如果每一条通路检验条件都为真 则该程序为部分正确的 实例 设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 在B点建立不变式断言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 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 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 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 检验条件为真 不变式断言法实例 对任一给定的自然数x 计算z 即计算x的平方根取整算法 1 3 2n 1 n 1 2取 y1 n y3 奇数2n 1 y2 1 3 5 2n 1 n 1 2 y1 1 2 输入断言 I x x 0输出断言 O x z z2 x z 1 2循环不变式断言 P x y1 y2 y3 y12 x y2 y1 1 2 y3 2y1 1 A I x BP x y1 y2 y3 D C O x z T F B 不变式断言法实例 检验条件 I R O通路1 A BI x P x 0 1 1 x 0 0 x 1 0 1 2 1 2 0 1通路2 B D BP x y1 y2 y3 y2p x y1 1 y2 y3 2 y3 2 y12 y1 1 2CP x y1 y2 y3 y2 x O x y y12x y12 x y1 1 2 不变式断言法实例 检验条件2y12 x y2 y1 1 2 y3 2y1 1 y2 x y1 1 2 x y2 y3 2 y1 1 1 2 y3 1 2 y1 1 1证明 x y1 1 2y2 y3 2 y1 1 2 2y1 1 2 y1 2 2y3 2 2y1 1 2 2 y1 1 1检验条件3y12 x y2 y1 1 2 y3 2y1 1 y2 x y12 xx y1 1 2 同步练习 开始 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规则公理方法 子目标断言法 子目标断言法与不变式断言法的主要区别是 两种方法对循环所建立的断言不同 不变式断言描述了程序变量y的中间值与初始值之间关系 而子目标断言法描述的是y的中间值与循环终止时的最终值yend之间的关系 两种方法进行归纳的方向不同 不变式断言沿着程序正常执行的方向进行归纳 而子目标断言法则沿着相反方向进行归纳 不变式断言法 输入断言 I x y x0 0 y0 0输出断言 O x y z z gcd x y 循环不变式断言 P x y x 0 y 0 gcd x y gcd x0 y0 例 设x y为正整数 求x y的最大公约数z的程序 即z gcd x y 子目标断言法 建立断言 输入断言I x y x0 0 y0 0输出断言O x y z z gcd x y 子目标断言P x y yend x 0 y 0 yend gcd x y 当控制以x y的容许值通过L时 x y的当前值的最大公约数等于y的最终值 子目标断言法 建立检验条件 通路1 b c证明当控制最后一次通过L时 即控制转出循环时 子目标断言成立 检验条件1x 0 x 0 y 0 yend gcd x y 通路2 b d b通过循环的then通路之后的子目标断言蕴涵通过此通路之前的子目标断言 检验条件2P x y x yend x0 y x P x y yend x 0 y x 0 yend gcd x y x x0 y x x 0 y 0 yend gcd x y 通路3 b e b通过循环的else通路之后的子目标断言蕴涵通过此通路之前的子目标断言 检验条件3P y x yend x0 yP x y yend 通路4 a b证明如果输入断言为真 且当控制第一次通过L时子目标断言为真 则输出断言为真 检验条件4x0 0 y0 0 P x0 y0 yend yend gcd x0 y0 子目标断言法 证明检验条件 检验条件1 x 0 x 0 y 0 yend gcd x y 证明 因为有x 0 yend y所以yend y gcd 0 y gcd x y 检验条件2 P x y x yend x0 y x P x y yend 即证明 x 0 y x 0 yend gcd x y x x0 y x x 0 y 0 yend gcd x y 由 x0 y x y 0 以及gcd x y x gcd x y 当且仅当x 0 y 0可知yend gcd x y x gcd x y 内容线索 程序正确性简介程序测试程序正确性证明简介Floyd不变式断言法子目标断言法Hoare规则公理方法 公理化方法 公理化方法是由C A R Hoare于1969年提出的一种形式化的证明程序部分正确性的方法 一 while型程序 While型程序由一个有限的语句序列组成 每个语句之间以分号隔开 B0 B1 Bn其中B0是程序中唯一的开始语句 STARTy f x Bi是下列语句之一 1 赋值语句 y g x y 2 条件语句 ifRthenF1elseF2或者 ifRdoF1 3 循环语句 whileRdoF1 4 复合语句 beginF1 F2 Fkend 5 停机语句 z h x y HALT 二 不变式演绎系统 1 不变式语句 P F Q 其中P和Q是逻辑表达式 F是一个程序段 它的含义是 如果执行F以前P成立 且执行终止 则执行F后Q成立 这时不变式语句为真 不变式语句也称为归纳表达式 2 推理规则A1 A2 AnB其中B是一个不变式语句 Ai i 1 n 是一个逻辑表达式或者是其他的不变式语句 它的含义是 为了推论后项B为真 只需证明前项A1 A2 An为真 为了证明不变式语句 Hoare定义了1条赋值公理和4条推理规则 1 赋值公理 P x g x y y g x y P x y 2 条件规则 S1 Q 和 S2 Q 为表示方便 我们可用证明规则的一般形式显然 上述条件语句的二种形式分别可表示为 Hoare验证系统 3 while规则 1 whileBdoS P I表示当控制进入循环时 不变式I为真 条件 I R F I 表示I是不变式 即如果执行F前I为真 且F执行终止 则F执行后I仍为真 条件I R Q表示如果控制退出循环 Q将是真 Hoare验证系统 4 并置规则 P F1 R R F2 Q P F1 F2 Q 5 结论规则P R R F Q P F Q 或者 P F R R Q P F Q P true PA 0 B A B 0 B 0 PA 0 B A B 0 则 true ifA 0thenB AelseB A B 0 例 计算X MAX A B 的程序为ifA BthenX AelseX B 试验证其正确性 证明 P true PA B X A X AX B PAA 而X AX BX MAX A B X BX AX MAX A B 故 P true ifA BthenX AelseX B X MAX A B 例 证明程序部分正确性的公理化方法就是依据以上的几条公理和规则进行的 推理过程一般有两种形式 1 根据给出的不变式断言 建立一些引理 根据这些引理和赋值公理 对程序P中的每一个赋值语句Fi导出相应的不变式语句 Ri Fi Qi 再根据这些不变式语句和上述的四条规则逐步地组成越来越长的程序段 一直到推导出 x P x z 为止 这样就证明了程序P的部分正确性 2 从不变式语句 x P x z 出发 利用有关的规则将它逐步分解 一直到将所有的语句推演为逻辑表达式 即检验条件 然后 证明这些逻辑表达式成立 这样就证明了程序的部分正确性 例利用公理化方法证明例5 2中的程序的部分正确性START x 0 y1 y2 y3 0 1 1 Whiley2 xdo P x y y1 y2 y3 y1 1 y2 y3 2 y3 2 Z y1 x z HALT 引理5 1X 0 P x 0 1 1 引理5 2P x y y2P x y1 1 y2 y3 2 y3 2 引理5 3P x y y2 x x y1 1 根据赋值公理有 P x 0 1 1 y1 y2 y3 0 y1 y2 y3 0 1 1 P x y 2 和 1 类似 根据赋值公理 引理5 2和结论规则 P x y y2 x y1 y2 y3 x y1 1 y2 y3 2 y3 2 P x y 3 取I为P x y Q为P x y y2 x 根据while规则和 2 中的结论可得 P x y Whiley2x 4 根据并置规则和