PM讲义-第5章 最弱前置谓词和程序语言的语义ppt课件

1、五章、五章、 最弱前置谓词和程序语言的语义最弱前置谓词和程序语言的语义n前言前言n引进最弱前置谓词（引进最弱前置谓词（Weakest Pre-predicate）的概念，）的概念，n并用它来定义一个小程序语言并用它来定义一个小程序语言L。该语言的主。该语言的主要成分：要成分：n赋值语句、赋值语句、n选择语句、选择语句、n循环语句，循环语句，n数据类型只有整型和布尔型数据类型只有整型和布尔型5.1 最弱前置谓词最弱前置谓词1.定义：假定定义：假定S是一个语句，是一个语句，Q是一个谓词，它描是一个谓词，它描述述S执行后所确定的某种关系。从执行后所确定的某种关系。从S和和Q定义另外定义另外一个谓词，

2、记为一个谓词，记为 wp(S,Q),它表示：它表示： “所有这样的状态的集合，所有这样的状态的集合，S S从其中任一状态开从其中任一状态开始执行必将在有限的时间内终止于满足始执行必将在有限的时间内终止于满足Q Q的状的状态态”。- S - wp(S,Q) Q 5.1 最弱前置谓词最弱前置谓词 我们称我们称 wp(S,Q) 是语句是语句S关于关于Q的的最弱前置谓词最弱前置谓词。“最弱最弱”反映在反映在“所有所有”一词之中，外延最大，内一词之中，外延最大，内涵自然最弱。涵自然最弱。5.1 最弱前置谓词最弱前置谓词例例1. 假设假设S是赋值语句是赋值语句 i := i+1; Q为为 i10 则：则：

3、 wp(S,Q)= wp(i := i+1, i10 )= (i 9)5.1 最弱前置谓词最弱前置谓词例例2. 假设假设S是是 if x=y then z:=x else z:=y Q为为 z:=max(x,y) 则：则：wp(S,Q) = T例例3. 令令S同例同例2， Q为为 z:=y, 则：则：wp(S,Q) = (x y)例例4. 令令S同例同例2， Q为为 z = y-1, 则：则： wp(S,Q) = FALSE5.1 最弱前置谓词最弱前置谓词wp(S,Q)与 P S Q：nP S Q表示 “若若S的执行开始于一个满足的执行开始于一个满足P的的状态，则状态，则S的执行必在有限的时间

4、内终止于一个的执行必在有限的时间内终止于一个满足满足Q的状态的状态” wp(S,Q)表示“所有这样的状态的集合，所有这样的状态的集合，S从其从其中任一状态开始执行必将在有限的时间内终止于中任一状态开始执行必将在有限的时间内终止于满足满足Q的状态的状态” 因此： P S Q ( P wp(S,Q)5.2 基本语句的语义前言基本语句的语义前言n前言：前言：n用用wp定义一个小程序设计语言定义一个小程序设计语言L，此语言的，此语言的表达式只有整型和布尔型两类，说明语句采表达式只有整型和布尔型两类，说明语句采用类用类Pascal的形式，其基本执行语句有空语的形式，其基本执行语句有空语句（句（Skip）

5、、赋值语句、选择语句、循环语）、赋值语句、选择语句、循环语句。句。n令记号令记号“=df” 为定义符，读做为定义符，读做“定义为定义为”5.2 基本语句的语义-空语句空语句1.空语句（空语句（Skip）Skip语句表示什么事都不做，相当于空语句。语句表示什么事都不做，相当于空语句。其定义如下：其定义如下：定义定义1： wp(skip,Q) =df Q5.2 基本语句的语义基本语句的语义-赋值语句赋值语句2. 赋值语句赋值语句1）简单变量赋值）简单变量赋值n 赋值形式：赋值形式： y := en 其中其中y为简单变量，为简单变量，e为表达式；为表达式；y，e必须相必须相同类型。这个语句在某种状态

6、下执行意味着：同类型。这个语句在某种状态下执行意味着：首先在此状态下计算出首先在此状态下计算出e的值，然后将此值存放的值，然后将此值存放在以在以y为名字的存储单元中，即用为名字的存储单元中，即用e的值代替的值代替y的的值。值。5.2 基本语句的语义基本语句的语义-赋值语句赋值语句n定义定义2：wp(“y := e”,Q) =df domain(e) 其中，其中， domain(e) 是一个谓词，表示所有使是一个谓词，表示所有使e可求值的可求值的状态集。状态集。在多数情况下，在多数情况下， domain(e) 总是成立，故常省略它，只总是成立，故常省略它，只写：写： wp(“y := e”,Q)

7、 =dfy ye eQ Qy ye eQ Q5.2 基本语句的语义基本语句的语义例1：例2：例3：例4： 5)y,5:ywp( p(x),a/b:xwp( 0)x,1x:xwp( 5)x,5:xwp(5.2 基本语句的语义基本语句的语义例1：例2：例3：例4：false 5)(5 5)y,5:ywp(p(a/b) 0(b p(x),a/b:xwp(-1)(x 0)(x 0)x,1x:xwp(True )5)(x 5)x,5:xwp(x1xx55.2 基本语句的语义 多个简单变量的同时赋值多个简单变量的同时赋值2)多个简单变量的同时赋值多个简单变量的同时赋值)(:1:)()(),:(4.,.,2

8、, 1;,.,2, 1) 1(:eidomainniiedomainQedomainQexwpeneenexnxxnxexsxedf其中：定义个表达式为个互不相同的变量为其中例例8：wp(“x,y:=x-y,y-x”,x+y=c) = （x-y+y-x = c） = (0 = c)5.2 基本语句的语义顺序复合顺序复合3. 顺序复合顺序复合考虑由两个语句考虑由两个语句s1和和s2构成的复合语句构成的复合语句“s1;s2”的语的语义：义：定义定义5： wp(“s1;s2”,Q) =df wp(“s1”,wp(“s2”,Q)5.2 基本语句的语义顺序复合顺序复合wp(“s1;s2”,Q) =df

9、wp(“s1”,wp(“s2”,Q)例：例： wp(“t:=x; x:=y; y:=t”, x=u2 y=u1) =wp(“t:=x; x:=y”,wp(“y:=t”, x=u2 y=u1) =wp(“t:=x; x:=y”, x=u2 t=u1) =wp(“t:=x”,wp(“x:=y”, x=u2 t=u1) =wp(“t:=x”,y=u2 t=u1) = y=u2 x=u15.2 基本语句的语义基本语句的语义选择语句选择语句形式：形式： IF := if c1 s1; c2 s2; . cn sn; fi其中，其中，n0; ci为布尔表达式为布尔表达式; si为任意为任意语句语句; ci

10、 si是一个带卫哨（是一个带卫哨（Guard）语句语句, ci为为si的卫哨的卫哨;用用 BB表示所有卫哨的析取：表示所有卫哨的析取： BB = c1 c2 . cnIF语句的执行过程：语句的执行过程：首先计算每个首先计算每个ci，若所有若所有ci都不为真，或都不为真，或 有某个有某个ci无定义则执行中无定义则执行中断（断（abort），否则，执），否则，执行任一个其值为真的行任一个其值为真的ci所所对应的对应的si。当当si执行完毕后，整个执行完毕后，整个IF就执行完了。就执行完了。5.2 基本语句的语义基本语句的语义n定义定义6：wp(IF,Q) =df domain(BB) BB c1w

11、p(s1,Q) c2wp(s2,Q) . cnwp(sn,Q) =df domain(BB) ( j : 1j n : cj) ( i : 1i n : ci wp(si,Q) )5.2 基本语句的语义基本语句的语义n例：令例：令IF为为 if x=0 y := x x=0 x=0 wp(“y := x”, y = abs(x) x=0 x= abs(x) x y x,y :=y,x; x=y skip fi已知已知P=True，Q = (x0, ci 为布尔为布尔表达式表达式, si 为语句为语句, c1 s1为带哨语句为带哨语句DO 语句的执行如下语句的执行如下: 首先计算每个首先计算每个

12、ci, 若有某个若有某个ci无定义无定义,则执则执行失败行失败(流产流产) 。 若所有若所有ci均为假均为假,则执行则执行终止终止, 否则执行任意其值否则执行任意其值为真的为真的ci所对应的所对应的si. 重复这个过程直至执行重复这个过程直至执行终止或失败终止或失败.DO语句等价于语句等价于: do BB IF od5.2 基本语句的语义基本语句的语义为给出为给出DO语句的形式语义语句的形式语义, 先定义两个符号先定义两个符号n令令: H0(Q) = BBQ 它是这样的一个状态集合它是这样的一个状态集合: DO从其中任一状态开从其中任一状态开始执行不经过任何迭代始执行不经过任何迭代(0次迭代次

13、迭代)即终止即终止,且终止时且终止时Q为真。为真。n定义一个谓词定义一个谓词H Hk k(Q) , k0. 它表示这样的一个状它表示这样的一个状态集合态集合: DO从其中任一状态开始执行从其中任一状态开始执行,最多经过最多经过k次迭代而终止次迭代而终止,且终止时且终止时Q为真。因此为真。因此,它可以表示它可以表示为为: Hk(Q) = H0(Q) wp(IF, Hk-1(Q) ), k05.2 基本语句的语义基本语句的语义n定义一个谓词定义一个谓词H Hk k(Q) , k0. 它表示这样的一它表示这样的一个状态集合个状态集合: DO从其中任一状态开始执行从其中任一状态开始执行,最多经过最多经

14、过k次迭代而终止次迭代而终止,且终止时且终止时Q为真。为真。因此因此,它可以表示为它可以表示为:nHk(Q) = H0(Q) wp(IF, Hk-1(Q) ), k0nH1(Q) = H0(Q) wp(IF, H0(Q) )nH2(Q) = H0(Q) wp(IF, H1(Q) )5.2 基本语句的语义基本语句的语义nwp(DO, Q)可以定义为这样一个状态集合可以定义为这样一个状态集合: DO从其中任一状态开始执行从其中任一状态开始执行,必须经过有限次必须经过有限次迭代后终止于满足迭代后终止于满足Q的状态。于是的状态。于是:n定义定义7:n wp(DO, Q) =df ( k: k0 : H

15、k(Q) )n由于由于Hk(Q) 的构造甚为麻烦。因此的构造甚为麻烦。因此, wp(DO, Q) 的定义实际上不便于使用的定义实际上不便于使用, 但可用于证明但可用于证明一个有用的定理。一个有用的定理。5.2 基本语句的语义基本语句的语义不变式不变式 n不变式不变式 ： 不必要求一定得到不必要求一定得到DO语句的最弱前置条件语句的最弱前置条件wp(DO,Q)，可以，可以寻找一个稍强的前置条件寻找一个稍强的前置条件 ，它满足：在，它满足：在DO执行之前成立，而执行之前成立，而且每经过一次迭代后也仍然保持成立，并且还能够保证且每经过一次迭代后也仍然保持成立，并且还能够保证BB Q 为真。因此，用为

16、真。因此，用 作为循环作为循环DO对于对于Q的前置条件。即寻的前置条件。即寻找满足下列形式的找满足下列形式的 ： do BB BB IF od; BB Q因为因为 在循环的每轮迭代的执行前后均保持为真，因此称在循环的每轮迭代的执行前后均保持为真，因此称 为该循环的一个不变式（为该循环的一个不变式（Invariant）5.2 基本语句的语义基本语句的语义界函数界函数 界函数界函数 ：n为说明循环的终止性，引入一个整型函数为说明循环的终止性，引入一个整型函数 ，它是，它是程序变量的函数，程序变量的函数， 用以指明循环至多执行用以指明循环至多执行 次迭代。次迭代。它满足：它满足：n 的值随迭代次数的

17、增加而递减，每次迭代的值随迭代次数的增加而递减，每次迭代 的值的值至少递减至少递减1，且，且:n只要能够继续迭代，只要能够继续迭代， 的值就一定保持的值就一定保持0n因此，只要表明存在这样的函数因此，只要表明存在这样的函数 ，循环就必定能，循环就必定能够终止，够终止， 称称 为循环的界函数（为循环的界函数（Bound Function）5.2 基本语句的语义基本语句的语义n例例1：计算数组：计算数组b0:10元素的和，并将结果存于元素的和，并将结果存于变量变量s中的程序为：中的程序为： i := 1; s := b0; do i11 s := s+bi ; i := i+1; od Q: s

18、= k: 0k 11 : bk 令：令： 为为 1i 11 s = (k: 0k 0 （3） ci wp(“ 1 := ; si”, 05.对每个对每个 i，1in， ci 1 := ; si” 1n形式化注释如下：形式化注释如下：5.2 基本语句的语义基本语句的语义P 不变式不变式 界函数界函数do c1 s1 c2 s2 cn snodBB Q例例2：证明下述程序的正确性：证明下述程序的正确性T i := 1; s := b0; : 1i 11 s = (k: 0k i : bk) : 11-i do i11 s := s+bi ; i := i+1; od Q: s = k: 0k 11

19、 : bk5.2 基本语句的语义基本语句的语义n证明：证明：(1)（证明（证明 在循环执行前为真在循环执行前为真） wp(“i := 1; s := b0”, ) (1111 b0 = (k: 0k 1 : bk) 1111 b0 = b0 True True i := 1; s := b0 成立，成立， 即循环开始时即循环开始时 成立成立5.2 基本语句的语义基本语句的语义（2）wp(“s := s+bi ; i := i+1”, ) 1i+111 s+bi = (k: 0k i+1 : bk) 0 i11 s= (k: 0k i : bk) i11 i111i11s=(k:0ki:bk)

20、1 i11 s= (k: 0k i : bk) i11 wp(“s := s+bi ; i := i+1”, ) 成立，即 是循环不变式是循环不变式5.2 基本语句的语义基本语句的语义（3） BB 1i 11s = (k: 0k i : bk) i11 i=11 s = (k: 0k i : bk) s = (k: 0k 11 : bk Q 循环终止时，循环终止时，Q为真为真5.2 基本语句的语义基本语句的语义(4)说明只要循环不终止，函数说明只要循环不终止，函数 总大于零总大于零 BB = 1i 11 s = (k: 0k i : bk) i0 = 05.2 基本语句的语义基本语句的语义(5

21、) 循环每迭代一次，循环每迭代一次， 至少减至少减1 wp(“ 1 := 11-i ; s := s+bi ; i := i+1”,11-i 1) = 11-(i+1) 11-i = 10 11 = True c1 wp(“ 1 := 11-i ; S”, 1) 成立成立综上所述，可知综上所述，可知 True 程序程序 Q 正确正确5.2 基本语句的语义基本语句的语义n练习：练习：形式化证明下述算法，算法是 set i to the highest power of 2 that at most n.算法： 0n i := 1; : 0i n ( p : i=2p) : n-i do 2*i

22、n i:= 2*i od R: 0 i n 2*i ( p : i=2p)练习练习形式化地证明如下各个形式化地证明如下各个DO循环的验证项目循环的验证项目n寻找寻找x在在b0.n-1中的位置中的位置i，若，若x不在其中，置不在其中，置 i 的值为的值为 n。 0=n i:=0;Inv. 0=i=n and x b0:i-1 : n-i do in and x bi i := i+1 odQ: 0=i0i,a,b := 1,1,0;Inv. 1=i=n and a=fi and b=fi-1BF: n-ido i=25.3 基本程序的设计方法基本程序的设计方法n主要内容：主要内容：n程序设计的基

23、本原则程序设计的基本原则n选择语句的设计选择语句的设计n循环语句的设计循环语句的设计n循环不变式的设计循环不变式的设计n界函数的设计界函数的设计程序设计的基本原则程序设计的基本原则nPrinciple 1: n一个程序和它的正确性证明应同时设计，并且一个程序和它的正确性证明应同时设计，并且最好以考虑证明为先导。最好以考虑证明为先导。nPrinciple 2：n使用理论来提供正确性的理解，而在适当的地使用理论来提供正确性的理解，而在适当的地方用常识和直观方法。方用常识和直观方法。n但当出现困难和复杂情况时，仍然依据形式理但当出现困难和复杂情况时，仍然依据形式理论作保证。论作保证。n当然一个人只有

24、既有常识又掌握理论才能有效当然一个人只有既有常识又掌握理论才能有效地在形式化和常识之间进行协调。地在形式化和常识之间进行协调。程序设计的基本原则程序设计的基本原则nPrinciple 3：n要了解将用程序来处理的对象的性质。要了解将用程序来处理的对象的性质。nPrinciple 4：n不要忽视任何看起来十分明显的原则，只有通不要忽视任何看起来十分明显的原则，只有通过有意识地运用这些原则才会获得成功。过有意识地运用这些原则才会获得成功。nPrinciple 5：n认识一个原则和应用一个原则是两回事。认识一个原则和应用一个原则是两回事。程序设计的基本原则程序设计的基本原则nPrinciple 6:

25、n在着手编程之前，首先要弄清楚问题是要求在着手编程之前，首先要弄清楚问题是要求“做什么做什么”的，并将其抽象化为前置条件和后置的，并将其抽象化为前置条件和后置条件，即给出精确的程序规范，且勿仓促编码条件，即给出精确的程序规范，且勿仓促编码。nPrinciple 7:n程序设计是一种面向目标的设计活动。即程序程序设计是一种面向目标的设计活动。即程序设计是围绕着目标设计是围绕着目标Q进行的，这意味着进行的，这意味着Q起着比起着比P更重要的作用。更重要的作用。程序设计的基本原则程序设计的基本原则n关于证明和测试数据分析关于证明和测试数据分析n边进行程序设计，边写下有关的测试数据。关边进行程序设计，边

26、写下有关的测试数据。关键在于有效地选择和生成测试数据集；键在于有效地选择和生成测试数据集；n从工程角度看，测试是重要的；从工程角度看，测试是重要的；n但从人员培训的角度看，应该训练程序员具有但从人员培训的角度看，应该训练程序员具有编制正确程序的能力；编制正确程序的能力；n因此，学习和研究形式证明技术是培养能力的因此，学习和研究形式证明技术是培养能力的一种有效的途径一种有效的途径n测试只能证明程序有错，并不能证明程序是正测试只能证明程序有错，并不能证明程序是正确的。确的。n对程序员的科学训练是十分重要的对程序员的科学训练是十分重要的n有人曾做过一个试验：一个题目由一批印度程序员有人曾做过一个试验

27、：一个题目由一批印度程序员来做，其结果惊人地相似；而由一批中国程序员来来做，其结果惊人地相似；而由一批中国程序员来做，编出的程序五花八门。做，编出的程序五花八门。n只有规范的科学的编程，一个大项目才能得到只有规范的科学的编程，一个大项目才能得到有效的管理，其质量才有保证。有效的管理，其质量才有保证。创造性创造性应该发应该发挥在适当的地方。挥在适当的地方。n高效的程序员不应该浪费很多的时间用于程序高效的程序员不应该浪费很多的时间用于程序调试，他们一开始就不要把缺陷引入调试，他们一开始就不要把缺陷引入程序设计的基本原则程序设计的基本原则n关于小程序的设计关于小程序的设计n70年代对小程序设计有很多

28、的研究年代对小程序设计有很多的研究n小程序设计是大规模程序正确性的基础。设一小程序设计是大规模程序正确性的基础。设一个大程序是由个大程序是由n个小程序组成，每个程序正确个小程序组成，每个程序正确的概率是的概率是p，那么整个程序正确的概率，那么整个程序正确的概率P满足：满足： P0; ci为布尔表达式; si为任意语句; ci si是一个带卫哨（Guard）语句, ci为si的卫哨;用 BB表示所有卫哨的析取： BB = c1 c2 . cn选择语句的设计选择语句的设计n选择语句的设计策略：选择语句的设计策略：n对于规范（对于规范（P，Q）n寻找语句寻找语句s1，它执行后能使，它执行后能使Q成立

29、成立n再寻找满足再寻找满足P c1 wp(s1,Q)的条件的条件c1n形成带卫哨语句形成带卫哨语句c1 s1n继续寻找带卫哨语句继续寻找带卫哨语句c2 s2,., cn snn直到直到P c1c2 . cn成立为止。成立为止。选择语句的设计选择语句的设计n选择语句的设计策略：选择语句的设计策略：n对于规范（对于规范（P，Q）n寻找语句寻找语句s1，它执行后，它执行后能使能使Q成立成立n再寻找满足再寻找满足P c1 wp(s1,Q)的条件的条件c1n形成带卫哨语句形成带卫哨语句c1 s1n继续寻找带卫哨语句继续寻找带卫哨语句c2 s2,., cn snn直到直到P c1c2 . cn成立为止。成

30、立为止。定理1（Theorem 1）考虑IF命令，假设谓词P满足： (1) P BB (2) Pci wp(si,Q)则：P wp (IF,Q)选择语句的设计举例选择语句的设计举例n例例1： 写一程序置换写一程序置换y1和和y2之值之值 使得使得y1y2.n解：其规范为：解：其规范为： P： y1=u1 y2=u2 Q: y1 y2 (y1=u1 y2=u2 y1=u2 y2=u1 ) 可能有语句可能有语句 ？ skip ？ y1,y2 := y2,y1 可求得条件分别为：可求得条件分别为： y1 y2 和和 y2 y1对于规范（P，Q）寻找语句s1，它执行后能使Q成立再寻找满足P c1 wp

31、(s1,Q)的条件c1形成带卫哨语句c1 s1继续寻找带卫哨语句c2 s2,., cn sn直到P c1c2 . cn成立为止。n(续续)C1 = y1 y2 C2 = y2 y1 C1 C2 = y1 y2 y2 y1 = True P C1 C2 成立成立n得程序如下：得程序如下： if y1 y2 skip y2 y1 y1,y2 := y2,y1 fi选择语句的设计举例选择语句的设计举例对于规范（P，Q）寻找语句s1，它执行后能使Q成立再寻找满足P c1 wp(s1,Q)的条件c1形成带卫哨语句c1 s1继续寻找带卫哨语句c2 s2,., cn sn直到P c1c2 . cn成立为止。

32、循环语句的设计循环语句的设计n讨论如何从以下条件构造循环程序：讨论如何从以下条件构造循环程序：n前置条件前置条件 Pn结果条件结果条件 Q n循环不变式循环不变式 n界函数界函数 n构造循环程序的理论基础：构造循环程序的理论基础：nDO 的语义的语义n相关定理相关定理n循环程序的验证的方法循环程序的验证的方法循环语句的设计循环语句的设计DO := do c1 s1 c2 s2 cn sn od其中其中,n0, ci 为布尔表达式为布尔表达式, si 为语句为语句, c1 s1为带哨语句为带哨语句循环语句的设计策略循环语句的设计策略n 卫哨先行卫哨先行n 走向终止走向终止设计策略设计策略1：卫哨

33、先行：卫哨先行n 首先寻找循环条件卫哨首先寻找循环条件卫哨cn满足满足 c Q; n 然后形成循环体然后形成循环体n使得界函数使得界函数 的值递减的值递减n并保持不变式并保持不变式 为真。为真。卫哨先行举例卫哨先行举例n例：写一程序，在给定的数组例：写一程序，在给定的数组b0.n-1中，中，n0，寻找给定值，寻找给定值x在数组中出现的位置。若在数组中出现的位置。若x在在b中出现多次，任意找到一次即可；若中出现多次，任意找到一次即可；若x未未在在b中出现，则输出中出现，则输出n：P : n0Q : (0 i 0 Q: s = i: 0in: bi要求循环满足下面的不变式和界函数要求循环满足下面的

34、不变式和界函数不变式不变式 : 0i n (s = j: 0j0 x20Q: y1 = y2 = gcd(x1,x2) : 0y1 0y2 gcd(y1,y2)=gcd(x1,x2 ) : y1+y2走向终止举例走向终止举例n解：解： 最大公约数的性质：最大公约数的性质： 对任意的对任意的0y1y1 y1 := y1-y2 C2：y1y2走向终止举例走向终止举例寻找导致循环终止（即递减）的语句si寻找保持不变式的相应条件ci形成带哨语句 ci si重复这个过程，直到形成足够多的带哨语句足以证明 BB Q 成立为止。Q:ny1=y2=gcd(x1,x2):n0y1 00 x20y1,y2 :=

35、x1,x2 界函数界函数 ：y1+y2do y1y2 y1 := y1-y2od y1=y2Q: y1 = y2 = gcd(x1,x2)走向终止举例走向终止举例不变式与循环语句不变式与循环语句n程序语句应使界函数递减程序语句应使界函数递减n界函数以什么样得轨迹减小决定了该界函数以什么样得轨迹减小决定了该程序的设计，而这样的轨迹早已蕴涵程序的设计，而这样的轨迹早已蕴涵在在 中了。中了。n因此说，一个不变式代表了一个循环因此说，一个不变式代表了一个循环语句，不同的不变式就可能得出不同语句，不同的不变式就可能得出不同的循环语句。的循环语句。不变式的构造不变式的构造u一般情况下，一般情况下， BB

36、= Q ，因此，因此Q 。u在循环开始时，在循环开始时， 为真，因此为真，因此IS 。ISQ气球理论气球理论(The Balloon Theory)ISQn把把Q看成一个瘪了气的气球。看成一个瘪了气的气球。n逐渐放宽对逐渐放宽对Q的限制，即削弱的限制，即削弱Q，即将气，即将气球吹大球吹大n直至包含循环的初始状态直至包含循环的初始状态气球理论气球理论(The Balloon Theory)ISQn把把Q看成一个瘪了气的气球。看成一个瘪了气的气球。n逐渐放宽对逐渐放宽对Q的限制，即削弱的限制，即削弱Q，即将气，即将气球吹大球吹大n直至包含循环的初始状态直至包含循环的初始状态气球理论气球理论(The

37、 Balloon Theory)ISQn把把Q看成一个瘪了气的气球。看成一个瘪了气的气球。n逐渐放宽对逐渐放宽对Q的限制，即削弱的限制，即削弱Q，即将气，即将气球吹大球吹大n直至包含循环的初始状态直至包含循环的初始状态气球理论气球理论(The Balloon Theory)ISnn-110.Qn把把Q看成一个瘪了气的气球。看成一个瘪了气的气球。n逐渐放宽对逐渐放宽对Q的限制，即削弱的限制，即削弱Q，即将气，即将气球吹大球吹大n直至包含循环的初始状态直至包含循环的初始状态气球理论气球理论(The Balloon Theory)n n， n-1，.， 1 ， 0描述了整个吹气的过程描述了整个吹气的

38、过程，一旦到达边界，就考虑如何泄气使，一旦到达边界，就考虑如何泄气使 回到回到Q。这个过程就是设计一个循环，每迭代一步就。这个过程就是设计一个循环，每迭代一步就漏气一次，最后收缩到漏气一次，最后收缩到Q的动作。的动作。n吹气的过程是设计吹气的过程是设计 的过程，而漏气的过程是的过程，而漏气的过程是设计循环体的过程。因此，将设计不变式的方设计循环体的过程。因此，将设计不变式的方法归结为削弱谓词法归结为削弱谓词Q的过程。的过程。ISnn-110.Q构造不变式方法构造不变式方法1. 削弱削弱Q就就 ：n删除删除Q的一个合取分量的一个合取分量n替换替换Q中的常量为变量中的常量为变量n扩大扩大Q中变量的

39、变化范围中变量的变化范围2. 联合联合P和和Q就就 就：靠近、趋向就：靠近、趋向适合于输入变量的值不因程序的执行而变化的情况。适用于输入变量的值因程序的执行而变化的情况。削弱削弱Q就就 - 删除删除Q的合取分量的合取分量n策略：策略：n假定假定Q是一个合取式，可以试着删除是一个合取式，可以试着删除Q的某个的某个合取分量而构造合取分量而构造 n而被删除的分量的否定式作为循环条件（卫而被删除的分量的否定式作为循环条件（卫哨）。哨）。nQ: AB Cn删除删除B构造构造 ： ACn B作为循环条件（卫哨）作为循环条件（卫哨）nQ: AB Cn删除删除C构造构造 ： ABn C作为循环条件（卫哨）作为

40、循环条件（卫哨）削弱削弱Q就就 - 删除删除Q的合取分量的合取分量n例例1：写一个程序，对给定的整数：写一个程序，对给定的整数x0，求满足如下的关系的，求满足如下的关系的r： Q： 0 r2 x (r+1) 2 即，即，r是不超过是不超过sqrt(x)的最大整数。的最大整数。削弱削弱Q就就 - 删除删除Q的合取分量的合取分量解：解：P ： x 0Q可写成：可写成：0 r2 r2 x x (r+1) 2从从Q中删除中删除x (r+1) 2，得一个可能得不变式，得一个可能得不变式 ： ： 0 r2 r2 x 由由P， 得初始化语句：得初始化语句： r:=0, 使得使得P r:=0 成立。成立。循环

41、条件：循环条件： c = （x (r+1) 2 ） c =（ x (r+1) 2 ) 得程序：得程序： r:=0 do (r+1) 2 x ? od界函数界函数 ： sqrt（x）- r循环体语句：循环体语句： r:=r+1;削弱削弱Q就就 - 用变量替换常量用变量替换常量n策略：策略：n用变量替换用变量替换Q中的有关常量，且给中的有关常量，且给出此变量的适当变化范围，以此削出此变量的适当变化范围，以此削弱弱Q而构造而构造 。削弱削弱Q就就 - 用变量替换常量用变量替换常量n例例1：平台问题：对给定的有序：平台问题：对给定的有序( )）数组）数组b0:n-1，数，数组的平台是一串相等值的序列，

42、要求写一个程序，存组的平台是一串相等值的序列，要求写一个程序，存b的的最长平台的长度于变量最长平台的长度于变量L中。即此程序执行后中。即此程序执行后Q成立：成立： Q: L 是是b0:n-1的最长平台的长度的最长平台的长度n解：解： b是有序的，是有序的， 区间区间bj,k是平稳的是平稳的 (bj=bk) Q: ( k:0 kn-L: bk=bk+L-1) ( i: 0 i0 ordered(b0:n-1) : 1 i n L 是是b0:i-1的最长平台的长度的最长平台的长度 界函数界函数 ： n-i削弱削弱Q就就 - 用变量替换常量用变量替换常量卫哨：卫哨： i n循环初值：循环初值： i,L :=1,1; 可使可使P i,L :=1,1; 成立成立i:=i+1 可使可使 递减，递减， 条件：条件： bi bi-L反之，反之， 当当bi = bi-L时，时，L:=L+1;i:=i+1得程序：得程序： i,L :=1,1;do i