程序设计方法学课件.ppt

《程序设计方法学课件.ppt》由会员分享，可在线阅读，更多相关《程序设计方法学课件.ppt（43页珍藏版）》请在三一办公上搜索。

1、2022/12/20,国家高性能计算中心,1,第二篇 预备知识,第一章 程序状态及有关转换的定理,第二章 程序正确性证明及其证明法则,第三章 数组的标记法及有关约定,2022/12/20,国家高性能计算中心,2,第一章 程序状态及有关状态转换的定理,1.4 使用断言说明程序,1.3 文字代换和状态转换定理,1.2 程序断言,1.1 程序状态与谓词演算中的有关知识,2022/12/20,国家高性能计算中心,3,1.1 程序状态与谓词演算中的有关知识,一、程序状态 程序变量： 程序中特定的标识符。程序执行过 程中的任一时刻，这些变量都具有 特定的值（或有待于赋值）input variable pr

2、ogram variableoutput variable,2022/12/20,国家高性能计算中心,4,设程序P含有n个标识符（程序变量） 程序状态：某一时刻标识符集合所对应的值集合 构成程序P在该时刻的状态(snapshot)。 程序状态记为s。s一个二元组的集合，每个二元组由一标识符和它所对应的值组成，例如： s=（x,5）,（y,0）,（z,3） 含义：程序中有三个变量：x，y，z。运行在 x5，y0，z3的状态。,2022/12/20,国家高性能计算中心,5,表达式的值：设程序处在状态s下，表达式e在状态s 下的值记为s(e)，表示用s中各标识符 的值代换e中对应标识符后计算所得的

3、结果。 如： 设，s=（x,5）,（y,0）,（z,3） 则， e1 = x+y s(e1)= 5+0 = 5 e2 = x3 s(e2) = F e3 = x/y s(e3)没定义,2022/12/20,国家高性能计算中心,6,例如：设有程序P： r:=x; q:=0; while r=y do begin r:=r-y; q:=q+1 end z1:=q; z2:=r,状态,初始状态,进入循环之前，经过赋初值以后的状态,退出循环之后的状态,2022/12/20,国家高性能计算中心,7,二、谓词及谓词变元的赋值,命题：可以判定真假的布尔表达式。 如：3+3=6，35 命题是“算术表达式”，对

4、事实的一种陈述。谓词：含有变量的布尔方程式 谓词的值视变量的取值而定。 如：x=2，x+y=6？ 谓词是“方程式” ，求谓词的值需带入变量的值。,2022/12/20,国家高性能计算中心,8,n元谓词： 所有变量都取自于一定的定义域，这里，Di表示变元xi的定义域。 谓词的计算 谓词计算是一个由变量的定义域到函数值域0，1集合的全映射过程。,T，F,2022/12/20,国家高性能计算中心,9,三、对谓词演算的扩充,1、对值域的扩充 二值谓词：T or F “三值”谓词：引入为“无定义的对象”的值U，将F，T扩展成F，T，U。 例如： 设 谓词： ， 状态： 则,2022/12/20,国家高性

5、能计算中心,10,2、对连接词（逻辑运算符）的扩充 引进新的运算符 cand, cor：分别表示有条件的and和or。 cand和cor 的运算法则用下面的真值表给出：,即： b cand c： if b 为U then U else if b then c else Fb cor c： if b 为U then U else if b then T else c,2022/12/20,国家高性能计算中心,11,cand、cor的性质1）不满足交换律，即 b cand c 与 c cand b， b cor c 与 c cor b 是不等价的2）满足结合律：E1 cand （ E2 cand

6、E3 ） （ E1 cand E2）cand E3 E1 cor （ E2 cor E3 ） （ E1 cor E2）cor E3分配律：E1 cand （ E2 cor E3 ） （ E1 cand E2）cor （ E1 cand E3 ） E1 cor （ E2 cand E3 ） （ E1 cor E2）cand （ E1 cor E3）De Morgan律：（E1 cand E2 ） E1 cor E2 （E1 cor E2 ） E1 cand E2,2022/12/20,国家高性能计算中心,12,3、对量词(quantifier)的扩充 全程量词 ： 存在量词 ： 其中， m，n为

7、整型表达式，且mn； Ei（i=1，2，n-1）是谓词； 标识符i称为被量化的标识符，或受约束标识符； 值集i|min并且i为整数为i的值域。,2022/12/20,国家高性能计算中心,13,引进一些新的量词化表示： 求和量词 乘积量词 计数量词 这些量词之间有下面的等价形式：,2022/12/20,国家高性能计算中心,14,约束变量与自由变量 约束变量：被量词化的变量 例如： x,y 是自由变量，i是约束变量 量词的作用域： 例：区分 和,2022/12/20,国家高性能计算中心,15,1.2 程序断言,一、 程序断言 程序中有关变量应满足的关系（或条件）称为程序断言。 程序断言的性质和要求

8、：断言必须准确、完善地刻画变量间应满足的关系（或条件）。断言通常用谓词（布尔表达式）表示。断言（谓词）可在程序状态S下计算其真假值。,2022/12/20,国家高性能计算中心,16,例2：求断言的值。设程序P的状态为： s = (B,3),(C,1),(A,T) 求断言(B+C)0A)在状态s下的值 解： s (B+C)0A) s (B+C)0) s(A) (3+1)0)T F 故，断言(B+C)0A)在状态s下为假,2022/12/20,国家高性能计算中心,17,程序断言的位置：设有程序P begin x:= ; y:= ; r:=0; while y 0 do r:=x mod y; x:

9、=y; y:= r end while z:=x end,2022/12/20,国家高性能计算中心,18,二、 程序断言的作用 将程序断言插入到程序的适当位置，用 括起来，表示，每当“控制流”到达这些位置时，将对该处的布尔表达式（程序断言）进行检测。 如果取值为真，则表示程序正确执行； 否则，表示出错，输出错误信息和有关变量的值以检错。,2022/12/20,国家高性能计算中心,19,三、 程序断言的重要性 在程序中插入适当的断言，可以使得我们在编制（调试）程序的过程中，自动验证程序的正确性，从而保证编制出来的程序是正确的。 借助这种方法，可以帮助我们写出没有错误的程序，缩短编制程序和调试所用

10、的时间，也使得写出的程序更容易被理解。,2022/12/20,国家高性能计算中心,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; ,2022/12/20,国家高性能计算中心,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); ,怎样验证程序是正确的呢？,如果这一程序段被反复调用（处于循环之中），这种调试就

11、太繁琐了。,有没有自动的方式验证每一步的正确性？,2022/12/20,国家高性能计算中心,22,思路： 在程序的某些关节点验证程序变量之间的关系，即验证程序状态在该点是否满足给定的关系（条件），如果满足说明正确，否则说明有错！方法： 首先在程序的必要位置插入对程序变量关系的陈述程序断言（包括前置条件、后置条件等） 然后当程序执行到该点时，求程序断言（谓词）的值，值为真表示正确，假表示出错。,2022/12/20,国家高性能计算中心,23, 0 x and 0y r:=x; q:=0; while r y do begin r:=r-y;q:=q+1 end; x = q*y + r and

12、0ry ,插入程序断言：,程序断言相当于对程序的注释，不是程序的必要部分，其作用仅在于“验证”程序的正确性。,如何验证while循环体内的正确性？,2022/12/20,国家高性能计算中心,24,验证while循环体内的正确性：分析：进入循环体之前， r=x，q=0，式x=y*q+r是成立的。循环体每次执行的前后，式x=y*q+r亦成立（由计算方法保证）。方法： 将x=y*q+r作为断言的一部分插入到程序的循环部分。,2022/12/20,国家高性能计算中心,25,经过加强后的断言描述：, 0 x and 0y and xy r:=x; q:=0; 0r and 0y and x = y*q+

13、r while r y do begin 0r and 0yr and x = y*q+r r:=r-y;q:=q+1 0r and 0y and x = y*q+r end; x = q*y + r and 0ry ,2022/12/20,国家高性能计算中心,26,1.3 文字代换和状态转换定理,表达式求值相当于用状态S下标识符的值代换表达式中的标识符，然后进行计算。 如何演算程序断言的值？ 为方便地计算程序断言在状态S下的值，给出一种一般方法：文字代换。,2022/12/20,国家高性能计算中心,27,一、文字代换1简单变量的文字代换 设E，e是表达式，x是标识符。 表示用e同时代替E中所

14、有x的自由出现而得到的表达式。 例：设谓词 含义：x和数组b的所有元素应小于y,注：这一过程中，可能需要适当使用括号把e括起来，以保持运算的优先次序。,2022/12/20,国家高性能计算中心,28,两级代换，逐级进行。用括号表示一定的组合关系,i是受约束变量，不能代换,2022/12/20,国家高性能计算中心,29,文字代换可以在任意标识符和表达式之间进行，但为了有效性，代换必须注意以下两点： 代换必须产生语法正确的表达式 如： 若e中标识符与E中受约束的标识符同名，则应先 将E中同名标识符换名，然后再进行代换 如：先换名：再代换：,语法错误,引起e中的i受约束,2022/12/20,国家高

15、性能计算中心,30,引理1： 引理2：如y中不是E中自由变量，则,关于文字代换的两个引理：,2022/12/20,国家高性能计算中心,31,例：,2同时代换（Simultaneous Substitution） 设 表示一个互不相同的标识符表，即 是一个表达式表，且与 有相同的长度。 则，在表达式E中用ei同时代换相应的xi的所有出现记为：,2022/12/20,国家高性能计算中心,32,1. 代换必须同时进行 如：2. 一般来说， 与 可能不同 如,同时代换的要点：,2022/12/20,国家高性能计算中心,33,二、状态转换（state transformation）,设S是一个状态，E是

16、一个表达式，则，E在状态S下的值记为S(E)。 例如： 则,文字代换,2022/12/20,国家高性能计算中心,34,程序状态的转换 程序状态是怎样转换的呢？ 给程序中的变量赋新值（包括增加或减少了变量的个数）。 设s和s是相邻的两个程序状态， s和s的差别主要在于s和s中某些变量的值不同（包括变量的增加或减少）。,2022/12/20,国家高性能计算中心,35,状态转换的表示： 设s和s是两个状态，它们有相同的标识符，且除了某个标识符的值不同外，其余的都一样，则用下面的标记来表示s（这里设s和s中x的值不同，x在s中的值为v，其余的标识符均相同）： s=(s；x:v),例：在状态s下执行赋值

17、语句x:=2，则终止状态为 s=(s；x:2),2022/12/20,国家高性能计算中心,36,3. 引理1.3： 证明：略。 引理1.4：已知状态S，设 ，则 证明：由S定义，有S(E)=(S;x:S(e)(E) 在状态(S;x:S(e)下计算E的值须用S(e)代换x，则： 由于x在 中不再出现，因而 的值不依赖于x，故有 由引理1.3即得,2022/12/20,国家高性能计算中心,37,引理3：同时代换情况下的引理 设x是一个互不相同的标示符表，E是表达式，u是一与x不同的互不相同的标识符表，则有 证明：略。,2022/12/20,国家高性能计算中心,38,1.4 使用断言说明程序,一、程

18、序说明1.程序说明的目标：精确描述程序要干什么。2. 如何进行程序说明采用自然语言利用断言说明程序3. 如何利用断言说明程序？ 一般方法：在程序的前后分别放置用于验证程序状态的谓词，判断程序执行之前是否进入“正确状态”，程序执行之后，是否输出“正确状态”。,2022/12/20,国家高性能计算中心,39,4. 使用断言进行程序说明的一般形式 Q S R 其中，S：表示程序（段）Q，R：表示谓词，是关于S的两个断言，分别表示S执行前后有关变量之间应满足的关系（状态）。 Q称为S的前置条件（或前断言）； R称为S的后置条件（或目标断言）。 注：断言用 括起来，以与程序分隔开。,2022/12/20

19、,国家高性能计算中心,40,例1 求两个非负实数之积的程序说明Q：a0b0 SR：z:=a*b例2 求数组b0:n-1元素之和的程序说明Q：n0 SR：s=(i；0in：bi),2022/12/20,国家高性能计算中心,41,例3 数组b0:n-1分类的程序说明Q：n0 SR：( )例4 求x/y商和余数的程序说明Q：x0y0 SR：0ryx=y*q+r,2022/12/20,国家高性能计算中心,42,二、程序正确性,1. 什么叫程序正确？ 如果程序在满足前提的条件下执行，能够达到结论所要求的目的，则称该程序是正确的对合法的输入能够得到合法的输出。 程序正确性包括两个方面的含义：完全正确性：如果在使Q为真的状态下开始执行S，S一定终止，且终止时的状态使R为真，则称S完全正确，记为：部分正确性：如果在使Q为真的状态下开始执行S，若S终止，且终止时的状态使R为真，则称S部分正确，记为：,2022/12/20,国家高性能计算中心,43,程序正确性证明的含义： 这里讨论的正确性是指程序的完全正确性； 注：式QSR本身也是谓词。 满足完全正确性，则谓词QSR为真，反之为假。 程序正确性证明就是证明QSR是否为真。 故，所谓程序的正确性，就是讨论S关于一对前后断言Q、R的正确性，即QSR是否成立的问题。第一章结束,