程序规范及程序正确性证明.ppt

《程序规范及程序正确性证明.ppt》由会员上传分享，免费在线阅读，更多相关内容在PPT专区-天天文库。

1、第二章程序规范及其正确性证明简介程序规范与程序程序规范在进行程序设计之前，第一步必须明确“做什么”。所谓做什么是指对欲求解的问题的描述。关于“做什么”的描述通常称为程序规范（PS-ProgramSpecification）。这里的PS仅指功能的描述，不包括诸如处理速度、执行时间、响应周期等与时间有关性能指标。PS是软件工程的需求分析的结果。PS的含义是映射，是输入到输出的映射，它反映了程序对数据的作用。程序程序也是映射，是输入到计算的映射，即每一输入都对应一串计算步骤。程序规范与程序的关系给出规范后，程序开

2、发就是建立一个程序，使之计算刚好能实现规范的映射；程序验证是证明程序正确地实现了规范，即证明规范和已有程序之间的一致性规范程序输入输出映射输入计算映射程序规范的描述规范必须用语言描述，该语言称为规范语言。描述一个复杂问题的输入和输出之间的关系是困难的，目前对规范语言的模式尚无定论。自然语言直观，易于理解不够准确，存在二义性符号语言可以精确地描述问题的输入和输出的关系但是规范文本比较繁琐一个合适的程序规范语言应满足的基本条件应当为描述者和使用者所直接理解应当有严格的数学语义应当与形式方法的构造理论和程序设计语

3、言协调应当有较强的表达能力和通用性断言与规范断言就是关于事物性质的陈述这个陈述可真可假。如“三是个质数”断言可以作为程序规范描述语言用断言作为程序的注解或作为正确性命题的一部分时，常用大括号括起来。断言与规范例1：写一个计算商和余数的程序程序规范：“设被除数x1是个非负整数”“除数x2是个正整数”“计算x1除以X2的商y1和余数y2”又描述为：“初始条件：{x1>=0andx2>0}计算满足{x1=x2*y1+y2and0<=y2=0andx2>0}

4、y2:=x1;y1:=0;{0<=y2and0=x2dobegin{0<=y2and0

5、的最终解必须满足的性质，称为结果断言或后置断言。断言与规范程序断言是对程序的性质的陈述最重要的一个程序断言为：{P}S{Q}其中，（P，Q）是程序S的程序规范S是一个程序（或语句）断言{P}S{Q}称为S关于（P，Q）的正确性断言若，S开始执行时P为真则，S的执行必终止，且终止时Q为真断言与规范问题：如何构造断言使他们能准确地反映不同位置上程序的性质？有了断言，如何证明他们的正确性？能否有准则，可以从规范（P，Q）构造出程序S，使{P}S{Q}为真。程序断言的进一步说明说明在给出规范描述（P，Q）时，必须指

6、明哪些量是可变的，哪些是不可变的。如果是可变的，不要时对前者还需指明其变化方式。输入参数在程序执行前从外部获得值，但在程序执行中，其值始终保持不变的变量。一般用以x开头的标识符表示。输出变量其值随程序的执行而不断变化的变量。一般以y开头的变量，或不以x和u开头的变量标识。辅助变量为了描述程序变量取值变化方式而因入的变量。这些变量不得在程序中出现，用以u开头的变量表示。断言与规范（举例）例1.编写一个程序Swap（y1，y2）功能是把y1，y2两变量的值互换。程序规范:({y1=u1∧y2=u2}，{y1=u

7、2∧y2=u1})断言与规范（举例）例2：对数组b[m：n]进行排序的程序。功能是把数组b[m：n]各元素的值从小到大排列起来，使得最后的数组满足b[i]≤b[i+1]，i=m，…,n-1。规范：P：{m≤n∧b[m:n]=u[m:n]}Q：{m≤n∧perm(b[m:n],u[m:n])∧(i:m≤i

8、开始于一个满足P的状态，那么这个执行必将在有限的时间内终止于一个满足Q的状态”。所谓一个状态时满足P（或Q），即指在此状态下P（或Q）为真。程序的非形式化正确性证明简介设（P，Q）是一个规范，S是依照这个规范要求设计的程序，且是由语句s1，s2，…，sn组成的一个枚举型程序即其执行等于组成它的各个语句的逐一顺序的执行其中的每个语句都只有一个入口和一个出口，且没有GOTO语句令P1,Q1,P2,Q2,…,Pn,Qn