程序设计方法学课件

单击此处编辑母版标题样式,单击此处编辑母版文本样式,第二级,第三级,第四级,第五级,*,国家高性能计算中心,*,单击此处编辑母版标题样式,单击此处编辑母版文本样式,第二级,第三级,第四级,第五级,*,国家高性能计算中心,*,2024/11/6,国家高性能计算中心,1,第二篇 预备知识,第一章 程序状态及有关转换的定理,第二章 程序正确性证明及其证明法则,第三章 数组的标记法及有关约定,2023/9/14国家高性能计算中心1第二篇 预备知识第一章,2024/11/6,国家高性能计算中心,2,第一章 程序状态及有关状态转换的定理,1.4,使用断言说明程序,1.3,文字代换和状态转换定理,1.2,程序断言,1.1,程序状态与谓词演算中的有关知识,2023/9/14国家高性能计算中心2第一章 程序状态及有关,2024/11/6,国家高性能计算中心,3,1.1,程序状态与谓词演算中的有关知识,一、程序状态,程序变量：程序中特定的标识符。程序执行过,程中的任一时刻，这些变量都具有,特定的值（或有待于赋值）,input variable,program variable,output variable,2023/9/14国家高性能计算中心31.1 程序状态与谓词,2024/11/6,国家高性能计算中心,4,设程序,P,含有,n,个标识符（程序变量）,程序状态,：某一时刻标识符集合所对应的值集合,构成程序,P,在该时刻的状态,(snapshot),。,程序状态记为,s,。,s,一个,二元组,的集合，每个二元组由一标识符和它所对应的值组成，例如：,s=,（,x,5,）,（,y,0,）,（,z,3,）,含义：程序中有三个变量：,x,，,y,，,z,。运行在,x,5,，,y,0,，,z,3,的状态。,2023/9/14国家高性能计算中心4 设程序P,2024/11/6,国家高性能计算中心,5,表达式的值,：设程序处在状态,s,下，表达式,e,在状态,s,下的值记为,s(e),，表示用,s,中各标识符,的值代换,e,中对应标识符后计算所得的,结果。,如：,设，,s=,（,x,5,）,（,y,0,）,（,z,3,）,则，,e,1,=x+y s(e,1,)=5+0=5,e,2,=x=y do,begin,r:=r-y;,q:=q+1,end,z1:=q;,z2:=r,状态,初始状态,进入循环之前，经过赋初值以后的状态,退出循环之后的状态,2023/9/14国家高性能计算中心6例如：设有程序P：状态,2024/11/6,国家高性能计算中心,7,二、谓词及谓词变元的赋值,命题：可以判定真假的,布尔表达式,。,如：,3+3=6,，,35,命题是,“,算术表达式,”,，对事实的一种陈述。,谓词：含有变量的,布尔方程式,谓词的值视变量的取值而定。,如：,x=2,，,x+y=6,？,谓词是,“,方程式,”,，求谓词的值需带入变量的值。,2023/9/14国家高性能计算中心7二、谓词及谓词变元的赋,2024/11/6,国家高性能计算中心,8,n,元谓词：,所有变量都取自于一定的,定义域,，这里，,D,i,表示变元,x,i,的定义域。,谓词的计算,谓词计算是一个由变量的定义域到函数值域,0,，,1,集合的全映射过程。,T,，,F,2023/9/14国家高性能计算中心8 n元谓词：T，F,2024/11/6,国家高性能计算中心,9,三、对谓词演算的扩充,1,、对值域的扩充,二值谓词：,T or F,“,三值,”,谓词：引入为,“,无定义的对象,”,的值,U,，将,F,，,T,扩展成,F,，,T,，,U,。,例如：,设 谓词：，,状态：,则,2023/9/14国家高性能计算中心9三、对谓词演算的扩充,2024/11/6,国家高性能计算中心,10,2,、对连接词（逻辑运算符）的扩充,引进新的运算符,cand,cor,：,分别表示有条件的,and,和,or,。,cand,和,cor,的运算法则用下面的真值表给出：,b,c,b cand c,b cor c,T,T,T,T,T,F,F,T,T,U,U,T,F,T,F,T,F,F,F,F,F,U,F,U,U,T,U,U,U,F,U,U,U,U,U,U,即：,b cand c,：,if b,为,U then U,else,if b then c,else F,b cor c,：,if b,为,U then U,else,if b then T,else c,2023/9/14国家高性能计算中心102、对连接词（逻辑运,2024/11/6,国家高性能计算中心,11,cand,、,cor,的性质,1,）不满足交换律，即,b cand c,与,c cand b,，,b cor c,与,c cor b,是不等价的,2,）满足,结合律,：,E,1,cand,（,E,2,cand E,3,）（,E,1,cand E,2,）,cand E,3,E,1,cor,（,E,2,cor E,3,）（,E,1,cor E,2,）,cor E,3,分配律,：,E,1,cand,（,E,2,cor E,3,）（,E,1,cand E,2,）,cor,（,E,1,cand E,3,）,E,1,cor,（,E,2,cand E,3,）（,E,1,cor E,2,）,cand,（,E,1,cor E,3,）,De Morgan,律,：,（,E,1,cand E,2,）,E,1,cor E,2,（,E,1,cor E,2,）,E,1,cand E,2,2023/9/14国家高性能计算中心11cand、cor的性,2024/11/6,国家高性能计算中心,12,3,、对量词,(quantifier),的扩充,全程量词 ：,存在量词 ：,其中，,m,，,n,为整型表达式，且,m,n,；,E,i,（,i=1,，,2,，,，,n-1,）是谓词；,标识符,i,称为,被量化的标识符,，或,受约束标识符,；,值集,i|mi,n,并且,i,为整数,为,i,的值域。,2023/9/14国家高性能计算中心12,2024/11/6,国家高性能计算中心,13,引进一些新的量词化表示：,求和量词,乘积量词,计数量词,这些量词之间有下面的等价形式：,2023/9/14国家高性能计算中心13引进一些新的量词化表,2024/11/6,国家高性能计算中心,14,约束变量与自由变量,约束变量：被量词化的变量,例如：,x,y,是自由变量，,i,是约束变量,量词的作用域：,例：区分,和,2023/9/14国家高性能计算中心14约束变量与自由变量,2024/11/6,国家高性能计算中心,15,1.2,程序断言,一、程序断言,程序中有关变量应满足的关系（或条件）称为程序断言。,程序断言的性质和要求：,断言必须准确、完善地刻画变量间应满足的关系（或条件）。,断言通常用谓词（布尔表达式）表示。,断言（谓词）可在程序状态,S,下计算其真假值。,2023/9/14国家高性能计算中心151.2 程序断言一、,2024/11/6,国家高性能计算中心,16,例,2,：求断言的值。设程序,P,的状态为：,s=(B,3),(C,1),(A,T),求断言,(B+C)0,A),在状态,s,下的值,解：,s(B+C)0A),s(B+C)0)s(A),(3+1)0)T,F,故，断言,(B+C)0A),在状态,s,下为假,2023/9/14国家高性能计算中心16例2：求断言的值。设,2024/11/6,国家高性能计算中心,17,程序断言的位置：设有程序,P,begin,x:=;y:=;r:=0;,while y 0 do,r:=x mod y;,x:=y;y:=r,end while,z:=x,end,2023/9/14国家高性能计算中心17程序断言的位置：设有,2024/11/6,国家高性能计算中心,18,二、程序断言的作用,将程序断言插入到程序的适当位置，用,括起来，表示，每当“控制流”到达这些位置时，将对该处的布尔表达式（程序断言）进行检测。如果取值为真，则表示程序正确执行；否则，表示出错，输出错误信息和有关变量的值以检错。,2023/9/14国家高性能计算中心18二、程序断言的作用,2024/11/6,国家高性能计算中心,19,三、程序断言的重要性,在程序中插入适当的断言，可以使得我们在编制（调试）程序的过程中，自动验证程序的正确性，从而保证编制出来的程序是正确的。借助这种方法，可以帮助我们写出没有错误的程序，缩短编制程序和调试所用的时间，也使得写出的程序更容易被理解。,2023/9/14国家高性能计算中心19三、程序断言的重要,2024/11/6,国家高性能计算中心,20,例：计算用正整数,y,除非负整数,x,所得的商,q,和余数,r,即：,x=q*y+r,基本程序段：,r:=x;q:=0;,while r,y do,begin r:=r-y;q:=q+1 end;,2023/9/14国家高性能计算中心20例：计算用正整数y除,2024/11/6,国家高性能计算中心,21,人工调试方式：,write(x=,x,y=,y);,r:=x;q:=0;,while r,y do,begin r:=r-y;q:=q+1 end;,write(y*q+r=,y*q+r);,怎样验证程序是正确的呢？,如果这一程序段被反复调用（处于循环之中），这种调试就太繁琐了。,有没有自动的方式验证每一步的正确性？,2023/9/14国家高性能计算中心21人工调试方式：怎样验,2024/11/6,国家高性能计算中心,22,思路,：,在程序的某些关节点验证程序变量之间的关系，即验证程序状态在该点是否满足给定的关系（条件），如果满足说明正确，否则说明有错！,方法,：,首先在程序的必要位置插入对程序变量关系的陈述,程序断言（包括前置条件、后置条件等）,然后当程序执行到该点时，求程序断言（谓词）的值，值为真表示正确，假表示出错。,2023/9/14国家高性能计算中心22思路：,2024/11/6,国家高性能计算中心,23,0,x and 0,y,r:=x;q:=0;,while r,y do,begin r:=r-y;q:=q+1 end;,x=q*y+r and 0,r,y,插入程序断言：,程序断言相当于对程序的注释，不是程序的必要部分，其作用仅在于“,验证,”程序的正确性。,如何验证while循环体内的正确性？,2023/9/14国家高性能计算中心23 插,2024/11/6,国家高性能计算中心,24,验证,while,循环体内的正确性：,分析：,进入循环体之前，,r=x,，,q=0,，式,x=y*q+r,是成立的。,循环体每次执行的前后，式,x=y*q+r,亦成立（由计算方法保证）。,方法：,将,x=y*q+r,作为断言的一部分插入到程序的循环部分。,2023/9/14国家高性能计算中心24验证while循环体,2024/11/6,国家高性能计算中心,25,经过加强后的断言描述：,0,x and 0,y and xy,r:=x;q:=0;,0,r and 0,y and x=y*q+r,while r,y do,begin,0,r and,0,yr,and x=y*q+r,r:=r-y;q:=q+1,0,r and 0,y and x=y*q+r,end;,x=q*y+r and 0,r,y,2023/9/14国家高性能计算中心25经过加强后的断言描述,2024/11/6,国家高性能计算中心,26,1.3,文字代换和状态转换定理,表达式求值相当于用状态,S,下标识符的值代换表达式中的标识符，然后进行计算。,如何演算程序断言的值？,为方便地计算程序断言在状态,S,下的值，给出一种一般方法：文字代换。,2023/9/14国家高性能计算中心261.3 文字代换和状,2024/11/6,国家高性能计算中心,27,一、文字代换,1,简单变量的文字代换,设,E,，,e,是表达式，,x,是标识符。,表示用,e,同时,代替,E,中所有,x,的,自由出现,而得到的