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

第3章程序规范及其正确性证明概述

内容－Whereweare？程序规范、规范的描述断言与规范及{P}S{Q}程序正确性的概念程序正确性证明的过程

程序设计之前，第一步必须明确“做什么”。所谓“做什么”是指对欲求解的问题的描述。程序规范（PS-ProgramSpecification）:关于“做什么”的描述。01这里的PS仅指功能的描述，不包括诸如处理速度、执行时间、响应周期等与时间有关性能指标。PS是软件工程的需求分析的结果。PS的含义是映射，是输入到输出的映射，它反映了程序对数据的作用。02程序规范：3.1程序规范与程序

3.1程序规范与程序(续)2.程序程序也是映射，是输入到计算的映射，即每一输入都对应一串计算步。3.程序规范与程序的关系给出规范后，程序开发就是建立一个程序，使得计算刚好能实现规范的映射；程序验证是证明程序正确地实现了规范，即证明规范和已有程序之间的一致性规范程序输入输出映射输入计算映射

STEP5STEP4STEP3STEP2STEP1规范必须用语言描述，该语言称为规范语言。描述一个复杂问题的输入和输出之间的关系是困难的，目前对规范语言的模式尚无定论。有三种模式：自然语言：不够准确，存在二义性，必须辅以数学语言。一阶谓词：可以精确地描述问题的输入和输出的关系，但是规范文本比较长。如Hoare系统。数学语言：用数学语言可以把输入和输出的映射描述为函数。这些函数的精确的泛函定义就构成了问题的规范。但存在过于规范的问题。程序规范的描述-----规范语言3.1程序规范与程序(续)当有严格的数学语义应当与形式方法的构造理论和程序设计语言协调应当有较强的表达能力和通用性应当为描述者和使用者所直接理解；一个合适的程序规范语言应满足的基本条件:3.1程序规范与程序(续)

3.1程序规范与程序(续)Z语言VDMB方法三者的比较6.形式化程序规范描述语言简介

Z语言是一种基于集合论和一阶谓词逻辑的形式化语言；是迄今为止应用最广泛的形式语言之一；PRG与IBM的Hursley实验室合作，将Z语言用于IBM的客户信息控制系统的开发，使得最终的产品质量得到了全面的的提高，所测出的错误数量大大减少，并且整体开发费用降低了9％；Z语言支持软件的形式化规范描述，规范的推理和求精；Z是在JeanRaymondAbrial等的开创性工作下，由英国牛津大学的程序设计研究小组（PRG，ProgrammingResearchGroup），于20世纪80年代初开发；在ISO指导下的国际标准化Z工作于2002年完成6.形式化程序规范描述语言简介－Z语言简介13.1程序规范与程序(续)

6.形式化程序规范描述语言简介－Z语言简介23.1程序规范与程序(续)提供了一种称为模式（Schema）的结构，它是Z的基本描述单位，以此来描述一个规范说明的状态空间（静态性质）和操作（动态行为）。Ｚ语言的模式和模式演算：状态模式对目标软件系统的结构特征进行抽象描述；操作模式对目标软件系统的行为特征进行抽象描述；通过模式演算，无论多么大型系统的规格说明都可以通过一个个小的部分来构成；

Ｚ模式说明可以组合成新的Ｚ模式，新的Ｚ模式继承其成分模式的一切属性和约束。软件系统的Ｚ模式规格说明可以按一定的层次结构给出。Ｚ规格说明由一系列模式组成，每个模式定义一个抽象对象或操作，并用谓词判定描述给出新的对象或操作的语义约束。模式例:6.形式化程序规范描述语言简介－Z语言简介33.1程序规范与程序(续)

3.1程序规范与程序(续)模式例1:[Student]//引入基本类型studentStudentSys//模式名Enrolled,tested:PStudent//声明部分,学生的密集类型#enrolled≤size//断言部分，合取关系tested?enrolled等价于：//水平方式StudentSys=[enrolled,tested:PStudent|

#enrolled≤size?tested?enrolled]6.形式化程序规范描述语言简介－Z语言简介4

3.1程序规范与程序(续)模式例2:EnrollStudent?StudentSys//=Studentsys?StudentSys’的简写name?:Student//在输入变量后加？name??enrolled//在输出变量后加！enrolledsize