第章程序规范及其正确性证明概述ppt课件.ppt
41页
第第3章章 程序规范及其正确性证明概述程序规范及其正确性证明概述 第第3章章 程序规范及其正确性证明概述程序规范及其正确性证明概述内容－内容－Where we are？？l程序规范、规范的描画程序规范、规范的描画l断言与规范及断言与规范及{P} S {Q}l程序正确性的概念程序正确性的概念l程序正确性证明的过程程序正确性证明的过程 第第3章章 程序规范及其正确性证明概述程序规范及其正确性证明概述3.1 程序规范与程序程序规范与程序1. 程序程序规范：范：程序程序设计之前，第一步必需明确之前，第一步必需明确“做什么〞做什么〞所所谓“做什么〞是指做什么〞是指对欲求解的欲求解的问题的描画程序程序规范〔范〔PS-Program Specification〕〕:关于关于“做什么〞的描画做什么〞的描画这里的里的PS仅指功能的描画，不包括指功能的描画，不包括诸如如处置速度、置速度、执行行时间、呼、呼应周期等与周期等与时间有关性能目的有关性能目的PS是是软件工程的需求分析的件工程的需求分析的结果PS的含的含义是映射，是是映射，是输入到入到输出的映射，它反映出的映射，它反映了程序了程序对数据的作用数据的作用。
第第3章章 程序规范及其正确性证明概述程序规范及其正确性证明概述3.1 程序规范与程序程序规范与程序(续续)2. 程序程序程序也是映射，是输入到计算的映射，即每一输入都对程序也是映射，是输入到计算的映射，即每一输入都对应一串计算步应一串计算步3. 程序规范与程序的关系程序规范与程序的关系给出规范后，程序开发就是建立一个程序，使得计算刚给出规范后，程序开发就是建立一个程序，使得计算刚好能实现规范的映射；好能实现规范的映射；程序验证是证明程序正确地实现了规范，即证明规范和程序验证是证明程序正确地实现了规范，即证明规范和已有程序之间的一致性已有程序之间的一致性规范规范程序程序输入输入输出输出映射映射输入输入计算计算映射映射 第第3章章 程序规范及其正确性证明概述程序规范及其正确性证明概述3.1 程序规范与程序程序规范与程序(续续)4. 程序规范的描画程序规范的描画-----规范言语规范言语规范必需用言语描画，该言语称为规范言语规范必需用言语描画，该言语称为规范言语描画一个复杂问题的输入和输出之间的关系是困难描画一个复杂问题的输入和输出之间的关系是困难的，目前对规范言语的方式尚无定论有三种方的，目前对规范言语的方式尚无定论。
有三种方式：式：自然言语：不够准确，存在二义性，必需辅以数学自然言语：不够准确，存在二义性，必需辅以数学言语一阶谓词：可以准确地描画问题的输入和输出的关一阶谓词：可以准确地描画问题的输入和输出的关系，但是规范文本比较长如系，但是规范文本比较长如Hoare系统数学言语：用数学言语可以把输入和输出的映射描数学言语：用数学言语可以把输入和输出的映射描画为函数这些函数的准确的泛函定义就构成了画为函数这些函数的准确的泛函定义就构成了问题的规范但存在过于规范的问题问题的规范但存在过于规范的问题 第第3章章 程序规范及其正确性证明概述程序规范及其正确性证明概述3.1 程序规范与程序程序规范与程序(续续)5. 一个适宜的程序规范言语应满足的根本条件一个适宜的程序规范言语应满足的根本条件:该当为描画者和运用者所直接了解；该当为描画者和运用者所直接了解；该当有严厉的数学语义该当有严厉的数学语义该当与方式方法的构造实际和程序设计言语协调该当与方式方法的构造实际和程序设计言语协调该当有较强的表达才干和通用性该当有较强的表达才干和通用性 第第3章章 程序规范及其正确性证明概述程序规范及其正确性证明概述3.1 程序规范与程序程序规范与程序(续续)lZ言语言语lVDMlB方法方法l三者的比较三者的比较6. 方式化程序规范描画言语简介方式化程序规范描画言语简介 第第3章章 程序规范及其正确性证明概述程序规范及其正确性证明概述3.1 程序规范与程序程序规范与程序(续续)lZ言语是一种基于集合论和一阶谓词逻辑的方式化言语；言语是一种基于集合论和一阶谓词逻辑的方式化言语；lZ言语支持软件的方式化规范描画，规范的推理和求精；言语支持软件的方式化规范描画，规范的推理和求精；l是迄今为止运用最广泛的方式言语之一；是迄今为止运用最广泛的方式言语之一；lZ是在是在Jean Raymond Abrial等的开创性任务下，由英国等的开创性任务下，由英国牛津大学的程序设计研讨小组〔牛津大学的程序设计研讨小组〔PRG，，Programming Research Group〕，于〕，于20世纪世纪80年代初开发；年代初开发；lPRG与与IBM的的Hursley实验室协作，将实验室协作，将Z言语用于言语用于IBM的客的客户信息控制系统的开发，使得最终的产质量量得到了全面户信息控制系统的开发，使得最终的产质量量得到了全面的的提高，所测出的错误数量大大减少，并且整体开发费的的提高，所测出的错误数量大大减少，并且整体开发费用降低了用降低了9％；％；l在在ISO指点下的国际规范化指点下的国际规范化Z任务于任务于2019年完成年完成6. 方式化程序规范描画言语简介－方式化程序规范描画言语简介－Z言语简介言语简介1 第第3章章 程序规范及其正确性证明概述程序规范及其正确性证明概述3.1 程序规范与程序程序规范与程序(续续)l提供了一种称为方式〔提供了一种称为方式〔Schema〕的构造，它是〕的构造，它是Z的根本描画单位，以此来描画一个规范阐明的的根本描画单位，以此来描画一个规范阐明的形状空间〔静态性质〕和操作〔动态行为〕。
形状空间〔静态性质〕和操作〔动态行为〕lＺ言语的方式和方式演算：Ｚ言语的方式和方式演算：l形状方式对目的软件系统的构造特征进展笼统描形状方式对目的软件系统的构造特征进展笼统描画；画；l操作方式对目的软件系统的行为特征进展笼统描操作方式对目的软件系统的行为特征进展笼统描画；画；l经过方式演算，无论多么大型系统的规格阐明都经过方式演算，无论多么大型系统的规格阐明都可以经过一个个小的部分来构成；可以经过一个个小的部分来构成；6. 方式化程序规范描画言语简介－方式化程序规范描画言语简介－Z言语简介言语简介2 第第3章章 程序规范及其正确性证明概述程序规范及其正确性证明概述3.1 程序规范与程序程序规范与程序(续续)lＺ方式阐明可以组合成新的Ｚ方式，新的ＺＺ方式阐明可以组合成新的Ｚ方式，新的Ｚ方式承继其成分方式的一切属性和约束软方式承继其成分方式的一切属性和约束软件系统的Ｚ方式规格阐明可以按一定的层次件系统的Ｚ方式规格阐明可以按一定的层次构造给出构造给出lＺ规格阐明由一系列方式组成，每个方式定Ｚ规格阐明由一系列方式组成，每个方式定义一个笼统对象或操作，并用谓词断定描画义一个笼统对象或操作，并用谓词断定描画给出新的对象或操作的语义约束。
给出新的对象或操作的语义约束l方式例方式例:6. 方式化程序规范描画言语简介－方式化程序规范描画言语简介－Z言语简介言语简介3 第第3章章 程序规范及其正确性证明概述程序规范及其正确性证明概述3.1 程序规范与程序程序规范与程序(续续)l方式例方式例1:l[Student] // 引入根本引入根本类型型studentl StudentSys //方式名方式名lEnrolled,tested: P Student // 声明部分声明部分, 学生的密集学生的密集类型型l#enrolled ≤size // 断言部分，合断言部分，合取关系取关系ltested enrolledl等价于：等价于：//程度方式程度方式lStudentSys=[enrolled,tested: P Student | #enrolled ≤size tested enrolled ]6. 方式化程序规范描画言语简介－方式化程序规范描画言语简介－Z言语简介言语简介4 第第3章章 程序规范及其正确性证明概述程序规范及其正确性证明概述3.1 程序规范与程序程序规范与程序(续续)l方式例方式例2:lEnrollStudentl StudentSys // = Studentsys StudentSys’的的简写写 lname?: Student // 在在输入入变量后加？量后加？lname? enrolled // 在在输出出变量后加！量后加！lenrolled < size // 带有后有后缀‘的的变量表示量表示操作后的操作后的变量量lenrolled’ = enrolled ∪∪{name?}ltested’= tested 6. 方式化程序规范描画言语简介－方式化程序规范描画言语简介－Z言语简介言语简介5 第第3章章 程序规范及其正确性证明概述程序规范及其正确性证明概述3.1 程序规范与程序程序规范与程序(续续)l缺陷缺陷:l⑴⑴ Ｚ言Ｚ言语对大型系大型系统的模的模块化才干缺乏。
化才干缺乏l⑵⑵ 难以以识别影响某一形状方式的一切操作方式影响某一形状方式的一切操作方式l⑶⑶ 不能支持不能支持规格格阐明的重用明的重用l⑷⑷ Ｚ言Ｚ言语难以由以由计算机直接算机直接处置l短少商品化的工具支持等到短少商品化的工具支持等到诸多多缘由由6. 方式化程序规范描画言语简介－方式化程序规范描画言语简介－Z言语简介言语简介6 第第3章章 程序规范及其正确性证明概述程序规范及其正确性证明概述3.1 程序规范与程序程序规范与程序(续续)l VDM〔Vienna Development Method〕是在1969年为开发PL/1言语时，由IBM公司维也纳实验室的研讨小组提出的初衷是为了描画PL/1言语的语义lVDM是一种功能构造性规格阐明技术，它经过一阶谓词逻辑和已建立的笼统数据类型来描画每个运算或函数的功能l这种方法在90年代初在欧美许多研讨机构或大学得到了广泛的运用如曼彻斯特大学将其作为CS的必修课 l2019年ISO制定了VDM的国际规范化版本VDM-SL6. 方式化程序规范描画言语简介－方式化程序规范描画言语简介－VDM简介简介1 第第3章章 程序规范及其正确性证明概述程序规范及其正确性证明概述3.1 程序规范与程序程序规范与程序(续续)lVDM技术的根本思想：技术的根本思想：l运用笼统数据类型、数学概念和符号来规定运运用笼统数据类型、数学概念和符号来规定运算或函数的功能；算或函数的功能；l可使软件系统的功能描画在笼统级上进展，完可使软件系统的功能描画在笼统级上进展，完全摆脱了实现细节，这样为软件实现者提供了全摆脱了实现细节，这样为软件实现者提供了很大的灵敏性；很大的灵敏性；l这种方式化规格阐明还为程序正确性证明提供这种方式化规格阐明还为程序正确性证明提供了根据。
了根据6. 方式化程序规范描画言语简介－方式化程序规范描画言语简介－VDM简介简介2 第第3章章 程序规范及其正确性证明概述程序规范及其正确性证明概述3.1 程序规范与程序程序规范与程序(续续)lVDM支持两种笼统：数据笼统和操作笼统支持两种笼统：数据笼统和操作笼统l一个一个VDM规范有以下不同的块组成：规范有以下不同的块组成：ltypesl
生了运算冗余l⑵⑵ VDM目前目前还未能建立一整套描画未能建立一整套描画机制，将一个大型系机制，将一个大型系统分解分解为许多多运算而描画出运算而描画出这些运算之些运算之间的关系的关系l⑶⑶ VDM方式方式规格格阐明明过于方式化不于方式化不容易了解容易了解6. 方式化程序规范描画言语简介－方式化程序规范描画言语简介－VDM简介简介4 第第3章章 程序规范及其正确性证明概述程序规范及其正确性证明概述3.1 程序规范与程序程序规范与程序(续续)lB方法是方法是20世纪世纪80年代初中期由年代初中期由J.R.Abrial以及以及BP研研讨中心的讨中心的MATRA和和GE Alsthom研讨小组开发的研讨小组开发的lＢ言语是计算机辅助软件工程中Ｂ技术、方法和工具Ｂ言语是计算机辅助软件工程中Ｂ技术、方法和工具集的简称集的简称;lＢ言语是一种健全的面向实践软件过程的基于数学实Ｂ言语是一种健全的面向实践软件过程的基于数学实际的技术际的技术;lＢ方法所用的符号和方法支持大部分的软件过程：需Ｂ方法所用的符号和方法支持大部分的软件过程：需求分析、规格阐明、软件设计、实现和维护求分析、规格阐明、软件设计、实现和维护;lＢ方法的指点性原那么：分层软件的逐渐构造伴随着Ｂ方法的指点性原那么：分层软件的逐渐构造伴随着逐渐的验证和校验；逐渐的验证和校验；6. 方式化程序规范描画言语简介－方式化程序规范描画言语简介－B言语简介言语简介1 第第3章章 程序规范及其正确性证明概述程序规范及其正确性证明概述3.1 程序规范与程序程序规范与程序(续续)lＢ工具盒包括有大量的工具，一切的工具集成在一个基Ｂ工具盒包括有大量的工具，一切的工具集成在一个基于窗口的软件开发环境中，因此支持运用Ｂ方法开发软于窗口的软件开发环境中，因此支持运用Ｂ方法开发软件的整个软件过程；件的整个软件过程；lＢ工具支持软件的逐渐构造，其中的验证过程可用静态Ｂ工具支持软件的逐渐构造，其中的验证过程可用静态分析，动态分析采用模拟技术，正确性证明那么运用集分析，动态分析采用模拟技术，正确性证明那么运用集成的定理证明器。
成的定理证明器lＢ方法用一种简单的伪程序文语来描画需求模型、阐明Ｂ方法用一种简单的伪程序文语来描画需求模型、阐明接口，并进展中间设计和实现；接口，并进展中间设计和实现；lB言语就是言语就是AMN〔笼统机器符号〕，〔笼统机器符号〕，AMN支持规格阐明支持规格阐明的类型检测、动态验证、数学证明等来确保设计过程的的类型检测、动态验证、数学证明等来确保设计过程的正确6. 方式化程序规范描画言语简介－方式化程序规范描画言语简介－B言语简介言语简介2 第第3章章 程序规范及其正确性证明概述程序规范及其正确性证明概述3.1 程序规范与程序程序规范与程序(续续)lB方法的特点方法的特点l简单熟习的符号表示法：这种符号表示法用来表达形状转简单熟习的符号表示法：这种符号表示法用来表达形状转换，从规格阐明到编码，这种一致的方式减少了学习的难换，从规格阐明到编码，这种一致的方式减少了学习的难度和转换中的语法错误度和转换中的语法错误l模块化构造：从规格阐明到实现的模块化构造允许将规格模块化构造：从规格阐明到实现的模块化构造允许将规格阐明和验证过程分解为多个子义务来进展阐明和验证过程分解为多个子义务来进展l大量适用的工具支持：现有大量的适用工具支持了大量适用的工具支持：现有大量的适用工具支持了B方法方法软件开发周期的一切阶段，包括动画和文档生成。
软件开发周期的一切阶段，包括动画和文档生成l胜利的工业运用：胜利的工业运用：B言语和方法已在很多的工业领域得到言语和方法已在很多的工业领域得到胜利运用，包括实时、仿真、信息处置和工程等胜利运用，包括实时、仿真、信息处置和工程等6. 方式化程序规范描画言语简介－方式化程序规范描画言语简介－B言语简介言语简介3 第第3章章 程序规范及其正确性证明概述程序规范及其正确性证明概述3.1 程序规范与程序程序规范与程序(续续)6. Z言语、言语、VDM、、B方式化方法的比较方式化方法的比较属性属性ZVDMB基础基础谓词演算谓词演算, 集合论集合论, 模模式式偏函数偏函数, 集集合论合论最弱前置条件最弱前置条件, 集合集合论论开发阶段开发阶段规范说明规范说明规范说明规范说明, 设计设计规范说明规范说明, 设计设计, 实实现现形式形式模式的符号模式的符号表示表示, 关系关系前前/后置条后置条件件, 函数函数严格的编程语言严格的编程语言工具支持工具支持在规格说明在规格说明级级在规格说在规格说明级明级B-Toolkit,AtchierB,所有开发阶段所有开发阶段培训支持培训支持图书、课程图书、课程图书图书, 课程课程实例研究、课程实例研究、课程 第第3章章 程序规范及其正确性证明概述程序规范及其正确性证明概述内容－内容－Where we are？？l程序规范、规范的描画程序规范、规范的描画l断言与规范及断言与规范及{P} S {Q}l程序正确性的概念程序正确性的概念l程序正确性证明的过程程序正确性证明的过程 第第3章章 程序规范及其正确性证明概述程序规范及其正确性证明概述3.2 断言与规范断言与规范1. 断言断言断言就是关于事物性断言就是关于事物性质的的陈说。
这个个陈说可真可假可真可假如如“三是个三是个质数〞数〞用断言作用断言作为程序的注解或作程序的注解或作为正确性命正确性命题的一部分的一部分时，常用大括号括起来常用大括号括起来例例1：写一个：写一个计算商和余数的程序算商和余数的程序程序程序规范：范：“设被除数被除数x1是个非是个非负整数，除数整数，除数x2是个是个正整数，正整数，计算算x1除以除以x2的商的商y1和余数和余数y2〞〞又描画又描画为：：“初始条件：初始条件：{x1>=0 AND x2>0}, 计算算满足足{x1=x2*y1+y2 and 0<=y2 果断言或后置断言 第第3章章 程序规范及其正确性证明概述程序规范及其正确性证明概述3.2 断言与规范断言与规范(续续)l程序断言是程序断言是对程序的性程序的性质的的陈说l最重要的一个程序断言最重要的一个程序断言为：：{P} S {Q}其中，〔中，〔P，，Q〕是程序〕是程序S的程序的程序规范，范，S是一是一个程序〔或个程序〔或语句〕句〕l断言断言{P} S {Q}称称为S关于〔关于〔P，，Q〕的正确〕的正确性断言l它的意它的意义：：“假假设S开开场执行行时P为真，那真，那么么S的的执行必行必终止且止且终止止时Q为真〞真〞 第第3章章 程序规范及其正确性证明概述程序规范及其正确性证明概述3.2 断言与规范断言与规范(续续)l例：求商余程序例：求商余程序l{x1>=0 and x2>0}lY2:=x1; y1:=0;l{0<=y2 and 0 为真 第第3章章 程序规范及其正确性证明概述程序规范及其正确性证明概述3.2 断言与规范断言与规范(续续)2. 程序断言的进一步阐明程序断言的进一步阐明阐明：在给出规范描画〔阐明：在给出规范描画〔P，，Q〕时，必需指明哪〕时，必需指明哪些量是可变的，哪些是不可变的假设是可变的，些量是可变的，哪些是不可变的假设是可变的，必要时对前者还需指明其变化方式必要时对前者还需指明其变化方式输入参数：在程序执行前从外部获得值，但在程序输入参数：在程序执行前从外部获得值，但在程序执行中，其值一直坚持不变的变量普通用以执行中，其值一直坚持不变的变量普通用以x开头的标识符表示开头的标识符表示输出变量：其值随程序的执行而不断变化的变量输出变量：其值随程序的执行而不断变化的变量普通以普通以y开头的变量，或不以开头的变量，或不以x和和u开头的变量标开头的变量标识辅助变量：为了描画程序变量取值变化方式而因入辅助变量：为了描画程序变量取值变化方式而因入的变量这些变量不得在程序中出现，用以的变量这些变量不得在程序中出现，用以u开开头的变量表示头的变量表示 第第3章章 程序规范及其正确性证明概述程序规范及其正确性证明概述3.2 断言与规范断言与规范(续续)l例例1. 编写一个程序写一个程序Swap〔〔y1，，y2〕，功能是〕，功能是把把y1，，y2两两变量的量的值互互换。 l其其规范范:l ({y1=u1∧∧ y2=u2}，，{y1=u2∧∧y2=u1}) 第第3章章 程序规范及其正确性证明概述程序规范及其正确性证明概述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章章 程序规范及其正确性证明概述程序规范及其正确性证明概述3.2 断言与规范断言与规范(续续)l程序程序规范范总结：：l在做程序在做程序规范范时，必需区分三种，必需区分三种变量：量：输入入变量、量、输出出变量、量、辅助助变量。 作量作为某一个某一个规范〔范〔P，，Q〕〕的的实现程序程序S，，S不得包含不得包含辅助助变量，量，S也不得也不得对输入参数入参数进展任何方式的展任何方式的赋值，，这些就是些就是对规范范〔〔P，，Q〕和断言〕和断言{P}S{Q}的的语法法规定l程序正确性断言程序正确性断言{P} S {Q}的意的意义：：l“假假设S的的执行开行开场于一个于一个满足足P的形状，那么的形状，那么这个个执行必将在有限的行必将在有限的时间内内终止于一个止于一个满足足Q的的形状〞l所所谓一个形状是一个形状是满足足P〔或〔或Q〕的，假〕的，假设在此形状在此形状下下P〔或〔或Q〕〕为真 第第3章章 程序规范及其正确性证明概述程序规范及其正确性证明概述内容－内容－Where we are？？l程序规范、规范的表示方法程序规范、规范的表示方法l断言与规范及断言与规范及{P} S {Q}l程序正确性的概念程序正确性的概念l程序正确性证明的过程程序正确性证明的过程 第第3章章 程序规范及其正确性证明概述程序规范及其正确性证明概述3.3 程序正确性概念程序正确性概念l定定义1. 假假设对于每一个使得于每一个使得P(ā)为真的真的输入入ā ，程序，程序S计算都算都终止，称程序止，称程序S对P是是终止的。 止的l定定义2：：对于于满足足P(ā)为真，且可以使程序真，且可以使程序S计算算终止的每个止的每个ā，假，假设Q(ā, P(ā))为真，那么称程真，那么称程序序S对于于P和和Q是部分正确的是部分正确的记为[P] S [Q]l ⊢ ⊢ [P] S [Q] iff l (ā)((⊢ ⊢p(ā) and (⊢ ⊢ S terminates))l ⊢ ⊢ Q(ā, P(ā)) 第第3章章 程序规范及其正确性证明概述程序规范及其正确性证明概述3.3 程序正确性概念程序正确性概念(续续)l定定义3：：对于于满足足P(ā)为真的每个真的每个ā ，假，假设程序程序S可以可以计算算终止，且止，且Q(ā, P(ā))为真，那么称程真，那么称程序序S对于于P和和Q是完全正确的是完全正确的记为 {P} S{Q}l ⊢ ⊢ {P} S{Q} iff l ( ā)(⊢ ⊢p(ā) ((⊢ ⊢ S terminates) and ⊢ ⊢ Q(ā, P(ā)))⊢ ⊢ [P] S [Q] iff (ā)((⊢ ⊢p(ā) and (⊢ ⊢ S terminates))⊢ ⊢ Q(ā, P(ā)) 第第3章章 程序规范及其正确性证明概述程序规范及其正确性证明概述〔〔1〕关于部分正确性〕关于部分正确性证明的方法明的方法Floyd 的不的不变式断言法式断言法Manna的子目的断言法的子目的断言法Hoare的公理化方法的公理化方法〔〔2〕关于〕关于终止性止性证明的方法明的方法Floyd的良序集方法的良序集方法Knuth的的计数器方法数器方法Manna等人的不等人的不动点方法点方法〔〔3〕关于完全正确性的〕关于完全正确性的证明方法明方法Hoare的公理化方法〔的公理化方法〔Manna、、Pnueli〕〕Bustall的的间发断言法断言法Dijkstra的弱的弱谓词转换方法以及方法以及强验证方法。 方法3.3 程序正确性概念程序正确性概念(续续)主要的程序正确性证明方法主要的程序正确性证明方法 第第3章章 程序规范及其正确性证明概述程序规范及其正确性证明概述内容－内容－Where we are？？l程序规范、规范的表示方法程序规范、规范的表示方法l断言与规范及断言与规范及{P} S {Q}l程序正确性的概念程序正确性的概念l程序正确性证明的过程程序正确性证明的过程 第第3章章 程序规范及其正确性证明概述程序规范及其正确性证明概述3.4 程序的非方式化正确性证明简介程序的非方式化正确性证明简介l设〔〔P，，Q〕是一个〕是一个规范，范，S是按照是按照这个个规范要求范要求设计的程的程序，且是由序，且是由语句句s1，，s2，，…，，sn组成的一个枚成的一个枚举型程序〔型程序〔即其即其执行等于行等于组成它的各个成它的各个语句的逐一句的逐一顺序的序的执行，其中行，其中的每个的每个语句都只需一个入口和一个出口，且没有句都只需一个入口和一个出口，且没有GOTO语句〕令P1,Q1,P2,Q2,…,Pn,Qn是是2n个个谓词，且，且P=P1，，Q=Qnl假假设一切断言一切断言 {Pi} Si {Qi}，，i=1，，2，，…,n,为真，并且真，并且l每个每个蕴涵：涵： Qi Pi+1，， i=1，，2，，…,n 成立，成立，l就称〔就称〔P1，，Q1〕，〕， 〔〔P2，，Q2〕，〕，…, 〔〔Pn，，Qn〕是〕是{P}S{Q}的一个的一个证明。 明l例例1：： 第第3章章 程序规范及其正确性证明概述程序规范及其正确性证明概述3.4 程序的非方式化正确性证明简介程序的非方式化正确性证明简介(续续)l例例1：令〔：令〔P，，Q〕〕为：：l P：：{i≥0∧∧s=b[0]+…+b[i]} l Q：：{i>0 ∧∧ s=b[0]+…+b[i]}l 令令S为：： i := i+1 ; s :=s+b[i]l 简单证明如下：明如下：l {P：：i≥0∧∧s=b[0]+…+b[i]}l {P1：： i+1>0∧∧s=b[0]+…+b[i+1-1]}l i := i+1 ;l {Q1: i>0∧∧s=b[0]+…+b[i-1]}l {P2: i>0∧∧s+b[i]=b[0]+…+b[i-1] +b[i]}l s :=s+b[i]l {Q: i>0 ∧∧ s=b[0]+…+b[i]}这个证明梗概意味着下面各断这个证明梗概意味着下面各断言依次为真：言依次为真：P P1{P1} i := i+1 {Q1}Q1 P2{P2} s :=s+b[i] {Q}只需证明上面的只需证明上面的4个断言为真，个断言为真，就可以证明就可以证明{P} S {Q}为真。 为真 第第3章章 程序规范及其正确性证明概述程序规范及其正确性证明概述思索练习思索练习写出下面问题的规范写出下面问题的规范:计算一个整数的绝对值；计算一个整数的绝对值；求两个整数的最大值；求两个整数的最大值；求两个非负整数的最大公约数；求两个非负整数的最大公约数；置置y等于数组等于数组b[0:n-1]中的最大值的位置；中的最大值的位置；断定一个大于断定一个大于1的整数能否素数；的整数能否素数；判别数组判别数组b[0:n-1]能否已排序了；能否已排序了；求数组求数组a[0:n-1]与与b[0:n-1]的内积的内积 第第3章章 程序规范及其正确性证明概述程序规范及其正确性证明概述作业：作业：l1. 编程编程l输入：输入一个文件，至多包含输入：输入一个文件，至多包含n个正整数，每个正整数，每个正整数都不大于个正整数都不大于n，例如，，例如，n＝＝10**7.假设输入假设输入时某个整数出现两次，就会产生一个致命的错误时某个整数出现两次，就会产生一个致命的错误这些整数与其他任何整数都不关联这些整数与其他任何整数都不关联l输出：以增序方式输出经过排序的整数列表输出：以增序方式输出经过排序的整数列表l约束：至多只需约束：至多只需1MB的可用内存；但是磁盘空间的可用内存；但是磁盘空间足够。 运转时间只允许几分钟；足够运转时间只允许几分钟；10秒钟是最适宜秒钟是最适宜的运转时间的运转时间l要求：写出实现方案；实现要求：写出实现方案；实现 第第3章章 程序规范及其正确性证明概述程序规范及其正确性证明概述小结小结l程序规范、规范的表示方法程序规范、规范的表示方法l断言与规范及断言与规范及{P} S {Q}l程序正确性的概念程序正确性的概念l完全正确性、部分正确性、终止性完全正确性、部分正确性、终止性l程序正确性证明的过程程序正确性证明的过程l证明证明{P} S {Q}成立的过程成立的过程 。
