程序设计方法学课件.ppt

《程序设计方法学课件.ppt》由会员分享，可在线阅读，更多相关《程序设计方法学课件.ppt（43页珍藏版）》请在淘文阁 - 分享文档赚钱的网站上搜索。

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

2、nput variable lprogram variableloutput variable 2023/2/8国家高性能计算中心4 设程序P含有n个标识符（程序变量）程序状态：某一时刻标识符集合所对应的值集合 构成程序P在该时刻的状态(snapshot)。程序状态记为s。s一个二元组的集合，每个二元组由一标识符和它所对应的值组成，例如：s=（x,5）,（y,0）,（z,3）含义：程序中有三个变量：x，y，z。运行在 x5，y0，z3的状态。2023/2/8国家高性能计算中心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=x=y do begin r:=r-y;q:=q+1 end z1:=q;z2:=r状态初始状态进入循环之前，经过赋初值以后的状态退出循环之后的状态2023/2/8国家高性能计算中心7二、谓词及谓词变元的赋值二、谓词及谓词变元的赋值l命题：可以判定真假的布尔表达式。如：3+3=6，35 命题是“算术表达式”，对事实的一种陈述。l谓词：含有变量的布尔方程式 谓词的值视变量的取值而定。如：x=2，x+y=6？谓词是“方程式”，求谓词的值需带入变量的值。2023/2/8国家高性能计算中心8l

4、n元谓词：所有变量都取自于一定的定义域，这里，Di表示变元xi的定义域。l谓词的计算 谓词计算是一个由变量的定义域到函数值域0，1集合的全映射过程。T，F2023/2/8国家高性能计算中心9三、对谓词演算的扩充三、对谓词演算的扩充 1、对值域的扩充 二值谓词：T or F “三值”谓词：引入为“无定义的对象”的值U，将F，T扩展成F，T，U。例如：设 谓词：，状态：则2023/2/8国家高性能计算中心102、对连接词（逻辑运算符）的扩充 引进新的运算符 cand,cor：分别表示有条件的and和or。cand和cor 的运算法则用下面的真值表给出：bcb cand cb cor cTTTTTF

5、FTTUUTFTFTFFFFFUFUUTUUUFUUUUUU即：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 c2023/2/8国家高性能计算中心11cand、cor的性质1）不满足交换律，即 b cand c 与 c cand b，b cor c 与 c cor b 是不等价的2）满足结合律：E1 cand（E2 cand E3）（E1 cand E2）cand E3 E1 cor（E2 cor E3）（E1 cor E2）cor E3分配律：E1 can

6、d（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 E22023/2/8国家高性能计算中心123、对量词(quantifier)的扩充 全程量词 ：存在量词 ：其中，m，n为整型表达式，且mn；Ei（i=1，2，n-1）是谓词；标识符i称为被量化的标识符，或受约束标识符；值集i|min并且i为整数为i的值域。2023/2/8国家高性能计算中心13引进一些新的量词化表示：求和量词

7、乘积量词 计数量词 这些量词之间有下面的等价形式：2023/2/8国家高性能计算中心14约束变量与自由变量 约束变量：被量词化的变量 例如：x,y 是自由变量，i是约束变量 量词的作用域：例：区分 和2023/2/8国家高性能计算中心151.2 程序断言程序断言一、一、程序断言程序断言 程序中有关变量应满足的关系（或条件）称为程序断言。程序断言的性质和要求：v断言必须准确、完善地刻画变量间应满足的关系（或条件）。v断言通常用谓词（布尔表达式）表示。v断言（谓词）可在程序状态S下计算其真假值。2023/2/8国家高性能计算中心16例例2：求断言的值。设程序P的状态为：s=(B,3),(C,1),

8、(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下为假 2023/2/8国家高性能计算中心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/2/8国家高性能计算中心18二、二、程序断言的作用程序断言的作用 将程序断言插入到程序的适当位置，用 括起来，表示，每当“控制流”到达这些位置时，将对该处的布尔表达式（程序断言）进行检测。如果取值为真

9、，则表示程序正确执行；否则，表示出错，输出错误信息和有关变量的值以检错。2023/2/8国家高性能计算中心19三、三、程序断言的重要性程序断言的重要性 在程序中插入适当的断言，可以使得我们在编制（调试）程序的过程中，自动验证程序的正确性，从而保证编制出来的程序是正确的。借助这种方法，可以帮助我们写出没有错误的程序，缩短编制程序和调试所用的时间，也使得写出的程序更容易被理解。2023/2/8国家高性能计算中心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/2

10、/8国家高性能计算中心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/2/8国家高性能计算中心22思路：在程序的某些关节点验证程序变量之间的关系，即验证程序状态在该点是否满足给定的关系（条件），如果满足说明正确，否则说明有错！方法：首先在程序的必要位置插入对程序变量关系的陈述程序断言（包括前置条件、后置条件等）然后当程序执行到该

11、点时，求程序断言（谓词）的值，值为真表示正确，假表示出错。2023/2/8国家高性能计算中心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 0ry 插入程序断言：程序断言相当于对程序的注释，不是程序的必要部分，其作用仅在于“验证”程序的正确性。如何验证while循环体内的正确性？2023/2/8国家高性能计算中心24验证while循环体内的正确性：分析：进入循环体之前，r=x，q=0，式x=y*q+r是成立的。循环体每次执行的前后，式x=y*q+r亦成立（由计算方法保证）。方法：将x=y*q+r作

12、为断言的一部分插入到程序的循环部分。2023/2/8国家高性能计算中心25经过加强后的断言描述：0 x and 0y and xy r:=x;q:=0;0r and 0y and x=y*q+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 2023/2/8国家高性能计算中心261.3 文字代换和状态转换定理文字代换和状态转换定理 表达式求值相当于用状态S下标识符的值代换表达式中的标识符，然后进行计算。如何演算程序断言的值？为方便地计算程序断言在

13、状态S下的值，给出一种一般方法：文字代换。2023/2/8国家高性能计算中心27一、文字代换一、文字代换1简单变量的文字代换 设E，e是表达式，x是标识符。表示用e同时代替E中所有x的自由出现而得到的表达式。例：设谓词 含义：x和数组b的所有元素应小于y注：这一过程中，可能需要适当使用括号把e括起来，以保持运算的优先次序。2023/2/8国家高性能计算中心28两级代换，逐级进行。用括号表示一定的组合关系i是受约束变量，不能代换2023/2/8国家高性能计算中心29 文字代换可以在任意标识符和表达式之间进行，但为了有效性，代换必须注意以下两点：代换必须产生语法正确的表达式 如：若e中标识符与E中

14、受约束的标识符同名，则应先 将E中同名标识符换名，然后再进行代换 如：先换名：再代换：语法错误引起e中的i受约束2023/2/8国家高性能计算中心30引理引理1：引理引理2：如y中不是E中自由变量，则 关于文字代换的两个引理：2023/2/8国家高性能计算中心31例：2同时代换（Simultaneous Substitution）设 表示一个互不相同的标识符表，即 是一个表达式表，且与 有相同的长度。则，在表达式E中用ei同时代换相应的xi的所有出现记为：2023/2/8国家高性能计算中心321.代换必须同时进行 如：2.一般来说，与 可能不同 如同时代换的要点：2023/2/8国家高性能计算

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

16、标识符均相同）：s=(s；x:v)例：在状态s下执行赋值语句x:=2，则终止状态为 s=(s；x:2)2023/2/8国家高性能计算中心363.引理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即得2023/2/8国家高性能计算中心37引理3：同时代换情况下的引理 设x是一个互不相同的标示符表，E是表达式，u是一与x不同的互不相同的标识符表，则有 证明：略。2023/2/8国家高性能计算中心381.4 使用断言说明程

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

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