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

第3章 程序规范及其正确性证明概述,内容Where we are？,程序规范、规范的描述断言与规范及P S Q程序正确性的概念程序正确性证明的过程,3.1 程序规范与程序,1.程序规范：程序设计之前，第一步必须明确“做什么”。所谓“做什么”是指对欲求解的问题的描述。程序规范（PS-Program Specification）:关于“做什么”的描述。这里的PS仅指功能的描述，不包括诸如处理速度、执行时间、响应周期等与时间有关性能指标。PS是软件工程的需求分析的结果。PS的含义是映射，是输入到输出的映射，它反映了程序对数据的作用。,3.1 程序规范与程序(续),2.程序程序也是映射，是输入到计算的映射，即每一输入都对应一串计算步。3.程序规范与程序的关系给出规范后，程序开发就是建立一个程序，使得计算刚好能实现规范的映射；程序验证是证明程序正确地实现了规范，即证明规范和已有程序之间的一致性,3.1 程序规范与程序(续),4.程序规范的描述-规范语言规范必须用语言描述，该语言称为规范语言。描述一个复杂问题的输入和输出之间的关系是困难的，目前对规范语言的模式尚无定论。有三种模式：自然语言：不够准确，存在二义性，必须辅以数学语言。一阶谓词：可以精确地描述问题的输入和输出的关系，但是规范文本比较长。如Hoare系统。数学语言：用数学语言可以把输入和输出的映射描述为函数。这些函数的精确的泛函定义就构成了问题的规范。但存在过于规范的问题。,3.1 程序规范与程序(续),5.一个合适的程序规范语言应满足的基本条件:应当为描述者和使用者所直接理解；应当有严格的数学语义应当与形式方法的构造理论和程序设计语言协调应当有较强的表达能力和通用性,3.1 程序规范与程序(续),Z语言VDMB方法三者的比较,6.形式化程序规范描述语言简介,3.1 程序规范与程序(续),Z语言是一种基于集合论和一阶谓词逻辑的形式化语言；Z语言支持软件的形式化规范描述，规范的推理和求精；是迄今为止应用最广泛的形式语言之一；Z是在Jean Raymond Abrial等的开创性工作下，由英国牛津大学的程序设计研究小组（PRG，Programming Research Group），于20世纪80年代初开发；PRG与IBM的Hursley实验室合作，将Z语言用于IBM的客户信息控制系统的开发，使得最终的产品质量得到了全面的的提高，所测出的错误数量大大减少，并且整体开发费用降低了9；在ISO指导下的国际标准化Z工作于2002年完成,6.形式化程序规范描述语言简介Z语言简介1,3.1 程序规范与程序(续),提供了一种称为模式（Schema）的结构，它是Z的基本描述单位，以此来描述一个规范说明的状态空间（静态性质）和操作（动态行为）。语言的模式和模式演算：状态模式对目标软件系统的结构特征进行抽象描述；操作模式对目标软件系统的行为特征进行抽象描述；通过模式演算，无论多么大型系统的规格说明都可以通过一个个小的部分来构成；,6.形式化程序规范描述语言简介Z语言简介2,3.1 程序规范与程序(续),模式说明可以组合成新的模式，新的模式继承其成分模式的一切属性和约束。软件系统的模式规格说明可以按一定的层次结构给出。规格说明由一系列模式组成，每个模式定义一个抽象对象或操作，并用谓词判定描述给出新的对象或操作的语义约束。模式例:,6.形式化程序规范描述语言简介Z语言简介3,3.1 程序规范与程序(续),模式例1:Student/引入基本类型student StudentSys/模式名Enrolled,tested:P Student/声明部分,学生的密集类型#enrolled size/断言部分，合取关系tested enrolled等价于：/水平方式StudentSys=enrolled,tested:P Student|#enrolled size tested enrolled,6.形式化程序规范描述语言简介Z语言简介4,3.1 程序规范与程序(续),模式例2:EnrollStudentStudentSys/=Studentsys StudentSys的简写 name?:Student/在输入变量后加？name?enrolled/在输出变量后加！enrolled size/带有后缀的变量表示操作后的变量enrolled=enrolled name?tested=tested,6.形式化程序规范描述语言简介Z语言简介5,3.1 程序规范与程序(续),缺点:语言对大型系统的模块化能力不足。难以识别影响某一状态模式的所有操作模式。不能支持规格说明的重用。语言难以由计算机直接处理。缺少商品化的工具支持等到诸多原因,6.形式化程序规范描述语言简介Z语言简介6,3.1 程序规范与程序(续),VDM（Vienna Development Method）是在1969年为开发PL/1语言时，由IBM公司维也纳实验室的研究小组提出的。初衷是为了描述PL/1语言的语义。VDM是一种功能构造性规格说明技术，它通过一阶谓词逻辑和已建立的抽象数据类型来描述每个运算或函数的功能。这种方法在90年代初在欧美许多研究机构或大学得到了广泛的应用。如曼彻斯特大学将其作为CS的必修课。1996年ISO制订了VDM的国际标准化版本VDM-SL,6.形式化程序规范描述语言简介VDM简介1,3.1 程序规范与程序(续),VDM技术的基本思想：运用抽象数据类型、数学概念和符号来规定运算或函数的功能；可使软件系统的功能描述在抽象级上进行，完全摆脱了实现细节，这样为软件实现者提供了很大的灵活性；这种形式化规格说明还为程序正确性证明提供了依据。,6.形式化程序规范描述语言简介VDM简介2,3.1 程序规范与程序(续),VDM支持两种抽象：数据抽象和操作抽象。一个VDM规范有以下不同的块组成：typesvaluesfunctionsoperationsstate ofend,6.形式化程序规范描述语言简介VDM简介3,3.1 程序规范与程序(续),缺点：由于VDM对抽象数据类型预先定义了运算，而某些用户定义的类型在规格说明描述中无需这么多运算，因而产生了运算冗余。VDM目前还未能建立一整套描述机制，将一个大型系统分解为许多运算而描述出这些运算之间的关系 VDM形式规格说明过于形式化不容易理解,6.形式化程序规范描述语言简介VDM简介4,3.1 程序规范与程序(续),B方法是20世纪80年代初中期由以及BP研究中心的MATRA和GE Alsthom研究小组开发的。语言是计算机辅助软件工程中技术、方法和工具集的简称;语言是一种健全的面向实际软件过程的基于数学理论的技术;方法所用的符号和方法支持大部分的软件过程：需求分析、规格说明、软件设计、实现和维护;方法的指导性原则：分层软件的逐步构造伴随着逐步的验证和校验；,6.形式化程序规范描述语言简介B语言简介1,3.1 程序规范与程序(续),工具盒包括有大量的工具，所有的工具集成在一个基于窗口的软件开发环境中，因而支持运用方法开发软件的整个软件过程；工具支持软件的逐步构造，其中的验证过程可用静态分析，动态分析采用模拟技术，正确性证明则使用集成的定理证明器。方法用一种简单的伪程序语言来描述需求模型、说明接口，并进行中间设计和实现；B语言就是AMN（抽象机器符号），AMN支持规格说明的类型检测、动态验证、数学证明等来确保设计过程的正确。,6.形式化程序规范描述语言简介B语言简介2,3.1 程序规范与程序(续),B方法的特点简单熟悉的符号表示法：这种符号表示法用来表达状态转换，从规格说明到编码，这种统一的形式减少了学习的难度和转换中的语法错误。模块化构造：从规格说明到实现的模块化构造允许将规格说明和验证过程分解为多个子任务来进行。大量实用的工具支持：现有大量的实用工具支持了B方法软件开发周期的所有阶段，包括动画和文档生成。成功的工业应用：B语言和方法已在很多的工业领域得到成功应用，包括实时、仿真、信息处理和工程等。,6.形式化程序规范描述语言简介B语言简介3,3.1 程序规范与程序(续),6.Z语言、VDM、B形式化方法的比较,内容Where we are？,程序规范、规范的描述断言与规范及P S Q程序正确性的概念程序正确性证明的过程,3.2 断言与规范,1.断言断言就是关于事物性质的陈述。这个陈述可真可假。如“三是个质数”用断言作为程序的注解或作为正确性命题的一部分时，常用大括号括起来。例1：写一个计算商和余数的程序程序规范：“设被除数x1是个非负整数，除数x2是个正整数，计算x1除以x2的商y1和余数y2”又描述为：“初始条件：x1=0 AND x20,计算满足x1=x2*y1+y2 and 0=y2x2的整数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=0 and x20Y2:=x1;y1:=0;0=x2 do begin 0=y2 and 0 x2y2 and x1=x2*y1+y2 y2:=y2-x2;y1:=y1+1;0=y2 and 0 x2 and x1=x2*y1+y2 end;x1=x2*y1+y2 and 0=y2x2,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=u2y2=u1),3.2 断言与规范(续),例2：对数组bm：n进行排序的程序。功能是把数组bm：n各元素的值从小到大排列起来，使得最后的数组满足bi bi+1，i=m，,n-1。规范：P：m n bm:n=um:n Q：m n perm(bm:n,um:n)(i:m i n:bi bi+1)其中，um:n代表b的任意可能初值；perm(bm:n,um:n)是一个常谓词，表示b是u的一个置换。,3.2 断言与规范(续),程序规范总结：在做程序规范时，必须区分三种变量：输入变量、输出变量、辅助变量。作为某一个规范（P，Q）的实现程序S，S不得包含辅助变量，S也不得对输入参数进行任何形式的赋值，这些就是对规范（P，Q）和断言PSQ的语法规定。程序正确性断言P S Q的意义：“若S的执行开始于一个满足P的状态，那么这个执行必将在有限的时间内终止于一个满足Q的状态”。所谓一个状态是满足P（或Q）的，若在此状态下P（或Q）为真。,内容Where we are？,程序规范、规范的表示方法断言与规范及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(S terminates)Q(,P(),3.3 程序正确性概念(续),定义3：对于满足P()为真的每个，如果程序S能够计算终止，且Q(,P()为真，则称程序S对于P和Q是完全正确的。记为 P SQ P SQ iff()(p()(S terminates)and Q(,P(),P S Q iff()(p()and(S terminates)Q(,P(),（1）关于部分正确性证明的方法Floyd 的不变式断言法Manna的子目标断言法Hoare的公理化方法（2）关于终止性证明的方法Floyd的良序集方法Knuth的计数器方法Manna等人的不动点方法（3）关于完全正确性的证明方法Hoare的公理化方法（Manna、Pnueli）Bustall的间发断言法Dijkstra的弱谓词转换方法以及强验证方法。,3.3 程序正确性概念(续),主要的程序正确性证明方法,内容Where we are？,程序规范、规范的表示方法断言与规范及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,为真，并且每个蕴涵：Qi Pi+1，i=1，2，,n 成立，就称（P1，Q1），（P2，Q2），,（Pn，Qn）是PSQ的一个证明。例1：,3.4 程序的非形式化正确性证明简介(续),例1：令（P，Q）为：P：i0s=b0+bi Q：i0 s=b0+bi 令S为：i:=i+1;s:=s+bi 简单证明如下：P：i0s=b0+bi P1：i+10s=b0+bi+1-1 i:=i+1;Q1:i0s=b0+bi-1 P2:i0s+bi=b0+bi-1+bi s:=s+bi Q:i0 s=b0+bi,这个证明梗概意味着下面各断言依次为真：P P1P1 i:=i+1 Q1Q1 P2P2 s:=s+bi Q只要证明上面的4个断言为真，就可以证明P S Q为真。,思考练习,写出下面问题的规范:计算一个整数的绝对值；求两个整数的最大值；求两个非负整数的最大公约数；置y等于数组b0:n-1中的最大值的位置；判定一个大于1的整数是否素数；判断数组b0:n-1是否已排序了；求数组a0:n-1与b0:n-1的内积,作业：,1.编程输入：输入一个文件，至多包含n个正整数，每个正整数都不大于n，例如，n10*7.如果输入时某个整数出现两次，就会产生一个致命的错误。这些整数与其他任何整数都不关联输出：以增序形式输出经过排序的整数列表约束：至多只有1MB的可用内存；但是磁盘空间足够。运行时间只允许几分钟；10秒钟是最适宜的运行时间要求：写出实现方案；实现,小结,程序规范、规范的表示方法断言与规范及P S Q程序正确性的概念完全正确性、部分正确性、终止性程序正确性证明的过程证明P S Q成立的过程,