第8章Z语言剖析.pptVIP

Chapter 8 Z语言 （一） 概述 （二） 表示抽象 （1） 集合、关系及函数 （2） 序列和包 （3） 自由类型 （4） 公理描述 （5） 模式 （三） 操作抽象 （1）模式运算及合成 （2）通用式函数 （四） Z规格的例 （1）图书馆数据库管理 （2）自动售货机 （一） 概述 Z是在Jean Raymond Abrial等的开创性工作下，由英国牛津大学的程序设计研究小组（PGR --- Programming Research Group），于80年代初所开发的一种形式语言。 PRG与IBM的Hursley实验室合作，将Z语言用于IBM的客户信息控制系统CICS（Custom Information and Control System）的开发，使得最终的产品质量得到了全面提高，所检测出的错误数量大大减少，并且整体开发费用降低了9%。 在1986年的第一次国际Z用户会议（Z Users Meeting---ZUM）上，与会人员达成了建立Z标准的共识。1989年建立了Z方法和工作的标准。1992年12月的第七次国际Z用户会议上通过了新的标准。在ISO指导下的国际标准化Z工作已于2002年完成。 （二） 表示抽象 抽象数据类型是程序设计中十分重要的概念，是封装原理和信息隐蔽原理的集中体现。 抽象数据类型将数据及其上的运算视为一个整体，即以数据类型作为基本单位直接描述现实世界中的对象； 要求严格区分数据类型的内外性态。外部可见的只是数据类型上的操作及其性态，而数据的内部表示则是隐蔽的，从而达到抽象之目的。 高级程序设计语言（如Pascal等）仅提供了一些标准的数据类型(如整型、实型、字符型等)及一些固定的结构类型(如数组型、记录型等)，而对问题领域中出现的其他类型对象，则必须用标准的数据类型和固定的结构类型加以模拟，无法直接定义反映问题性质的新对象。 （二） 表示抽象 数据抽象和过程抽象是软件规格过程中的两类重要抽象。 数据抽象是利用抽象的数据结构进行对象的描述，而不关心这些抽象数据结构在计算机中是如何表示和实现的。 过程抽象是指忽略任务具体完成的过程，而只精确描述该任务所要完成的功能，即描述了从输入到输出的映射，该映射的定义域和值域均使用数据抽象来刻画。 Z语言基于集合理论和一阶谓词逻辑，支持了这两种类型的抽象，并分别称之为表示抽象和操作抽象。 （二） 表示抽象 表示抽象将数据从数据结构的表示细节抽象出来，使用了集合、关系、函数、序列、包、模式等抽象数据类型，这些类型构成了Z语言的类型系统； 操作抽象描述了在数据抽象中所引入的数据上的抽象算法与操作。 表示抽象通过类型定义、全局变（常）量、以及状态空间声明进行表述； 操作抽象通过函数和基于一阶谓词逻辑的操作来表述。 （二） 表示抽象 Z语言表示抽象的要素总体上可分为两类：基于集合理论的集合、关系、函数、序列和包，以及Z独有的模式。这些表示要素构成了Z语言的类型系统。 Z中的任何一个变量、常量、以及表达式都必须有一个确定的类型。每一个变量的类型是在对象声明时规定的。 变量声明的形式为（其中，T是一个类型） x: T —个z文档的许多地方都会出现变量声明。例如，在如下定义集合Bigcountries时使用a: country声明a为类型country的变量。 Bigcountries = = {a: country | a has more than 40 million inhabitants} 例，Evennum = = {x: Z | ?y: Z ?y0?x=2*y}，其中，x: Z、y: Z分别声明x 、y为类型Z的变量；符号“?”用来分割量词约束和谓词表达式。 （1） 集合、关系及函数 集合是具有一定属性的元素构成的整体，即一个集合中的元素一般是同一“类”对象。 一个集合可以作为一个类型，每一个类型实际上就是一个集合。 集合的基本表示方法：一种是将集合的元素按任意顺序枚举出来，称为枚举法；另一种是用规则或公式来说明集合中元素所具有的性质，称为描述法。例如，A= ={a,b}，B= ={y|y3+y2-y = 80}分别定义了两个集合。（注：“= =”表示“定义为”） 集合是Z语言的基本类型，由用户通过基本类型定义来引入。基本类型定义的格式为： [basictype1, basictype2, …, basictypek] 整数类型（Z）是Z中定义的一个重要基本类型，又称为内定义类型，它不需要用户的再次引入或声明。非负整数或自然数集合（N）、正整数集合（N1）也是Z语言的内定义类型。 （1） 集合、关系及函数 声明加