《程序正确性证明》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：求数组b0 : n-1中所有元素的最大值。 in n:integer; in b0:n-1:array of integer; out y:integer Q: n 1 S R:y MAX(i: 0 i n; bi),程序规约的实例,例2：求两个非负整数的最大公约数。 in a,b :integer; out y:integer Q: a 0 b 0 S R:y MAX(i: 1 i min(a,b) (a mod i 0) (b mod i 0),程序正确性定义,衡量一个程序的正确性，主要看程序是否实现了问题所要求的功能。若程序实现了问题所要求的功能，则称它为正确的，否则是不正确的。 对程序的正确性理解，可以分为两个层次： 从广义来说，一个程序的正确性取决于该程序满足问题实际需求的程度。 从狭义而言，如果一个程序满足了它的程序规约就是正确的。,程序正确性定义,程序规约QSR是一个逻辑表达式，其取值为真或假。 其中取值为真的含义是指：给定一段程序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。 程序： q0；rx； while( r y) /该循环不变式断言： r ry； q q1； ,/(xyqr ) r 0,5.2 不变式断言法,证明步骤： 1、建立断言 建立程序的输入、输出断言，如果程序中有循环出现的话，在循环中选取一个断点，在断点处建立一个循环不变式断言。 2、建立检验条件 将程序分解为不同的通路，为每一个通路建立一个检验条件，该检验条件为如下形式： I R = O 其中I为输入断言，R为进入通路的条件，O为输出断言。 3、证明检验条件 运用数学工具证明步骤2得到的所有检验条件，如果每一条通路检验条件都为真，则该程序为部分正确的。,不变式断言法实例1,例：设x,y为正整数，求x,y的最大公约数z的程序，即z=gcd(x,y)。,Function gcd(x1,x2:integer); var y1,y2,z : Integer; Begin y1:=x1;y2:=x2; while (y1y2) do if (y1y2) y1:=y1-y2 else y2:=y2-y1 z:=y1; write(z); End.,不变式断言法实例1(建立断言),输入断言： I(x1,x2): x10 x20 输出断言： O(x1,x2,z):z=gcd(x1,x2) 循环不变式断言： P(x1,x2,y1,y2): x10 x20 y10 y20 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) x10 x20 = x10 x20 y10 Y20 gcd(y1,y2)=gcd(x1,x2) 通路2： P(x1,x2,y1,y2) y1y2 y1y2 = P(x1,x2,y1-y2,y2) x10 x20 y10 y20 gcd(y1,y2)=gcd(x1,x2) y1y2 y1y2 = x10 x20 y1-y20 y20 gcd(y1-y2,y2)=gcd(x1,x2),不变式断言法实例1(建立检验条件),通路3： P(x1,x2,y1,y2) y1y2 y1 P(x1,x2,y1,y2-y1) x10 x20 y10 y20 gcd(y1,y2)=gcd(x1,x2) y1y2 y1 x10 x20 y10 y2-y10 gcd(y1,y2-y1)=gcd(x1,x2) 通路4： P(x1,x2,y1,y2) y1=y2 = O(x1,x2,z) x10 x20 y10 y20 gcd(y1,y2)=gcd(x1,x2) y1=y2 = z=gcd(x1,x2),不变式断言法实例1(证明检验条件),通路1： x10 x20 x1=y1 x2=y2 = 通路2： 若y1y2, gcd(y1-y2,y2) = gcd(y1,y2) =gcd(x1,x2) 通路3: 若y2y1, gcd(y1,y2)=gcd(y1,y2-y1) =gcd(x1,x2) 通路4: 若y1=y2,gcd(y1,y2) =gcd(x1,x2)=y1=y2=z P(x1,x2,y1,y2) y1=y2 = O(x1,x2,z),不变式断言法实例2,对任一给定的自然数x，计算z ，即计算x的平方根取整。 13(2n+1)=(n+1)2 y1=n; y3=2y1+1; y2= (y1+1)2 输入断言： I(x):x0 输出断言： 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-B I(x)= P(x,0,1,1) x0= 0 x 1=(0+1) 2 1=2*0+1 通路2：B-D-B P(x,y1,y2,y3) y2x = p(x,y1+1,y2+y3+2,y3+2) y12x y2=(y1+1)2 y3 = 2y1+1 y2x = (y1+1) 2 x y2+y3+2=(y1+1+1) 2 y3+2=2(y1+1)+1 通路3：B-C P(x,y1,y2,y3) y2x =O(x,y1) y12 x y2=(y1+1)2 y3 = 2y1+1 y2x = y12 x(y1+1)2,不变式断言法实例2,检验条件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 证明： 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)2 y3+2=2y1+1+2=2(y1+1)+1 检验条件3 y12 x y2=(y1+1)2 y3 = 2y1+1 y2x = 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 (x00 y00) 输出断言 O(x,y,z): z=gcd(x,y) 子目标断言 P(x,y,yend): x=0 y=0 (x0 y0) = yend = gcd(x,y),START,Read(x,y),x0,y=x,y:=y-x,x y,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 检验条件1 x=0 = P(x,y,yend) x=0 = x=0 y=0 (x0 y0) = yend =gcd(x,y) 通路2：b-d-b 检验条件2 P(x,y-x, yend) x0 y=x =P(x,y, yend) x=0 y-x=0 (x0 y-x0) = yend = gcd(x,y-x) x0 y=x = x=0 y=0 (x0 y0) = yend = gcd(x,y) 通路3：b-e-b 检验条件3 P(y,x, yend) x0 y P(x,y, yend) 通路4：a-b 检验条件4 x0 =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 yx =P(x,y, yend) 即证明： x=0 y-x=0 (x0 y-x0) = yend = gcd(x,y-x) x0 y=x = x=0 y=0 (x0 y0) = yend = gcd(x,y) ,程序部分正确但不终止实例,例：求两个非负整数x、y的最大公约数z的程序。,Program A var x,y,z,s:integer; begin read(x,y); while x 0 do if y x then y = y x; else x = x y; z = y; write (z); end.,可以利用不变式断言等方法证明该程序的部分正确性，但无法证明它是终止的。 因为当y0时，程序循环将不终止！,第5章 程序正确性证明,5.1程序正确性验证概述 5.2不变式断言法 5.3子目标断言法 5.4界函数法计数器法,5.5良序集方法证明程序终止性,1.基本概念 偏序集 良序集 2.采用良序集方法证明程序终止性,偏序集的概念,偏序集 设有一个非空集合W和一个定义在W上的二元关系 ，且这个关系 满足下列性质： 1）传递性，即对于一切a,b,cW,如果a b,b c ，则a c 2）反对称性，即对于a b,则有ba 3）反自反性，即对于一切aW，aa 称W为具有关系 的偏序集，记做（W, ）。 例如： （1）具有小于关系（）的，位于01之间的实数集合A1。 （2）具有小于关系（）的全体整数集合B1。 但将 换成 就不是偏序集。 （1）具有小于等于关系（）的，位于01之间的实数集合A1。 （2）具有小于等于关系（）的全体整数集合B1。,良序集的概念,良序集 设（W, ）是偏序集，如果不存在由W中的元素构成的无限递减序列: a2 a1 a0 ，则称（W, ）是良序集。 例如： （1）若N是自然数集合，那么（N，）是良序集。 （2）具有通常序A B C Z的字母表=A,B,Z是良序集。 下述集合A1和B1是偏序集，但不是良序集。 （1）具有小于关系（）的，位于01之间的实数集合A1。 （2）具有小于关系（）的全体整数集合B1。,采用良序集证明程序终止性思路,结构化程序由顺序、选择和循环三种基本结构组成，而影响程序终止性的是循环结构，因此，是程序终止性证明的重点。 程序终止性证明思路： A. 选取良序集合（W, ）； B. 选取割点集，割断循环； C. 在割点上寻找函数u，使uW； D. 证明每次循环，u依次递减。 由于良序集合（W, ）不存在无穷递减序列，因此，循环必然终止。,用良序集方法证明程序终止性步骤,1.选取一个点集去截断程序的各个循环部分，并在每个截断点i处建立中间断言Qi (x,y)； 2.选取一个良序集(W, )，并在每个截断点处定义一个终止表达式E i (x,y)，表达式在W上取值； 3.证明对每一个从程序入口到截断点j的通路aj有 I(x) Raj (x,y) = Qj(x,raj(x,y) 证明对每一个从截断点i到截断点j的通路aij ，有 Qi (x,y) R a i j (x,y) = Q j (x,r a i j (x,y) 即证明中间断言是“正确的”，是“良断言”； 4.证明 Qi (x,y) = E i (x,y) W，即终止表达式是良函数； 5.证明对于每一个从截断点i到截断点j的通路aij ，有 Qi (x,y) Raj (x,y) =E j (x,y) E i (x,y)。,良序集方法证明程序终止性实例,例子：对任一给定的自然数x，计算z ，即计算x的平方根取整。,良序集方法证明程序终止性实例,1.选取断点B ，建立中间断言 Q(x,y1,y2,y3): y2 0 2.取良序集（N,B ：I(x) = Q(x,y1,y2,y3)， 即：x0=0 0 从截断点B-B： Q(x,y1,y2,y3) y2+y3 Q(x,y1+1,y2+y3,y3+2) 即：y2 0 y2+y3 y2+y3 0,良序集方法证明程序终止性实例,4.证明E(x,y)是良函数，即证明Q(x,y) = E(x,y)N ，即 y2 0 = x-y20 N 5.证明终止条件成立 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）中的中间断言是不变式断言。,计数器方法证明程序终止性实例,计算非负整数的最大公约数,var x,y,z,s: integer; begin Read(x,y) while x0 do begin If yx then y:=y-x; else s:=x;x:=y;y:=s; end z:=y;write(z); end,计数器方法证明程序终止性实例,1.引进计数器I,并建立如下断言 x0 y 0 2x+y+I 2x0+y0,var x,y,z,s: integer; read(x,y); I:=0; /计数器赋初值 while x0 do begin if y x then y:=y-x; else s:=x;x:=y;y:=s fi; I:= I+1; /计数器递增 End; z:=y; write(z);,计数器方法证明程序终止性实例,2.建立检验条件并证明，从而证明计数器断言为不变式断言。 检验条件1：a - b x00y00 = x00y002x0+y0+02x0+y0 检验条件2：b - d - b x0y0(2x+y+I2x0+y0)x0yx = x0y-x0(2x+(y-x)+I+12x0+y0) 证明： x0 = (x-10) 2x+(y-x)+I+1=2x+y+I-(x-1) 2x+y+I 2x0+y0 检验条件3：b - e - b x0y0(2x+y+I2x0+y0)x0y y0x0(2y+x+I+1 2x0+y0) 证明： (y yx-1) 2y+x+I+1y+x-1+x+I+1=y+2x+I 2x0+y0 由于2x+y+I2x0+y0是不变式断言，因此，I（循环次数）必定小于常量2x0+y0 ，也就是循环只能执行有限次，即程序终止。,采用计数器方法证明程序终止性和利用不变式断言法证明部分正确性步骤完全类似，只要再添加输出断言部分检验条件并证明，即可完成程序部分正确性证明。 因此，可以把上述两者联合起来，完成程序的完全正确性证明。,5.4界函数法证明程序的可终止性,该方法是计数器方法的一种变形，证明程序的可终止性的常用方法.,界函数法:对程序中的每一个循环,构造一个界函数,若该循环存在界函数,则该循环是可终止的,否则,该循环不可终止.,界函数必须满足的条件: (1)与循环变量有关的整函数,记为N(x,y); (2)在循环的过程中N(x,y)0; (3)每执行一次循环, N(x,y)的值减小.,3.4界函数法计数器法,例3.证明