PM-Chap6小程序设计的基本方法.ppt

第六章 程序设计基本方法,主要内容： 引言-程序设计的基本原则 选择语句的设计 循环语句的设计 循环不变式的设计 界函数的设计,6.1 程序设计的基本原则,Principle 1: A program and its proof should be developed hand in hand, with the proof usually leading the way, 一个程序和它的正确性证明应同时设计，并且最好以考虑证明为先导。 Principle 2：使用理论来提供正确性的理解，而在适当的地方用常识和直观方法，但当出现困难和复杂情况时，仍然依据形式理论作保证。当然一个人只有既有常识又掌握理论才能有效地在形式化和常识之间进行协调，前者是程序员一直在使用。,6.1 程序设计的基本原则,Principle 3：要了解将用程序来处理的对象的性质。 例：假设有一袋装有黑白两色棋子。每次从袋中任取两粒子，若它们同色，则丢掉这两粒子，然后再补进一只黑子，否则丢掉黑子，放回白子。连续执行这一步骤，直至袋中只剩下一子为止。试问最后这一子是黑或白？编一程序回答此问题。,6.1 程序设计的基本原则,Principle 4：不要忽视任何看起来十分明显的原则，只有通过有意识地运用这些原则才会获得成功。 Principle 5：认识一个原则和应用一个原则是两回事。 Ideas may be simple and easy to understand, but their application may require efforts. Recognizing a principle and applying it are two different things. Principle 6:在着手编程之前，首先要弄清楚问题是要求“做什么”的，并将其抽象化为前置条件和后置条件，即给出精确的程序规范，且勿仓促编码。,6.1 程序设计的基本原则,Principle 7: 程序设计是一种面向目标的设计活动。即程序设计是围绕着目标Q进行的，这意味着Q起着比P更重要的作用。 关于证明和测试数据分析 边进行程序设计，边写下有关的测试数据。关键在于有效地选择和生成测试数据集； 从工程角度看，测试是重要的； 但从人员培训的角度看，应该训练程序员具有编制正确程序的能力； 因此，学习和研究形式证明技术是培养能力的一种有效的途径 测试只能证明程序有错，并不能证明程序是正确的。,Test,对程序员的科学训练是十分重要的，有人曾做过一个试验：一个题目由一批印度的程序员和中国的程序员来做，结果如何？ 由一批印度程序员来做，其结果惊人地相似； 而由一批中国程序员来做，编出的程序五花八门。 只有规范的科学的编程，一个大项目才能得到有效地管理，其质量才有保证。创造性应该发挥在适当的地方。,6.1 程序设计的基本原则,高效的程序员不应该浪费很多的时间用于程序调试，他们一开始就不要把缺陷引入 “程序测试是表明故障的非常有效的方法，但对于证明没有故障，调试是很无能为力的” 关于小程序的设计 70年代对小程序设计有很多的研究 小程序设计是大规模程序正确性的基础。设一个大程序是由n个小程序组成，每个程序正确的概率是p，那么整个程序正确的概率P满足： Ppn.,6.2 选择语句的设计,选择语句的设计策略： 对于规范（P，Q），寻找语句s1，它执行后可能确立Q，再寻找满足Pc1 wp(s1,Q)的布尔条件c1，形成带卫哨语句 c1 s1. 继续寻找这样的带哨语句 c2s2,., cn sn, 直到P c1c2 . cn成立为止。 例1：写一程序置换y1和y2之值使得y1y2. 解：其规范为： P：y1=u1 y2=u2 Q: y1y2(y1=u1y2=u2y1=u2y2=u1) 可能有语句 ？ skip ? y1,y2 := y2,y1 可求得条件分别为： y1 y2 和 y2 y1,6.2 选择语句的设计,(续) y1 y2 y2 y1 = True P y1 y2 y2 y1 成立 得程序如下： if y1 y2 skip y2 y1 y1,y2 := y2,y1 fi,6.3循环语句的设计,引言： 讨论如何从前置条件P和结果条件Q，循环不变式和界函数构造循环程序。关于DO 的语义以及相关定理和循环程序的验证的方法是循环程序构造的理论基础。,6.3循环语句的设计,设计策略1（卫哨先行）： 首先寻找循环条件卫哨c，满足 c Q; 然后形成循环体，使得界函数 的值递减，并保持不变式为真。 例：写一程序，在给定的数组b0n-1中，n0,寻找既 定值x. 若x在b中出现多次，任意找到一次即可。有： 解：P : n0 Q : (0 i n x=bi) or (i=n xb) 不变式 ： “x不在已搜索过的区域b0:i-1中” 0 i n xb0：i-1 界函数 ： n-i,6.3循环语句的设计,解： （1）先考虑循环的初值： 显然 i:=0 使得 ; P wp(“i:=0 ”, )成立 （2）寻找循环条件c，使得 c Q成立，显然如下的c 能够满足要求： c (inx=bi ) i=n c (x bi i n) (3)构造循环体：使界函数递减，并保持不变式为真，令 i := i+1 可以验证： c wp(“i:=i+1”, ) 成立 于是，得程序为：,6.3循环语句的设计,True i:=0; do (x bi i n) c i:=i+1 od (x=bi i=n) Q,6.3循环语句的设计,练习： 求数组b0n-1的和。已知： P: n0 Q: s = i: 0in: bi 要求循环满足下面的不变式和界函数 不变式 : 0i n (s = j: 0ji: bj) 界函数 ：n-i,6.3循环语句的设计,设计策略2：走向终止 寻找导致循环终止（即递减）的语句Si，寻找保持不变式的相应条件ci，形成带哨语句 ci si. 重复这个过程，直到形成足够多的带哨语句足以证明 BB Q 成立为止。 例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,6.3循环语句的设计,解： 最大公约数的性质：对任意的0y1 类似有 ： y1 := y1-y2 条件： y1y2 得程序如下：,6.3循环语句的设计,x10 x20 y1,y2 := x1,x2 界函数：y1+y2 do y1y2 y1 := y1-y2 od y1=y2 Q: y1 = y2 = gcd(x1,x2),x10 x20 y1,y2 := x1,x2 界函数：y1+y2 do y1 y2 y1 y2 if y1y2 y1 := y1-y2 fi od y1=y2 Q: y1 = y2 = gcd(x1,x2),6.3循环语句的设计,例2：检索一个二维数组： P: order(b0:m-1,0:n-1) n0 m 0 Q: (0im 0 jn x=bi,j xb) 即给出一个有序的二维数组（有可能为空）查找x 0 j n-1 ： 0i m 0 j n x不在这里 i m-1 : (m-i)*n-j+m-i (他表明了未搜索的值的个数和行的个数之和),思考： 中没有m-i 是否可以？,6.3循环语句的设计,解：初始化语句 i,j :=0,0; 显然 j:=j+1, i:=i+1 都可以使得 减小，由 c1 wp(“j:=j+1”, ) 可得： im j n x bi,j j:=j+1 是相应的条件c1 但： c1 Q 而： i:=i+1 只有在 im j=n 时才能执行，因此有： i m j=n i,j := i+1,0 程序： i,j :=0,0; do im j n x bi,j j:=j+1 im j=n i,j := i+1,0 od,6.3循环语句的设计,讨论： 程序语句应使界函数递减，界函数以什么样的轨迹减小决定了该程序的设计，而界函数的轨迹早已蕴涵在中了。 因此说，一个不变式代表了一个循环语句，不同的不变式就可能得出不同的循环语句。,Review,DO循环的验证项目 程序设计的基本原则 选择语句的设计原则：语句-条件 循环语句的设计策略：卫哨先行、走向终止,6.4 不变式的构造,构造不变式有两类方法： 1. 削弱Q构造： 删除 Q 的一个合取分量 替换 Q 中的常量为变量 扩大 Q 中变量的变化范围等 2. 联合P和Q构造,适合于输入变量的值不因程序的执行而变化的情况 适用于输入变量的值因程序的执行而变化的情况。,6.4 不变式的构造,气球理论（The Balloon Theory） 一般情况下， BB = Q , 因此Q . 把Q看成一个瘪了气的气球。逐渐放宽对Q的限制，即削弱Q，即将气球吹大，直至包含循环的初始状态（这个初始状态顶多几条简单赋值和选择语句可以得到）,IS,Q,初始状态,n,n-1,1,0,.,6.4 不变式的构造,n， n-1，.， 1 ，0描述了整个吹气的过程，一旦到达边界，就考虑如何泄气使 回到Q。这个过程就是设计一个循环，每迭代一步就漏气一次，最后收缩到Q的动作。 吹气的过程是设计的过程，而漏气的过程是设计循环体的过程。因此，将设计不变式的方法归结为削弱谓词Q的过程。,6.4 不变式的构造,2. 削弱Q就- 删除Q的合取分量 （AB C可以削弱为AB 或AC ） 策略：假定Q是一个合取式，可以试着删除其某个合取分量而构造，而被删除的分量的否定式作为循环条件（卫哨）c。 例1：写一个程序，对给定的整数x0，求满足如下的关系的r： Q： 0 r2 x (r+1) 2 即，r是不超过sqrt(x)的最大整数。,6.4 不变式的构造,解： 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;,6.4 不变式的构造,3. 削弱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,6.4 不变式的构造,卫哨： 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,6.4 不变式的构造,例2：已知 n0, 求整数数组 b0:n-1的和存于S中。有： P: n0 Q: S = j: 0jn : bj 以变量替换常量： ：0i n S =(j: 0ji : bj) : n-i,6.4 不变式的构造,例3：写一个程序，对给定的整数n0，求a，使R为真： R： a2 n (a+1)2 设计不变式： 用b替换（a+1），并令an b:=d; fi od,6.4 不变式的构造,4. 削弱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 即是最小公共值所处的位置，执行后满足： Q： i=i0 j=j0 k=k0 ：0 i i0 0 j j0 0 k k0 : i0-i+j0-j+k0-k,6.4 不变式的构造,程序： 初始语句： i,j,k:=0,0,0; do figj fihk i := i+1; gjhkgjfi j := j+1; hkfihkgj k := k+1; od,6.4 不变式的构造,讨论： BB = figj fihk gjhkgjfi hkfihkgj BB = （fi=gj=hk） 而 （ figj gjhk hkfi） = （fi=gj=hk） 只要每个条件的第一个分量也是正确的。,6.4 不变式的构造,5. 联合P和Q构造 若输入变量的值在程序执行过程中必须变化，则需要联合P和Q而构造。 例：对给定的m,n0，把数组b0:n-1每个元素的值变为m*i+bi,即： P： i: 0 in : bi = ui Q: i: 0 in : bi = ui+m*i : 0 j=n i: 0ij : bi=ui+m*i i: j in : bi = ui,6.5 界函数（Bound Function),前言 界函数主要用于表明循环的终止性。同时也可以用于估计执行时间的上限（时间复杂度）。同一程序可以有不同的界函数，只要满足前面关于循环语义的定理的要求即可。,6.5 界函数,一般地，通过分析循环不变式，能够较容易地找到界函数。 多数情况下，循环迭代是依照一个或几个变量的值的变化而进行的，此时，界函数可依照这些变量的变化范围和变化规律而设定。 例如：假定i