PM-06-Chap03-程序规范及其正确性证明概述

《PM-06-Chap03-程序规范及其正确性证明概述》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、第3章程序规范及其正确性证明概述鲍玉斌东北大学信息学院计算机软件与理论研究所24July20211内容－Whereweare？程序规范、规范的描述断言与规范及{P}S{Q}程序正确性的概念程序正确性证明的过程2005年3月3日星期四2鲍玉斌东大信息学院计算机软件所程序设计方法学AllRightsReserved3.1程序规范与程序1.程序规范：程序设计之前，第一步必须明确“做什么”。所谓“做什么”是指对欲求解的问题的描述。程序规范（PS-ProgramSpecification）:关于“做什么”的描述。这里的PS仅指功能的描述，不包括诸如处理速度、执行时间、响应周期等

2、与时间有关性能指标。PS是软件工程的需求分析的结果。PS的含义是映射，是输入到输出的映射，它反映了程序对数据的作用。2005年3月3日星期四3鲍玉斌东大信息学院计算机软件所程序设计方法学AllRightsReserved3.1程序规范与程序(续)2.程序程序也是映射，是输入到计算的映射，即每一输入都对应一串计算步。3.程序规范与程序的关系给出规范后，程序开发就是建立一个程序，使得计算刚好能实现规范的映射；程序验证是证明程序正确地实现了规范，即证明规范和已有程序之间的一致性规范程序输入输出映射输入计算映射2005年3月3日星期四4鲍玉斌东大信息学院计算机软件所程序设计方

3、法学AllRightsReserved3.1程序规范与程序(续)4.程序规范的描述-----规范语言规范必须用语言描述，该语言称为规范语言。描述一个复杂问题的输入和输出之间的关系是困难的，目前对规范语言的模式尚无定论。有三种模式：自然语言：不够准确，存在二义性，必须辅以数学语言。一阶谓词：可以精确地描述问题的输入和输出的关系，但是规范文本比较长。如Hoare系统。数学语言：用数学语言可以把输入和输出的映射描述为函数。这些函数的精确的泛函定义就构成了问题的规范。但存在过于规范的问题。2005年3月3日星期四5鲍玉斌东大信息学院计算机软件所程序设计方法学AllRights

4、Reserved3.1程序规范与程序(续)5.一个合适的程序规范语言应满足的基本条件:应当为描述者和使用者所直接理解；应当有严格的数学语义应当与形式方法的构造理论和程序设计语言协调应当有较强的表达能力和通用性2005年3月3日星期四6鲍玉斌东大信息学院计算机软件所程序设计方法学AllRightsReserved3.1程序规范与程序(续)Z语言VDMB方法三者的比较6.形式化程序规范描述语言简介2005年3月3日星期四7鲍玉斌东大信息学院计算机软件所程序设计方法学AllRightsReserved3.1程序规范与程序(续)Z语言是一种基于集合论和一阶谓词逻辑的形式化语言

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

6、息学院计算机软件所程序设计方法学AllRightsReserved3.1程序规范与程序(续)提供了一种称为模式（Schema）的结构，它是Z的基本描述单位，以此来描述一个规范说明的状态空间（静态性质）和操作（动态行为）。Ｚ语言的模式和模式演算：状态模式对目标软件系统的结构特征进行抽象描述；操作模式对目标软件系统的行为特征进行抽象描述；通过模式演算，无论多么大型系统的规格说明都可以通过一个个小的部分来构成；6.形式化程序规范描述语言简介－Z语言简介22005年3月3日星期四9鲍玉斌东大信息学院计算机软件所程序设计方法学AllRightsReserved3.1程序规范与程

7、序(续)Ｚ模式说明可以组合成新的Ｚ模式，新的Ｚ模式继承其成分模式的一切属性和约束。软件系统的Ｚ模式规格说明可以按一定的层次结构给出。Ｚ规格说明由一系列模式组成，每个模式定义一个抽象对象或操作，并用谓词判定描述给出新的对象或操作的语义约束。模式例:6.形式化程序规范描述语言简介－Z语言简介32005年3月3日星期四10鲍玉斌东大信息学院计算机软件所程序设计方法学AllRightsReserved3.1程序规范与程序(续)模式例1:[Student]//引入基本类型studentStudentSys//模式名Enrolled,tested:PStuden