[工学]PM讲义-第5章最弱前置谓词和程序语言的语义.ppt

五章、 最弱前置谓词和程序语言的语义,前言 引进最弱前置谓词（Weakest Pre-predicate）的概念， 并用它来定义一个小程序语言L。该语言的主要成分： 赋值语句、 选择语句、 循环语句， 数据类型只有整型和布尔型,5.1 最弱前置谓词,1.定义：假定S是一个语句，Q是一个谓词，它描述S执行后所确定的某种关系。从S和Q定义另外一个谓词，记为 wp(S,Q),它表示： “所有这样的状态的集合，S从其中任一状态开始执行必将在有限的时间内终止于满足Q的状态”。 - S - wp(S,Q) Q ,5.1 最弱前置谓词,我们称 wp(S,Q) 是语句S关于Q的最弱前置谓词。 “最弱”反映在“所有”一词之中，外延最大，内涵自然最弱。,5.1 最弱前置谓词,例1. 假设S是赋值语句 i := i+1; Q为 i10 则： 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) = FALSE,5.1 最弱前置谓词,wp(S,Q)与 P S Q： P S Q表示 “若S的执行开始于一个满足P的状态，则S的执行必在有限的时间内终止于一个满足Q的状态” wp(S,Q)表示“所有这样的状态的集合，S从其中任一状态开始执行必将在有限的时间内终止于满足Q的状态” 因此： P S Q ( P wp(S,Q),5.2 基本语句的语义前言,前言： 用wp定义一个小程序设计语言L，此语言的表达式只有整型和布尔型两类，说明语句采用类Pascal的形式，其基本执行语句有空语句（Skip）、赋值语句、选择语句、循环语句。 令记号“=df” 为定义符，读做“定义为”,5.2 基本语句的语义-空语句,1.空语句（Skip） Skip语句表示什么事都不做，相当于空语句。其定义如下： 定义1： wp(skip,Q) =df Q,5.2 基本语句的语义-赋值语句,2. 赋值语句 1）简单变量赋值 赋值形式： y := e 其中y为简单变量，e为表达式；y，e必须相同类型。这个语句在某种状态下执行意味着：首先在此状态下计算出e的值，然后将此值存放在以y为名字的存储单元中，即用e的值代替y的值。,5.2 基本语句的语义-赋值语句,定义2：wp(“y := e”,Q) =df domain(e) 其中， domain(e) 是一个谓词，表示所有使e可求值的状态集。 在多数情况下， domain(e) 总是成立，故常省略它，只写： wp(“y := e”,Q) =df,5.2 基本语句的语义,例1： 例2： 例3： 例4：,5.2 基本语句的语义,例1： 例2： 例3： 例4：,5.2 基本语句的语义 多个简单变量的同时赋值,2)多个简单变量的同时赋值,例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 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=u1,5.2 基本语句的语义选择语句,形式： IF := if c1 s1; c2 s2; cn sn; fi 其中，n0; ci为布尔表达式; si为任意语句; ci si是一个带卫哨（Guard）语句, ci为si的卫哨; 用 BB表示所有卫哨的析取： BB = c1 c2 . cn,IF语句的执行过程： 首先计算每个ci， 若所有ci都不为真，或 有某个ci无定义则执行中断（abort），否则，执行任一个其值为真的ci所对应的si。 当si执行完毕后，整个IF就执行完了。,5.2 基本语句的语义,定义6： wp(IF,Q) =df domain(BB) BB c1wp(s1,Q) c2wp(s2,Q) . cnwp(sn,Q) =df domain(BB) (j : 1j n : cj) (i : 1i n : ci wp(si,Q) ),5.2 基本语句的语义,例：令IF为 if x=0 y := x x=0 x=0 wp(“y := x”, y = abs(x) x=0 x= abs(x) x=0 (-x= abs(x) = true,wp(IF,Q)=df domain(BB) BB c1wp(s1,Q) c2wp(s2,Q) . cnwp(sn,Q),定理1（Theorem 1）,考虑IF命令，假设谓词P满足： (1) P BB (2) P ci wp（si,Q），0 i n 则： P wp（IF，Q）,定理1（举例）,例：考察下列的选择语句S： if x y x,y :=y,x; x=y skip fi 已知P=True，Q = (x=y) 要证明 P S Q,定理1（举例）,由定理可知，P wp(S,Q)成立. 因此说明例中的选择语句S对给定的输入/输出断言P和Q是正确的.,证明：,5.2 基本语句的语义循环语句,5. 循环语句 一般形式: DO := do c1 s1 c2 s2 cn sn od 其中,n0, ci 为布尔 表达式, si 为语句, c1 s1为带哨语句,DO 语句的执行如下: 首先计算每个ci, 若有某个ci无定义,则执行失败(流产) 。 若所有ci均为假,则执行终止, 否则执行任意其值为真的ci所对应的si. 重复这个过程直至执行终止或失败. DO语句等价于: do BB IF od,5.2 基本语句的语义,为给出DO语句的形式语义, 先定义两个符号 令: H0(Q) = BBQ 它是这样的一个状态集合: DO从其中任一状态开始执行不经过任何迭代(0次迭代)即终止,且终止时Q为真。 定义一个谓词Hk(Q) , k0. 它表示这样的一个状态集合: DO从其中任一状态开始执行,最多经过k次迭代而终止,且终止时Q为真。因此,它可以表示为: Hk(Q) = H0(Q) wp(IF, Hk-1(Q) ), k0,5.2 基本语句的语义,定义一个谓词Hk(Q) , k0. 它表示这样的一个状态集合: DO从其中任一状态开始执行,最多经过k次迭代而终止,且终止时Q为真。因此,它可以表示为: Hk(Q) = H0(Q) wp(IF, Hk-1(Q) ), k0 H1(Q) = H0(Q) wp(IF, H0(Q) ) H2(Q) = H0(Q) wp(IF, H1(Q) ),5.2 基本语句的语义,wp(DO, Q)可以定义为这样一个状态集合: DO从其中任一状态开始执行,必须经过有限次迭代后终止于满足Q的状态。于是: 定义7: wp(DO, Q) =df ( k: k0 : Hk(Q) ) 由于Hk(Q) 的构造甚为麻烦。因此, wp(DO, Q) 的定义实际上不便于使用, 但可用于证明一个有用的定理。,5.2 基本语句的语义不变式,不变式 ： 不必要求一定得到DO语句的最弱前置条件wp(DO,Q)，可以寻找一个稍强的前置条件，它满足：在DO执行之前成立，而且每经过一次迭代后也仍然保持成立，并且还能够保证BB Q 为真。因此，用作为循环DO对于Q的前置条件。即寻找满足下列形式的 ： do BB BB IF od; BB Q 因为 在循环的每轮迭代的执行前后均保持为真，因此称为该循环的一个不变式（Invariant）,5.2 基本语句的语义界函数,界函数： 为说明循环的终止性，引入一个整型函数，它是程序变量的函数， 用以指明循环至多执行 次迭代。它满足： 的值随迭代次数的增加而递减，每次迭代的值至少递减1，且: 只要能够继续迭代， 的值就一定保持0 因此，只要表明存在这样的函数，循环就必定能够终止， 称 为循环的界函数（Bound Function）,5.2 基本语句的语义,例1：计算数组b0:10元素的和，并将结果存于变量s中的程序为： i := 1; s := b0; do i11 s := s+bi ; i := i+1; od Q: s = k: 0k 11 : bk 令： 为 1i 11 s = (k: 0k i : bk) 为 11-i 可以证明是个循环不变式，且 i11 Q，而 =11-i 表示循环尚需进行的迭代次数。,5.2 基本语句的语义,定理2（不变式定理） 考虑一个DO循环，令谓词 满足： （1） ci wp(si, ), 1 i n 令整数函数 满足（ 1是新标识符） （2） BB 0 （3） ci wp(“1 := ; si”, 1 ), 1 i n 则： wp(DO, BB ) 说明:（1）说明 是循环不变式；（2）说明只要循环不终止，函数总大于零；（3）指出循环每迭代一次， 至少减1； 结论则说明若前置条件为真，则DO的执行必终止，且终止时 BB 为真。,5.2 基本语句的语义 关于PDOQ的验证项目,关于PDOQ的验证项目 根据定理2，为证明PDOQ，关键在于寻找谓词 和界函数，使得下面的项目一一成立： 在循环执行前为真， 对每个 i，1i n， ci si BB Q BB 0 对每个 i，1in， ci 1 := ; si”1 形式化注释如下：,5.2 基本语句的语义,P 不变式 界函数 do c1 s1 c2 s2 cn sn od BB 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 : bk,5.2 基本语句的语义,证明： (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) 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 0 = 0,5.2 基本语句的语义,(5) 循环每迭代一次， 至少减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 基本语句的语义,练习： 形式化证明下述算法，算法是 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 n i:= 2*i od R: 0 i n 2*i (p : i=2p),练习,形式化地证明如下各个DO循环的验证项目 寻找x在b0n-1中的位置i，若x不在其中，置 i 的值为 n。 0=n i:=0; Inv. 0=i=n and xb0:i-1 : n-i do in and x bi i := i+1 od Q: 0=in and x=bi or i=n and x b0:n-1,练习,2 寻找第n个Fibinacci数 0,1,1,2,3,5 n0 i,a,b := 1,1,0; Inv. 1=i=n and a=fi and b=fi-1 BF: n-i do in i,a,b := i+1,a+b,a od Q: a=fn,0, n=0; f(n) = 1, n=1 fn-1+fn-2, n=2,5.3 基本程序的设计方法,主要内容： 程序设计的基本原则 选择语句的设计 循环语句的设计 循环不变式的设计 界函数的设计,程序设计的基本原则,Principle 1: 一个程序和它的正确性证明应同时设计，并且最好以考虑证明为先导。 Principle 2： 使用理论来提供正确性的理解，而在适当的地方用常识和直观方法。 但当出现困难和复杂情况时，仍然依据形式理论作保证。 当然一个人只有既有常识又掌握理论才能有效地在形式化和常识之间进行协调。,程序设计的基本原则,Principle 3： 要了解将用程序来处理的对象的性质。 Principle 4： 不要忽视任何看起来十分明显的原则，只有通过有意识地运用这些原则才会获得成功。 Principle 5： 认识一个原则和应用一个原则是两回事。,程序设计的基本原则,Principle 6: 在着手编程之前，首先要弄清楚问题是要求“做什么”的，并将其抽象化为前置条件和后置条件，即给出精确的程序规范，且勿仓促编码。 Principle 7: 程序设计是一种面向目标的设计活动。即程序设计是围绕着目标Q进行的，这意味着Q起着比P更重要的作用。,程序设计的基本原则,关于证明和测试数据分析 边进行程序设计，边写下有关的测试数据。关键在于有效地选择和生成测试数据集； 从工程角度看，测试是重要的； 但从人员培训的角度看，应该训练程序员具有编制正确程序的能力； 因此，学习和研究形式证明技术是培养能力的一种有效的途径 测试只能证明程序有错，并不能证明程序是正确的。,对程序员的科学训练是十分重要的 有人曾做过一个试验：一个题目由一批印度程序员来做，其结果惊人地相似；而由一批中国程序员来做，编出的程序五花八门。 只有规范的科学的编程，一个大项目才能得到有效的管理，其质量才有保证。创造性应该发挥在适当的地方。 高效的程序员不应该浪费很多的时间用于程序调试，他们一开始就不要把缺陷引入,程序设计的基本原则,关于小程序的设计 70年代对小程序设计有很多的研究 小程序设计是大规模程序正确性的基础。设一个大程序是由n个小程序组成，每个程序正确的概率是p，那么整个程序正确的概率P满足： Ppn.,选择语句的设计,形式： IF := if c1 s1; c2 s2; cn sn; fi 其中，n0; ci为布尔表达式; si为任意语句; ci si是一个带卫哨（Guard）语句, ci为si的卫哨; 用 BB表示所有卫哨的析取： BB = c1 c2 . cn,选择语句的设计,选择语句的设计策略： 对于规范（P，Q） 寻找语句s1，它执行后能使Q成立 再寻找满足P c1 wp(s1,Q)的条件c1 形成带卫哨语句c1 s1 继续寻找带卫哨语句c2 s2,., cn sn 直到P c1c2 . cn成立为止。,选择语句的设计,选择语句的设计策略： 对于规范（P，Q） 寻找语句s1，它执行后能使Q成立 再寻找满足P c1 wp(s1,Q)的条件c1 形成带卫哨语句c1 s1 继续寻找带卫哨语句c2 s2,., cn sn 直到P c1c2 . cn成立为止。,定理1（Theorem 1） 考虑IF命令，假设谓词P满足： (1) P BB (2) Pci wp(si,Q) 则：P wp (IF,Q),选择语句的设计举例,例1： 写一程序置换y1和y2之值 使得y1y2. 解：其规范为： 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(s1,Q)的条件c1 形成带卫哨语句c1 s1 继续寻找带卫哨语句c2 s2,., cn sn 直到P c1c2 . cn成立为止。,(续) C1 = y1 y2 C2 = y2 y1 C1 C2 = y1 y2 y2 y1 = True P C1 C2 成立 得程序如下： 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成立为止。,循环语句的设计,讨论如何从以下条件构造循环程序： 前置条件 P 结果条件 Q 循环不变式 界函数 构造循环程序的理论基础： DO 的语义 相关定理 循环程序的验证的方法,循环语句的设计,DO := do c1 s1 c2 s2 cn sn od 其中,n0, ci 为布尔表达式, si 为语句, c1 s1为带哨语句,循环语句的设计策略,卫哨先行 走向终止,设计策略1：卫哨先行,首先寻找循环条件卫哨c 满足 c Q; 然后形成循环体 使得界函数 的值递减 并保持不变式 为真。,卫哨先行举例,例：写一程序，在给定的数组b0n-1中，n0，寻找给定值x在数组中出现的位置。若x在b中出现多次，任意找到一次即可；若x未在b中出现，则输出n： P : n0 Q : (0 i n x=bi) or (i=n xb) : “x不在已搜索过的区域b0:i-1中” 0 i n xb0：i-1 : n-i,解： （1）先考虑循环的初值： 显然 i:=0; 使得 P wp(“i:=0 ”, )成立 （2）寻找循环条件c，使得 c Q成立，显然如下的c 能够满足要求： c (inx=bi ) i=n c (x bi i n),卫哨先行举例,首先寻找循环条件卫哨c 满足 c Q; 然后形成循环体 使得界函数 的值递减 并保持不变式 为真。,(3)构造循环体：使界函数递减，并保持不变式为真，令： i := i+1; 可以验证： c wp(“i:=i+1”, ) 成立 于是，得程序为： True i:=0; do (x bi i n) c i:=i+1 od (x=bi i=n) Q,卫哨先行举例,首先寻找循环条件卫哨c 满足 c Q; 然后形成循环体 使得界函数 的值递减 并保持不变式 为真。,求数组b0n-1的和。 已知： P: n0 Q: s = i: 0in: bi 要求循环满足下面的不变式和界函数 不变式 : 0i n (s = j: 0jn: bj) 界函数 ：n-i,卫哨先行练习,寻找导致循环终止（即递减）的语句si 寻找保持不变式的相应条件ci 形成带哨语句 ci si 重复这个过程，直到形成足够多的带哨语句足以证明 BB Q 成立为止。 卫哨先行 首先寻找循环条件卫哨c 然后形成循环体,设计策略2：走向终止,例3：计算任意两个正整数x1,x2的最大公约数gcd(x1,x2)。 假定不用乘除。 令有初始语句： y1,y2 := x1,x2; 则： P： x10 x20 Q: y1 = y2 = gcd(x1,x2) : 0y1 0y2 gcd(y1,y2)=gcd(x1,x2 ) : y1+y2,走向终止举例,解： 最大公约数的性质： 对任意的0y1 y1 := y1-y2 C2：y1y2,走向终止举例,寻找导致循环终止（即递减）的语句si 寻找保持不变式的相应条件ci 形成带哨语句 ci si 重复这个过程，直到形成足够多的带哨语句足以证明 BB Q 成立为止。,Q: y1=y2=gcd(x1,x2) : 0y1 0y2 gcd(y1,y2)=gcd(x1,x2 ),得到如下程序： x10 x20 y1,y2 := x1,x2 界函数：y1+y2 do y1y2 y1 := y1-y2 od y1=y2 Q: y1 = y2 = gcd(x1,x2),走向终止举例,不变式与循环语句,程序语句应使界函数递减 界函数以什么样得轨迹减小决定了该程序的设计，而这样的轨迹早已蕴涵在中了。 因此说，一个不变式代表了一个循环语句，不同的不变式就可能得出不同的循环语句。,不变式的构造,一般情况下， BB = Q ，因此Q 。 在循环开始时， 为真，因此IS 。,IS,Q,气球理论(The Balloon Theory),IS,Q,把Q看成一个瘪了气的气球。 逐渐放宽对Q的限制，即削弱Q，即将气球吹大 直至包含循环的初始状态,气球理论(The Balloon Theory),IS,Q,把Q看成一个瘪了气的气球。 逐渐放宽对Q的限制，即削弱Q，即将气球吹大 直至包含循环的初始状态,气球理论(The Balloon Theory),IS,Q,把Q看成一个瘪了气的气球。 逐渐放宽对Q的限制，即削弱Q，即将气球吹大 直至包含循环的初始状态,气球理论(The Balloon Theory),IS,n,n-1,1,0,.,Q,把Q看成一个瘪了气的气球。 逐渐放宽对Q的限制，即削弱Q，即将气球吹大 直至包含循环的初始状态,气球理论(The Balloon Theory),n， n-1，.， 1 ，0描述了整个吹气的过程，一旦到达边界，就考虑如何泄气使 回到Q。这个过程就是设计一个循环，每迭代一步就漏气一次，最后收缩到Q的动作。 吹气的过程是设计的过程，而漏气的过程是设计循环体的过程。因此，将设计不变式的方法归结为削弱谓词Q的过程。,IS,n,n-1,1,0,.,Q,构造不变式方法,1. 削弱Q就： 删除Q的一个合取分量 替换Q中的常量为变量 扩大Q中变量的变化范围 2. 联合P和Q就 就：靠近、趋向,适合于输入变量的值不因程序的执行而变化的情况。 适用于输入变量的值因程序的执行而变化的情况。,削弱Q就- 删除Q的合取分量,策略： 假定Q是一个合取式，可以试着删除Q的某个合取分量而构造 而被删除的分量的否定式作为循环条件（卫哨）。 Q: AB C 删除B构造： AC B作为循环条件（卫哨） Q: AB C 删除C构造： AB C作为循环条件（卫哨）,削弱Q就- 删除Q的合取分量,例1：写一个程序，对给定的整数x0，求满足如下的关系的r： Q： 0 r2 x (r+1) 2 即，r是不超过sqrt(x)的最大整数。,削弱Q就- 删除Q的合取分量,解： P ： x 0 Q可写成：0 r2 r2 x x (r+1) 2 从Q中删除x (r+1) 2，得一个可能得不变式： ： 0 r2 r2 x 由P， 得初始化语句： r:=0, 使得P r:=0 成立。 循环条件： 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就- 用变量替换常量,策略： 用变量替换Q中的有关常量，且给出此变量的适当变化范围，以此削弱Q而构造。,削弱Q就- 用变量替换常量,例1：平台问题：对给定的有序( )）数组b0:n-1，数组的平台是一串相等值的序列，要求写一个程序，存b的最长平台的长度于变量L中。即此程序执行后Q成立： Q: L 是b0:n-1的最长平台的长度 解： b是有序的， 区间bj,k是平稳的 (bj=bk) Q: (k:0 k0 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 n if bi bi-L i:=i+1 ; bi = bi-L L:=L+1;i:=i+1; fi od,削弱Q就- 用变量替换常量,例2：已知 n0, 求整数数组 b0:n-1的和存于S中。有： P: n0 Q: S = j: 0jn : bj 以变量替换常量： ：0i n S =(j: 0ji : bj) : n-i,削弱Q就- 用变量替换常量,例3：写一个程序，对给定的整数n0，求a，使R为真： R： a2 n (a+1)2 设计不变式： 用b替换（a+1），并令an b:=d; fi od,削弱Q就-扩大变量的取值范围,策略：扩大Q中某些变量的取值范围 ，削弱Q构造。 例：令f0:n,g0:n,h0:n是三个固定的单调上升的整数数组（n0）。已知他们存在公共值。写一程序，求最小公共值在f,g,h中的位置。 解：P: n0 令i0,j0,k0满足：fi0=gj0=hk0 ijk: i fi gj hk i0,j0,k0即是最小公共值所处的位置，因此执行后满足： Q: i=i0 j=j0 k=k0 : 0 i i0 0 j j0 0 k k0 : i0-i+j0-j+k0-k,削弱Q就-扩大变量的取值范围,程序： 初始语句： i,j,k:=0,0,0; do figj fihk i := i+1; gjhk