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

第二章程序规范及其正确性证明简介程序规范与程序•程序规范–在进行程序设计之前，第一步必须明确“做什么”。所谓做什么是指对欲求解的问题的描述。关于“做什么”的描述通常称为程序规范（PS-ProgramSpecification）。–这里的PS仅指功能的描述，不包括诸如处理速度、执行时间、响应周期等与时间有关性能指标。PS是软件工程的需求分析的结果。–PS的含义是映射，是输入到输出的映射，它反映了程序对数据的作用。•程序–程序也是映射，是输入到计算的映射，即每一输入都对应一串计算步骤。程序规范与程序的关系•给出规范后，程序开发就是建立一个程序，使之计算刚好能实现规范的映射；•程序验证是证明程序正确地实现了规范，即证明规范和已有程序之间的一致性规范程序输入输出映射输入计算映射程序规范的描述•规范必须用语言描述，该语言称为规范语言。•描述一个复杂问题的输入和输出之间的关系是困难的，目前对规范语言的模式尚无定论。–自然语言•直观，易于理解•不够准确，存在二义性–符号语言•可以精确地描述问题的输入和输出的关系•但是规范文本比较繁琐一个合适的程序规范语言应满足的基本条件•应当为描述者和使用者所直接理解•应当有严格的数学语义•应当与形式方法的构造理论和程序设计语言协调•应当有较强的表达能力和通用性断言与规范•断言就是关于事物性质的陈述–这个陈述可真可假。如“三是个质数”•断言可以作为程序规范描述语言•用断言作为程序的注解或作为正确性命题的一部分时，常用大括号括起来。断言与规范•例1：写一个计算商和余数的程序–程序规范：•“设被除数x1是个非负整数”•“除数x2是个正整数”•“计算x1除以X2的商y1和余数y2”–又描述为：•“初始条件：{x1=0andx20}•计算满足{x1=x2*y1+y2and0=y2x2}的整数y1和y2”断言与规范•例：求商余程序–{x1=0andx20}–y2:=x1;y1:=0;–{0=y2and0x2andx1=x2*y1+y2}–whiley2=x2do–begin{0=y2and0x2=y2andx1=x2*y1+y2}–y2:=y2-x2;y1:=y1+1;–{0=y2and0x2andx1=x2*y1+y2}–end;–{x1=x2*y1+y2and0=y2x2}断言与规范•一般地，一个程序规范可表示为由两个谓词构成的二元组（P，Q）。其中，–P描述了所欲求解的问题必须满足的初始条件，它限定了输入参数的性质，称为初始断言或前置断言；–Q描述了问题的最终解必须满足的性质，称为结果断言或后置断言。断言与规范•程序断言是对程序的性质的陈述•最重要的一个程序断言为：{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）时，必须指明哪些量是可变的，哪些是不可变的。如果是可变的，不要时对前者还需指明其变化方式。•输入参数–在程序执行前从外部获得值，但在程序执行中，其值始终保持不变的变量。一般用以x开头的标识符表示。•输出变量–其值随程序的执行而不断变化的变量。一般以y开头的变量，或不以x和u开头的变量标识。•辅助变量–为了描述程序变量取值变化方式而因入的变量。这些变量不得在程序中出现，用以u开头的变量表示。断言与规范（举例）•例1.–编写一个程序Swap（y1，y2）–功能是把y1，y2两变量的值互换。•程序规范:–({y1=u1∧y2=u2}，{y1=u2∧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≤in:b[i]≤b[i+1])}–其中，u[m:n]代表b的任意可能初值；perm(b[m:n],u[m:n])表示b是u的一个置换。程序的非形式化正确性证明简介•程序正确性断言{P}S{Q}的意义：–“若S的执行开始于一个满足P的状态，那么这个执行必将在有限的时间内终止于一个满足Q的状态”。–所谓一个状态时满足P（或Q），即指在此状态下P（或Q）为真。程序的非形式化正确性证明简介•设（P，Q）是一个规范，S是依照这个规范要求设计的程序，且是由语句s1，s2，…，sn组成的一个枚举型程序–即其执行等于组成它的各个语句的逐一顺序的执行–其中的每个语句都只有一个入口和一个出口，且没有GOTO语句•令P1,Q1,P2,Q2,…,Pn,Qn是2n个谓词，且P=P1，Q=Qn。如果所有断言{Pi}Si{Qi}，i=1，2，…,n,为真，并且每个蕴涵：QiPi+1，i=1，2，…,n成立，就称（P1，Q1），（P2，Q2），…,（Pn，Qn）是{P}S{Q}的一个证明。程序的非形式化正确性证明简介程序的非形式化正确性证明举例•例1：令（P，Q）为：P：{i≥0∧s=b[0]+…+b[i]}Q：{i0∧s=b[0]+…+b[i]}令S为：i:=i+1;s:=s+b[i]简单证明如下：{P：i≥0∧s=b[0]+…+b[i]}{P1：i+10∧s=b[0]+…+b[i+1-1]}i:=i+1;{Q1:i0∧s=b[0]+…+b[i-1]}{P2:i0∧s+b[i]=b[0]+…+b[i-1]+b[i]}s:=s+b[i]{Q:i0∧s=b[0]+…+b[i]}这个证明梗概意味着下面各断言依次为真：1.PP12.{P1}i:=i+1{Q1}3.Q1P24.{P2}s:=s+b[i]{Q}只要证明上面的4个断言为真，就可以证明{P}S{Q}为真。课堂练习•写出下面问题的规范:1.计算一个整数的绝对值；2.求两个整数的最大值；3.求两个非负整数的最大公约数；4.置y等于数组b[0:n-1]中的最大值的位置；5.判定一个大于1的整数是否素数；6.判断数组b[0:n-1]是否已排序了；7.求数组a[0:n-1]与b[0:n-1]的内积