程序规范及其正确性证明概述课件

第3章程序标准及其正确性证明概述内容－Whereweare？程序标准、标准的描述断言与标准及{P}S{Q}程序正确性的概念程序正确性证明的过程3.1程序标准与程序1.程序标准：程序设计之前，第一步必须明确“做什么〞。所谓“做什么〞是指对欲求解的问题的描述。程序标准〔PS-ProgramSpecification〕:关于“做什么〞的描述。这里的PS仅指功能的描述，不包括诸如处理速度、执行时间、响应周期等与时间有关性能指标。PS是软件工程的需求分析的结果。PS的含义是映射，是输入到输出的映射，它反映了程序对数据的作用。3.1程序标准与程序(续)2.程序程序也是映射，是输入到计算的映射，即每一输入都对应一串计算步。3.程序标准与程序的关系给出标准后，程序开发就是建立一个程序，使得计算刚好能实现标准的映射；程序验证是证明程序正确地实现了标准，即证明标准和已有程序之间的一致性规范程序输入输出映射输入计算映射3.1程序标准与程序(续)4.程序标准的描述-----标准语言标准必须用语言描述，该语言称为标准语言。描述一个复杂问题的输入和输出之间的关系是困难的，目前对标准语言的模式尚无定论。有三种模式：自然语言：不够准确，存在二义性，必须辅以数学语言。一阶谓词：可以精确地描述问题的输入和输出的关系，但是标准文本比较长。如Hoare系统。数学语言：用数学语言可以把输入和输出的映射描述为函数。这些函数的精确的泛函定义就构成了问题的标准。但存在过于标准的问题。3.1程序标准与程序(续)5.一个适宜的程序标准语言应满足的根本条件:应当为描述者和使用者所直接理解；应当有严格的数学语义应当与形式方法的构造理论和程序设计语言协调应当有较强的表达能力和通用性3.1程序标准与程序(续)Z语言VDMB方法三者的比较6.形式化程序标准描述语言简介3.1程序标准与程序(续)Z语言是一种基于集合论和一阶谓词逻辑的形式化语言；Z语言支持软件的形式化标准描述，标准的推理和求精；是迄今为止应用最广泛的形式语言之一；Z是在JeanRaymondAbrial等的开创性工作下，由英国牛津大学的程序设计研究小组〔PRG，ProgrammingResearchGroup〕，于20世纪80年代初开发；PRG与IBM的Hursley实验室合作，将Z语言用于IBM的客户信息控制系统的开发，使得最终的产品质量得到了全面的的提高，所测出的错误数量大大减少，并且整体开发费用降低了9％；在ISO指导下的国际标准化Z工作于2002年完成6.形式化程序标准描述语言简介－Z语言简介13.1程序标准与程序(续)提供了一种称为模式〔Schema〕的结构，它是Z的根本描述单位，以此来描述一个标准说明的状态空间〔静态性质〕和操作〔动态行为〕。Ｚ语言的模式和模式演算：状态模式对目标软件系统的结构特征进行抽象描述；操作模式对目标软件系统的行为特征进行抽象描述；通过模式演算，无论多么大型系统的规格说明都可以通过一个个小的局部来构成；6.形式化程序标准描述语言简介－Z语言简介23.1程序标准与程序(续)Ｚ模式说明可以组合成新的Ｚ模式，新的Ｚ模式继承其成分模式的一切属性和约束。软件系统的Ｚ模式规格说明可以按一定的层次结构给出。Ｚ规格说明由一系列模式组成，每个模式定义一个抽象对象或操作，并用谓词判定描述给出新的对象或操作的语义约束。模式例:6.形式化程序标准描述语言简介－Z语言简介33.1程序标准与程序(续)模式例1:[Student]//引入根本类型studentStudentSys//模式名Enrolled,tested:PStudent//声明局部,学生的密集类型#enrolled≤size//断言局部，合取关系testedenrolled等价于：//水平方式StudentSys=[enrolled,tested:PStudent|

#enrolled≤sizetestedenrolled]6.形式化程序标准描述语言简介－Z语言简介43.1程序标准与程序(续)模式例2:EnrollStudentStudentSys//=StudentsysStudentSys’的简写

name?:Student//在输入变量后加？name?enrolled//在输出变量后加！enrolled<size//带有后缀‘的变量表示操作后的变量enrolled’=enrolled∪{name?}tested’=tested

6.形式化程序标准描述语言简介－Z语言简介53.1程序标准与程序(续)缺点:⑴Ｚ语言对大型系统的模块化能力缺乏。⑵难以识别影响某一状态模式的所有操作模式。⑶不能支持规格说明的重用。⑷Ｚ语言难以由计算机直接处理。缺少商品化的工具支持等到诸多原因6.形式化程序标准描述语言简介－Z语言简介63.1程序标准与程序(续)VDM〔ViennaDevelopmentMethod〕是在1969年为开发PL/1语言时，由IBM公司维也纳实验室的研究小组提出的。初衷是为了描述PL/1语言的语义。VDM是一种功能构造性规格说明技术，它通过一阶谓词逻辑和已建立的抽象数据类型来描述每个运算或函数的功能。这种方法在90年代初在欧美许多研究机构或大学得到了广泛的应用。如曼彻斯特大学将其作为CS的必修课。1996年ISO制订了VDM的国际标准化版本VDM-SL6.形式化程序标准描述语言简介－VDM简介13.1程序标准与程序(续)VDM技术的根本思想：运用抽象数据类型、数学概念和符号来规定运算或函数的功能；可使软件系统的功能描述在抽象级上进行，完全摆脱了实现细节，这样为软件实现者提供了很大的灵活性；这种形式化规格说明还为程序正确性证明提供了依据。6.形式化程序标准描述语言简介－VDM简介23.1程序标准与程序(续)VDM支持两种抽象：数据抽象和操作抽象。一个VDM标准有以下不同的块组成：types<typedefinitions>values<valuedefinitions>functions<functiondefinitions>operations<operationdefinitions>state<statename>of<statedefinition>end6.形式化程序标准描述语言简介－VDM简介33.1程序标准与程序(续)缺点：⑴由于VDM对抽象数据类型预先定义了运算，而某些用户定义的类型在规格说明描述中无需这么多运算，因而产生了运算冗余。⑵VDM目前还未能建立一整套描述机制，将一个大型系统分解为许多运算而描述出这些运算之间的关系⑶VDM形式规格说明过于形式化不容易理解6.形式化程序标准描述语言简介－VDM简介43.1程序标准与程序(续)B方法是20世纪80年代初中期由以及BP研究中心的MATRA和GEAlsthom研究小组开发的。Ｂ语言是计算机辅助软件工程中Ｂ技术、方法和工具集的简称;Ｂ语言是一种健全的面向实际软件过程的基于数学理论的技术;Ｂ方法所用的符号和方法支持大局部的软件过程：需求分析、规格说明、软件设计、实现和维护;Ｂ方法的指导性原那么：分层软件的逐步构造伴随着逐步的验证和校验；6.形式化程序标准描述语言简介－B语言简介13.1程序标准与程序(续)Ｂ工具盒包括有大量的工具，所有的工具集成在一个基于窗口的软件开发环境中，因而支持运用Ｂ方法开发软件的整个软件过程；Ｂ工具支持软件的逐步构造，其中的验证过程可用静态分析，动态分析采用模拟技术，正确性证明那么使用集成的定理证明器。Ｂ方法用一种简单的伪程序语言来描述需求模型、说明接口，并进行中间设计和实现；B语言就是AMN〔抽象机器符号〕，AMN支持规格说明的类型检测、动态验证、数学证明等来确保设计过程的正确。6.形式化程序标准描述语言简介－B语言简介23.1程序标准与程序(续)B方法的特点简单熟悉的符号表示法：这种符号表示法用来表达状态转换，从规格说明到编码，这种统一的形式减少了学习的难度和转换中的语法错误。模块化构造：从规格说明到实现的模块化构造允许将规格说明和验证过程分解为多个子任务来进行。大量实用的工具支持：现有大量的实用工具支持了B方法软件开发周期的所有阶段，包括动画和文档生成。成功的工业应用：B语言和方法已在很多的工业领域得到成功应用，包括实时、仿真、信息处理和工程等。6.形式化程序标准描述语言简介－B语言简介33.1程序标准与程序(续)6.Z语言、VDM、B形式化方法的比较属性ZVDMB基础谓词演算,集合论,模式偏函数,集合论最弱前置条件,集合论开发阶段规范说明规范说明,设计规范说明,设计,实现形式模式的符号表示,关系前/后置条件,函数严格的编程语言工具支持在规格说明级在规格说明级B-Toolkit,AtchierB,所有开发阶段培训支持图书、课程图书,课程实例研究、课程内容－Whereweare？程序标准、标准的描述断言与标准及{P}S{Q}程序正确性的概念程序正确性证明的过程3.2断言与标准1.断言断言就是关于事物性质的陈述。这个陈述可真可假。如“三是个质数〞用断言作为程序的注解或作为正确性命题的一局部时，常用大括号括起来。例1：写一个计算商和余数的程序程序标准：“设被除数x1是个非负整数，除数x2是个正整数，计算x1除以x2的商y1和余数y2〞又描述为：“初始条件：{x1>=0ANDx2>0},计算满足{x1=x2*y1+y2and0<=y2<x2}的整数y1和y2〞3.2断言与标准(续)一般地，一个程序标准可表示为由两个谓词构成的二元组〔P，Q〕。其中，P描述了所欲求解的问题必须满足的初始条件，它限定了输入参数的性质，称为初始断言或前置断言；Q描述了问题的最终解必须满足的性质，称为结果断言或后置断言。3.2断言与标准(续)程序断言是对程序的性质的陈述。最重要的一个程序断言为：{P}S{Q}。其中，〔P，Q〕是程序S的程序标准，S是一个程序〔或语句〕断言{P}S{Q}称为S关于〔P，Q〕的正确性断言。它的意义：“假设S开始执行时P为真，那么S的执行必终止且终止时Q为真〞3.2断言与标准(续)例：求商余程序{x1>=0andx2>0}Y2:=x1;y1:=0;{0<=y2and0<x2andx1=x2*y1+y2}Whiley2>=x2dobegin{0<=y2and0<x2<＝y2andx1=x2*y1+y2}

y2:=y2-x2;y1:=y1+1;

{0<=y2and0<x2andx1=x2*y1+y2}end;{x1=x2*y1+y2and0<=y2<x2}3.2断言与标准(续)问题：如何构造断言使他们能准确地反映不同位置上程序的性质？有了断言，如何证明他们的正确性？能否有准那么，可以从标准〔P，Q〕构造出程序S，使{P}S{Q}为真。3.2断言与标准(续)2.程序断言的进一步说明说明：在给出标准描述〔P，Q〕时，必须指明哪些量是可变的，哪些是不可变的。如果是可变的，必要时对前者还需指明其变化方式。输入参数：在程序执行前从外部获得值，但在程序执行中，其值始终保持不变的变量。一般用以x开头的标识符表示。输出变量：其值随程序的执行而不断变化的变量。一般以y开头的变量，或不以x和u开头的变量标识。辅助变量：为了描述程序变量取值变化方式而因入的变量。这些变量不得在程序中出现，用以u开头的变量表示。3.2断言与标准(续)例1.编写一个程序Swap〔y1，y2〕，功能是把y1，y2两变量的值互换。其标准:({y1=u1∧y2=u2}，{y1=u2∧y2=u1})3.2断言与标准(续)例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<n:b[i]≤b[i+1])}其中，u[m:n]代表b的任意可能初值；perm(b[m:n],u[m:n])是一个常谓词，表示b是u的一个置换。3.2断言与标准(续)程序标准总结：在做程序标准时，必须区分三种变量：输入变量、输出变量、辅助变量。作为某一个标准〔P，Q〕的实现程序S，S不得包含辅助变量，S也不得对输入参数进行任何形式的赋值，这些就是对标准〔P，Q〕和断言{P}S{Q}的语法规定。程序正确性断言{P}S{Q}的意义：“假设S的执行开始于一个满足P的状态，那么这个执行必将在有限的时间内终止于一个满足Q的状态〞。所谓一个状态是满足P〔或Q〕的，假设在此状态下P〔或Q〕为真。内容－Whereweare？程序标准、标准的表示方法断言与标准及{P}S{Q}程序正确性的概念程序正确性证明的过程3.3程序正确性概念定义1.如果对于每一个使得P(ā)为真的输入ā，程序S计算都终止，称程序S对P是终止的。定义2：对于满足P(ā)为真，且能够使程序S计算终止的每个ā，如果Q(ā,P(ā))为真，那么称程序S对于P和Q是局部正确的。记为[P]S[Q]。⊢[P]S[Q]iff(ā)((⊢p(ā)and(⊢Sterminates))⊢Q(ā,P(ā))3.3程序正确性概念(续)定义3：对于满足P(ā)为真的每个ā，如果程序S能够计算终止，且Q(ā,P(ā))为真，那么称程序S对于P和Q是完全正确的。记为{P}S{Q}⊢{P}S{Q}iff(ā)(⊢p(ā)((⊢Sterminates)

and⊢Q(ā,P(ā)))⊢[P]S[Q]iff(ā)((⊢p(ā)and(⊢Sterminates))⊢

Q(ā,P(ā))〔1〕关于局部正确性证明的方法Floyd的不变式断言法Manna的子目标断言法Hoare的公理化方法〔2〕关于终止性证明的方法Floyd的良序集方法Knuth的计数器方法Manna等人的不动点方法〔3〕关于完全正确性的证明方法Hoare的公理化方法〔Manna、Pnueli〕Bustall的间发断言法Dijkstra的弱谓词转换方法以及强验证方法。3.3程序正确性概念(续)主要的程序正确性证明方法内容－Whereweare？程序标准、标准的表示方法断言与标准及{P}S{Q}程序正确性的概念程序正确性证明的过程3.4程序的非形式化正确性证明简介设〔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,为真，并且每个蕴涵：QiPi+1，i=1，2，…,n成立，就称〔P1，Q1〕，〔P2，Q2〕，…,〔Pn，Qn〕是{P}S{Q}的一个证明。例1：3.4程序的非形式化正确性证明简介(续)例1：令〔P，Q〕为：P：{i≥0∧s=b[0]+…+b[i]}Q：{i>0∧s