《程序正确性证明》PPT课件.ppt

第5章程序正确性证明 5 1程序正确性验证概述5 2不变式断言法5 3子目标断言法5 4界函数法 计数器法 5 1程序正确性概述 什么样的程序才是正确的 如何来保证程序是正确的 关于程序正确性的认识 什么样的程序才是正确的 测试 或 调试 方法根据问题的特性和软件所要实现的功能 选择一些具有代表性的数据 设计测试用例 通过用例程序执行 去发现被测试程序的错误 采用 测试 方法可以发现程序中的错误 但却不能证明程序中没有错误 因此 为保证程序的正确性 必须从理论上研究有关 程序正确性证明 的方法 程序正确性证明发展历程 20世纪50年代Turing开始研究 1967年 Floyd和Naur提出不变式断言法 1969年 Hoare提出公理化方法 1975年 Dijkstra提出最弱前置谓词和程序推导方法 解决了断言构造难的问题 可从程序规约推导出正确程序 使正确性证明变得实用 程序正确性理论是十分活跃的课题 不仅可以证明顺序程序的正确性 而且还可以证明非确定性程序 以及并行程序的正确性 程序正确性理论 程序设计的一般过程 程序正确性理论 程序功能的精确描述1 程序规约 对程序所实现功能的精确描述 由程序的前置断言和后置断言两部分组成 2 前置断言 程序执行前的输入应满足的条件 又称为输入断言 3 后置断言 程序执行后的输出应满足的条件 又称为输出断言 程序规约的基本分类 非形式化程序规约非形式化程序规约采用自然语言描述程序功能 简单 方便 但存在二义性 因此 不利于程序的正确性证明 形式化程序规约采用数学化的语言描述程序功能 描述精确 无二义性 便于程序的正确性证明 程序规约的实例 在书写程序规约时 使用Q表示前置断言 R表示后置断言 S表示问题求解的实现程序 在前置断言Q之前 还必须给出Q和R中所出现的标识符的必要说明 例1 求数组b 0 n 1 中所有元素的最大值 inn integer inb 0 n 1 arrayofinteger outy integer Q n 1 SR y MAX i 0 i n b i 程序规约的实例 例2 求两个非负整数的最大公约数 ina b integer outy integer Q a 0 b 0 SR y MAX i 1 i min a b amodi 0 bmodi 0 程序正确性定义 衡量一个程序的正确性 主要看程序是否实现了问题所要求的功能 若程序实现了问题所要求的功能 则称它为正确的 否则是不正确的 对程序的正确性理解 可以分为两个层次 从广义来说 一个程序的正确性取决于该程序满足问题实际需求的程度 从狭义而言 如果一个程序满足了它的程序规约就是正确的 程序正确性定义 程序规约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 为真的输入信息i 程序S的计算都将终止 并且R i S i 都为真 则称程序S关于Q和R是完全正确的 一个程序的完全正确 等价于该程序是部分正确 同时又是终止的 程序正确性的证明方法分类 证明部分正确性的方法A Floyd的不变式断言法B Manna的子目标断言法C Hoare的公理化方法终止性证明的方法A Floyd的良序集方法B Knuth的计数器方法C Manna等人的不动点方法完全正确性的方法A Hoare公理化方法的推广B Burstall的间发断言法C Dijkstra的弱谓词变换方法以及强验证方法 第5章程序正确性证明 5 1程序正确性验证概述5 2不变式断言法5 3子目标断言法5 4界函数法 计数器法 循环不变式断言 把反映循环变量的变化规律 且在每次循环体的执行前后均为真的逻辑表达式称为该循环的不变式断言 例带余整数除法问题 设x为非负整数 y为正整数 求x除以y的商q 以及余数r 程序 q 0 r x while r y 该循环不变式断言 r r y q q 1 x y q r r 0 5 2不变式断言法 证明步骤 1 建立断言建立程序的输入 输出断言 如果程序中有循环出现的话 在循环中选取一个断点 在断点处建立一个循环不变式断言 2 建立检验条件将程序分解为不同的通路 为每一个通路建立一个检验条件 该检验条件为如下形式 I R O其中I为输入断言 R为进入通路的条件 O为输出断言 3 证明检验条件运用数学工具证明步骤2得到的所有检验条件 如果每一条通路检验条件都为真 则该程序为部分正确的 不变式断言法实例1 例 设x y为正整数 求x y的最大公约数z的程序 即z gcd x y Functiongcd x1 x2 integer vary1 y2 z Integer Beginy1 x1 y2 x2 while y1y2 doif y1 y2 y1 y1 y2elsey2 y2 y1z y1 write z End 不变式断言法实例1 建立断言 输入断言 I x1 x2 x1 0 x2 0输出断言 O x1 x2 z z gcd x1 x2 循环不变式断言 P x1 x2 y1 y2 x1 0 x2 0 y1 0 y2 0 gcd y1 y2 gcd x1 x2 通路划分 通路1 a b通路2 b d b通路3 b e b通路4 b g c 不变式断言法实例1 建立检验条件 检验条件 I R O通路1 I x1 x2 P x1 x2 y1 y2 x1 0 x2 0 x1 0 x2 0 y1 0 Y2 0 gcd y1 y2 gcd x1 x2 通路2 P x1 x2 y1 y2 y1y2 y1 y2 P x1 x2 y1 y2 y2 x1 0 x2 0 y1 0 y2 0 gcd y1 y2 gcd x1 x2 y1y2 y1 y2 x1 0 x2 0 y1 y2 0 y2 0 gcd y1 y2 y2 gcd x1 x2 不变式断言法实例1 建立检验条件 通路3 P x1 x2 y1 y2 y1y2 y1P x1 x2 y1 y2 y1 x1 0 x2 0 y1 0 y2 0 gcd y1 y2 gcd x1 x2 y1y2 y1x1 0 x2 0 y1 0 y2 y1 0 gcd y1 y2 y1 gcd x1 x2 通路4 P x1 x2 y1 y2 y1 y2 O x1 x2 z x1 0 x2 0 y1 0 y2 0 gcd y1 y2 gcd x1 x2 y1 y2 z gcd x1 x2 不变式断言法实例1 证明检验条件 通路1 x1 0 x2 0 x1 y1 x2 y2 通路2 若y1 y2 gcd y1 y2 y2 gcd y1 y2 gcd x1 x2 通路3 若y2 y1 gcd y1 y2 gcd y1 y2 y1 gcd x1 x2 通路4 若y1 y2 gcd y1 y2 gcd x1 x2 y1 y2 zP x1 x2 y1 y2 y1 y2 O x1 x2 z 不变式断言法实例2 对任一给定的自然数x 计算z 即计算x的平方根取整 1 3 2n 1 n 1 2y1 n y3 2 y1 1 y2 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 不变式断言法实例2 检验条件 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 y2 x p x y1 1 y2 y3 2 y3 2 y12 x y2 y1 1 2 y3 2y1 1 y2 x y1 1 2 x y2 y3 2 y1 1 1 2 y3 2 2 y1 1 1通路3 B CP x y1 y2 y3 y2 x O x y1 y12 x y2 y1 1 2 y3 2y1 1 y2 x y12 x y1 1 2 不变式断言法实例2 检验条件2y12 x y2 y1 1 2 y3 2y1 1 y2 x y1 1 2 x y2 y3 2 y1 1 1 2 y3 2 2 y1 1 1证明 x y1 1 2 y2 x y2 y1 1 2 y2 y3 2 y1 1 2 2y1 1 2 y1 1 2 2 y1 1 1 y1 1 1 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 作业 课本P174习题1 习题2 要求用不变式断言法证明 第5章程序正确性证明 5 1程序正确性验证概述5 2不变式断言法5 3子目标断言法5 4界函数法 计数器法 5 3子目标断言法 子目标断言法与不变式断言法的主要区别是 两种方法对循环所建立的断言不同 不变式断言描述了程序变量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 x0 0 y0 0 输出断言O x y z z gcd x y 子目标断言P x y yend x 0 y 0 x 0 y 0 yend gcd x y START Read x y x0 y x y y x xy z y STOP T F T F I x y a P x y yend b c O x y z d e g 子目标断言法 建立检验条件 通路1 控制转出循环时 子目标断言成立 通路2 通路3 如果在通过循环之后 子目标断言在断点处成立 那么 在通过循环之前 断言也成立 通路4 如果输入断言为真 且控制第一次通过断点B时子目标断言为真 则输出断言为真 子目标断言法 建立检验条件 通路1 b c检验条件1x 0 P x y yend x 0 x 0 y 0 x 0 y 0 yend gcd x y 通路2 b d b检验条件2P x y x yend x0 y x P x y yend x 0 y x 0 x 0 y x 0 yend gcd x y x x0 y x x 0 y 0 x 0 y 0 yend gcd x y 通路3 b e b检验条件3P y x yend x0 yP x y yend 通路4 a b检验条件4x0 0 y0 0 x0 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 x 0 y x 0 yend gcd x y x x0 y x x 0 y 0 x 0 y 0 yend gcd x y 程序部分正确但不终止实例 例 求两个非负整数x y的最大公约数z的程序 ProgramAvarx y z s integer beginread x y whilex 0doify xtheny y x elsex x y z y write z end 可以利用不变式断言等方法证明该程序的部分正确性 但无法证明它是终止的 因为当y 0时 程序循环将不终止 第5章程序正确性证明 5 1程序正确性验证概述5 2不变式断言法5 3子目标断言法5 4界函数法 计数器法 5 5良序集方法证明程序终止性 1 基本概念偏序集良序集2 采用良序集方法证明程序终止性 偏序集的概念 偏序集设有一个非空集合W和一个定义在W上的二元关系 且这个关系满足下列性质 1 传递性 即对于一切a b c W 如果ab bc 则ac2 反对称性 即对于ab 则有b a3 反自反性 即对于一切a W a a称W为具有关系的偏序集 记做 W 例如 1 具有小于关系 的 位于0 1之间的实数集合A1 2 具有小于关系 的全体整数集合B1 但将 换成 就不是偏序集 1 具有小于等于关系 的 位于0 1之间的实数集合A1 2 具有小于等于关系 的全体整数集合B1 良序集的概念 良序集设 W 是偏序集 如果不存在由W中的元素构成的无限递减序列 a2a1a0 则称 W 是良序集 例如 1 若N是自然数集合 那么 N 是良序集 2 具有通常序ABC Z的字母表 A B Z 是良序集 下述集合A1和B1是偏序集 但不是良序集 1 具有小于关系 的 位于0 1之间的实数集合A1 2 具有小于关系 的全体整数集合B1 采用良序集证明程序终止性思路 结构化程序由顺序 选择和循环三种基本结构组成 而影响程序终止性的是循环结构 因此 是程序终止性证明的重点 程序终止性证明思路 A 选取良序集合 W B 选取割点集 割断循环 C 在割点上寻找函数u 使u W D 证明每次循环 u依次递减 由于良序集合 W 不存在无穷递减序列 因此 循环必然终止 用良序集方法证明程序终止性步骤 1 选取一个点集去截断程序的各个循环部分 并在每个截断点i处建立中间断言Qi x y 2 选取一个良序集 W 并在每个截断点处定义一个终止表达式Ei x y 表达式在W上取值 3 证明对每一个从程序入口到截断点j的通路aj有I x Raj x y Qj x raj x y 证明对每一个从截断点i到截断点j的通路aij 有Qi x y Raij x y Qj x raij x y 即证明中间断言是 正确的 是 良断言 4 证明Qi x y Ei x y W 即终止表达式是良函数 5 证明对于每一个从截断点i到截断点j的通路aij 有Qi x y Raj x y Ej x y Ei x y 良序集方法证明程序终止性实例 例子 对任一给定的自然数x 计算z 即计算x的平方根取整 良序集方法证明程序终止性实例 1 选取断点B 建立中间断言Q x y1 y2 y3 y202 取良序集 N B I x Q x y1 y2 y3 即 x 0 00 从截断点B B Q x y1 y2 y3 y2 y3Q x y1 1 y2 y3 y3 2 即 y20 y2 y3 y2 y30 良序集方法证明程序终止性实例 4 证明E x y 是良函数 即证明Q x y E x y N 即 y20 x y2 0 N5 证明终止条件成立 Q x y y2 y3 E x y1 1 y2 y3 y3 2 0 y2 y3 x y2 y3 x y2 采用良序集证明程序终止性总结 1 采用良序集方法证明程序终止性 关键在于选择合适的中间断言Qi x y 和终止表达式Ei x y 2 采用良序集证明程序终止性 与程序部分正确性证明采用了不同途径 相互完全独立 因此 证明程序的完全正确性工作量较大 3 采用计数器方法可以将程序的部分正确性和终止性证明结合进行 5 6计数器方法证明程序终止性 证明思路通过估计循环执行的最大次数证明程序终止性的方法 证明步骤 1 为程序的每一个循环附加一个新的变量作为该循环的计数器 初始值置为0 每循环一次该计数器加1 2 为每个循环设置一个中间断言 它表示相应的计数器不会超过固定的界限 3 证明 2 中的中间断言是不变式断言 计数器方法证明程序终止性实例 计算非负整数的最大公约数 varx y z s integer beginRead x y whilex 0dobeginIfy xtheny y x elses x x y y s endz y write z end 计数器方法证明程序终止性实例 1 引进计数器I 并建立如下断言x 0 y 0 2x y I 2x0 y0 varx y z s integer read x y I 0 计数器赋初值whilex 0dobeginify xtheny y x elses x x y y sfi I I 1 计数器递增End z y write z 计数器方法证明程序终止性实例 2 建立检验条件并证明 从而证明计数器断言为不变式断言 检验条件1 a b x0 0 y0 0 x0 0 y0 0 2x0 y0 0 2x0 y0 检验条件2 b d b x 0 y 0 2x y I 2x0 y0 x 0 y x x 0 y x 0 2x y x I 1 2x0 y0 证明 x 0 x 1 0 2x y x I 1 2x y I x 1 2x y I 2x0 y0检验条件3 b e b x 0 y 0 2x y I 2x0 y0 x 0 y y 0 x 0 2y x I 1 2x0 y0 证明 yy x 1 2y x I 1 y x 1 x I 1 y 2x I 2x0 y0由于2x y I 2x0 y0是不变式断言 因此 I 循环次数 必定小于常量2x0 y0 也就是循环只能执行有限次 即程序终止 采用计数器方法证明程序终止性和利用不变式断言法证明部分正确性步骤完全类似 只要再添加输出断言部分检验条件并证明 即可完成程序部分正确性证明 因此 可以把上述两者联合起来 完成程序的完全正确性证明 5 4界函数法 证明程序的可终止性 该方法是计数器方法的一种变形 证明程序的可终止性的常用方法 界函数法 对程序中的每一个循环 构造一个界函数 若该循环存在界函数 则该循环是可终止的 否则 该循环不可终止 界函数必须满足的条件 1 与循环变量有关的整函数 记为N x y 2 在循环的过程中N x y 0 3 每执行一次循环 N x y 的值减小 3 4界函数法 计数器法 例3 证明例1的可终止性 y1 x1 y2 x2 y1y2 y1 y2 z y1 y2 y2 y1 y1 y1 y2 A B C D E F T F T 取N x y max y1 y2 3 4界函数法 计数器法 因为x1 0 x2 0 所以循环第一次进入循环时y1 0 y2 0 进入循环以后 当y1 y2时 y1 y1 y2 0 y2不变 所以N x y 0 当y10 y1不变 所以N x y 0 故在循环过程中N x y 0 当y1 y2时 N y1 y2 y2 N y1 y2 当y1 y2时 N y1 y2 y1 N y1 y2 故随着循环的执行 N x y 递减 故该循环存在界函数N x y max y1 y2 所以该循环可终止 另一种计数器方法证明程序终止性 证明思路 对程序中的每一个循环 构造一个和该循环中变量有关的整数函数N x y 若N x y 满足以下两个条件 当循环条件成立时 N x y 0 每次循环 N x y 都减小 由N x y 的值构成一个单调递减的整数序列 N x y 0 因而 循环只能执行有限次 另一种计数器方法证明程序终止性实例 例 设x y为正整数 求x y的最大公约数z的程序 即z gcd x y 另一种计数器方法证明程序终止性实例 选取N y1 y2 max y1 y2 输入断言 I x1 x2 x1 0 x2 0当第一次进入循环时有y1 0 y2 0有算法得y1 y2 则y1 y2 y1 y2不变 y1y2 y1不变 始终有y1 0 y2 0于是就有N y1 y2 0 每执行一次循环 N y1 y2 是递减的 采用计数器方法证明程序终止性难点 采用计数器方法证明程序终止性关键在于确定一个合适的中间断言 或选取一个合适的函数N x y 尤其对于一些循环次数事先难以估计的程序 要找出循环次数的上限更为困难 正整数的一个性质 对于任意正整数 满足下列关系 若y1 y2 gcd y1 y2 gcd y1 y2 y2 若y2 y1 gcd y1 y2 gcd y1 y2 y1 若y1 y2 gcd y1 y2 y1 y2