PMChap程序正确性证明.ppt

第七章 程序正确性证明1、概述 2、不变式断言法证明程序的部分正确性 3、良序集方法证明程序的终止性 4、Hoare公理学方法7.1 概述1. 基本概念n非形式化的程序验证是靠程序员阅读理解程 序完成的n程序测试是指测试者特意挑出一批输入数据 ，通过运行程序，检查每个输入数据所对应 的运行结果是否符合预期要求nDijkstra说过“程序测试只能证明程序有错 ，不能说明程序正确”n正确性证明是论证程序达到预期目的的一般 性陈述，而该论证不与程序输入数据的特定 值有关，但能够代表穷举性测试7.1 概述2. 关于程序正确性证明的早期工作n1967年，Floyd提出用“断言法”证明框图程序的正确性n1969年，Hoare在Floyd的基础上，定义了一个小语言 和一个逻辑系统他的工作为公理学语义的研究奠定了基 础n1973年，Hoare和Wirth把PASCAL语言的大部分公理 化n1974年，人们利用模逻辑验证并行程序的正确性n1975年一个基于公理和推导规则的自动验证系统首次 出现n1979年，出现了用公理化思想定义的程序设计语言 Euclidn1976年，Dijkstra提出了最弱前置谓词和谓词转换器 的概念，用于进行程序的正确性证明和程序的形式化推导 。

n1980年，D.Gries综合了以谓词演算为基础的证明系统 ，称之为“程序设计科学”首次把程序设计从经验、技术 升华为科学形式化的正确性证明技术n分三类：n以指称语义学为基础的描述方法，已 被VDM开发计划中采用n以代数语义学为基础的研究程序的终 止性、一致性和等价性的证明方法n以公理语义学为基础的正确性验证技 术n理论上发展的最完善nFloyd的归纳断言法nHoare的公理化方法nE.W.dijstra的最弱前置谓词法形式化的正确性证明技术n已开发的验证系统:nSPV(Stanford Pascal Verifier),基于Hoare技 术的Pascal程序验证系统nBOYER/MOORE证明器，证明LISP程序，其理 论基础是《计算逻辑》nHDM Verifier SPECIAL 验证系统nCDR（Correctness of Data Representation ），是抽象数据类型实现的正确性证明nGYPSY验证环境n验证与开发的顺序nGenerate and ProvenVerify while develop7.1 概述3. 程序正确性概念n定义1. 如果对于每一个使得P(ā)为真的输入ā ，程序S计算都终止，称程序S对P是终止的。

n定义2：对于满足P(ā)为真，且能够使程序S计 算终止的每个ā，如果Q(ā, P(ā))为真，则称 程序S对于P和Q是部分正确的记为[P] S [Q]⊢ [P] S [Q] iff (ā)((⊢p(ā) and (⊢ S terminates))⊢ Q(ā, P(ā))3. 程序正确性概念(续)n定义3：对于满足P(ā)为真的每个ā ，如果程 序S能够计算终止，且Q(ā, P(ā))为真，则称 程序S对于P和Q是完全正确的记为 {P} S{Q}⊢ {P} S{Q} iff ( ā)(⊢p(ā)  ((⊢ S terminates) and ⊢ Q(ā, P(ā)))⊢ [P] S [Q] iff (ā)((⊢p(ā) and (⊢ S terminates))⊢ Q(ā, P(ā))7.1 概述4. 主要的程序正确性证明方法 （1）关于部分正确性证明的方法nFloyd 的不变式断言法nManna的子目标断言法nHoare的公理化方法 （2）关于终止性证明的方法nFloyd的良序集方法nKnuth的计数器方法nManna等人的不动点方法 （3）关于完全正确性的证明方法nHoare的公理化方法（Manna、Pnueli）nBustall的间发断言法nDijkstra的弱谓词转换方法以及强验证方法。

7.1 概述5. 中间断言n定义1：在程序任一中间点 i 附 上谓词 ,如果每当执行 到达i时 对于该点的当 前值必为真，则 称 为 i 点上的中间断言，或称为归纳 断言n定义2：对于循环路径上的断言，因为每次循环执行到达该点 时该断言必为真，所以该断言 又称为循环不变式，简称不变 式开始x1,x2  y1,y2y1= y2?y1>y2?y1-y2  y1y2-y1  y2y1 z结束P(x)Ap(x,y)FBF EDGCQ(x,z)7.2 不变式断言法--证明部分正确性•证明步骤（分 三步） 1）建立断 言：选取断点 ，建立断言 2）建立检 验条件 3）验证检 验条件开始x1,x2  y1,y2y1= y2?y1>y2?y1-y2  y1y2-y1  y2y1 z结束P(x)Ap(x,y)FBFEDGCQ(x,z)7.2 不变式断言法--证明部分正确性1）建立断言：选 取断点，建立断 言n建立输入断 言n建立输出断 言，n若有循环， 在循环通路中 选取一个断点 来“分割”循环 ，并在此建立 一个适当的断 言开始x1,x2  y1,y2y1= y2?y1>y2?y1-y2  y1y2-y1  y2y1 z结束P(x)Ap(x,y)FBFEDGCQ(x,z)7.2 不变式断言法--证明部分正确性n2）建立检验条件n程序的执行可以分解为几条有限的通路，对每 一条通路建立一个检验条件。

n“检验条件”是程序运行通过通路时应满足的条 件具体地说：若将每一条通路看作一段程序， 它的输入断言、输出断言分别为 ，而且通过此通路的条件为 ，通过此通 路后y的值变为 ，则相应的检验条件为：7.2 不变式断言法--证明部分正确性3）验证检验条件n验证（2）中得到的所有的检验条 件，如果每一通路的检验条件均为真 ，则该程序是部分正确的7.2 不变式断言法 --证明部分正确性2. 举例 例：设x1,x2是正 整数，求它们 的最大公约数 ，即z = gcd(x1,x2)其流程图程序如 右图：开始x1,x2  y1,y2y1= y2?y1>y2?y1-y2  y1y2-y1  y2y1 z结束P(x)Ap(x,y)FBFEDGCQ(x,z)7.2 不变式断言法--证明部分正确性证明：n关于最大公约数的性质： IF y1>y2>0 then gcd(y1,y2) = gcd(y1- y2,y2) IF y2>y1>0 then gcd(y1,y2) = gcd(y1,y2- y1) IF y2=y1>0 then y1=y2 = gcd(y1,y2)n1) 建立断言：n输入断言：P(x) ： x1>0 and x2>0n输出断言：Q(x,z): z = gcd(x1,x2)n不变式断言： p(x,y): x1>0 ∧ x2>0 ∧y1> 0∧y2>0 ∧gcd(x1,x2) = gcd(y1,y2)7.2 不变式断言法--证明部分正确性n2) 建立检验条件n根据图中选择的切点，程序有四条通路：na1: A  Bna2: B  D  Bna3: B  E  Bna4: B G  Cn通路a1: nR1(x,y) = Truenr1(x,y) = (x1,x2)n检验条件： P(x) and R1(x,y)  p(x, r1(x,y) ) .(1)7.2 不变式断言法--证明部分正确性n通路a2(B  D  B): nR2(x,y) = (y1 neq y2 and y1>y2)nr2(x,y) = (y1-y2,y2)n检验条件：p(x,y) and R2(x,y)  p(x, r2(x,y) ) .(2)n通路a3(B  E  B): nR3(x,y) = (y1 neq y2 and y1 ≤ y2)nr3(x,y) = (y1,y2-y1)n检验条件：p(x,y) and R3(x,y)  p(x, r3(x,y) ) .(3)n通路a4(B  G  C): nR4(x,y) = (y1 = y2)nr4(x,z) = (y1)n检验条件：p(x,y) and R4(x,y)  Q(x, r4(x,z) ) .(4)开始x1,x2  y1,y2y1= y2?y1>y2?y1-y2  y1y2-y1  y2y1 z结束P(x)Ap(x,y)FBF EDGCQ(x,z)7.2 不变式断言法--证明部分正确性n3) 证明检验条件n将上面建立的四个检验条件展开，然后证明它们为真n(x1>0 ∧ x2>0 ∧True)  (x1>0 ∧ x2>0 ∧x1>0 ∧x2>0 ∧ gcd(x1,x2) = gcd(x1,x2)) .(1)n(x1>0 ∧ x2>0 ∧y1>0 ∧y2>0 ∧gcd(x1,x2) = gcd(y1,y2) ∧ y1 ≠ y2 ∧ y1>y2)  (x1>0 ∧ x2>0 ∧y1-y2>0 ∧y2>0 ∧ gcd(x1,x2) = gcd(y1- y2,y2))(2)n(x1>0 ∧ x2>0 ∧y1>0 ∧y2>0 ∧gcd(x1,x2) = gcd(y1,y2) ∧ y1 ≠ y2 ∧ y1 ≤ y2)  (x1>0 ∧ x2>0 ∧y1>0 ∧y2-y1>0 ∧ gcd(x1,x2) = gcd(y1,y2- y1))(3)n(x1>0 ∧ x2>0 ∧y1>0 ∧y2>0 ∧gcd(x1,x2) = gcd(y1,y2) ∧ y1 = y2  (y1 = gcd(x1,x2)) .(4)n结论：综上所述，该流程图程序是部分正确的。

7.2 不变式断言法--证明部分正确性3. 通路条件Ri(x,y)和变换函数ri(x,y)的求法 1）通路条件Ri(x,y)是指从穿过从i到j这条路径的条件 2）变换函数ri(x,y)描述了当这条路径被穿过后，程序变量 值的改变 3）求Ri(x,y)和ri(x,y)的反向代换技术： 从割点 i 到 j 的路径a， 反向代换技术为： a. 开始，置Ri(x,y)=True, ri(x,y) 为 y， 两者附 着在割点 j 上 b. 根据下面的构造R和r的规则，由 j 向i 反向移 动在割点 i 上得到的最终的R和r 就是所求的 Ri(x,y)和ri(x,y). c. 构造R和r的规则如下：7.2 不变式断言法--证明部分正确性c. 构造R和r的规则如下：R(x, y)∧t(x,y)r(x, y)y= f(x)老新R(x,f(x))r(x,f(x))R(x, y)r(x,y)y= g(x,y)老新R(x,g(x,y))r(x, g(x,y))R(x, y)r(x,y)老新R(x,y) ∧t(x,y)r(x,y)R(x, y)r(x,y)老新R(x, y)r(x,y)t(x,y) Tt(x,y) F7.2 不变式断言法--证明部分正确性nc. 构造R和r的规则如下(续)：新R(x,y)r(x,y)老R(x,y)r(x,y)7.2 不变式断言法--证明部分正确性4) 例：考虑下图，求该路径的路径函数R和 ry= g1(x,y)step1:Step2:R: T r: g3(x,y) R : T r : yFt1(x,y)y= g2(x,y)t2(x,y)Ty= g3(x,y)Step3:R: t2(x,y) r: g3(x,y)Step4:R: t2(x,g2 (x,y)) r: g3(x,g2(x,y))Step5:R: t1(x,y) ∧ t2(x,g2 (x,y)) r: g3(x,g2(x,y))Step6:R: t1(x,g1(x,y)) ∧ t2(x,g2 (x,g1(x,y))) r: g3(x,g2。