第8章-Z语言

1Chapter8Z语言（一）概述（二）表示抽象（1）集合、关系及函数（2）序列和包（3）自由类型（4）公理描述（5）模式（三）操作抽象（1）模式运算及合成（2）通用式函数（四）Z规格的例（1）图书馆数据库管理（2）自动售货机2（一）概述Z是在JeanRaymondAbrial等的开创性工作下，由英国牛津大学的程序设计研究小组（PGR---ProgrammingResearchGroup），于80年代初所开发的一种形式语言。PRG与IBM的Hursley实验室合作，将Z语言用于IBM的客户信息控制系统CICS（CustomInformationandControlSystem）的开发，使得最终的产品质量得到了全面提高，所检测出的错误数量大大减少，并且整体开发费用降低了9%。在1986年的第一次国际Z用户会议（ZUsersMeeting---ZUM）上，与会人员达成了建立Z标准的共识。1989年建立了Z方法和工作的标准。1992年12月的第七次国际Z用户会议上通过了新的标准。在ISO指导下的国际标准化Z工作已于2002年完成。3（二）表示抽象抽象数据类型是程序设计中十分重要的概念，是封装原理和信息隐蔽原理的集中体现。抽象数据类型将数据及其上的运算视为一个整体，即以数据类型作为基本单位直接描述现实世界中的对象；要求严格区分数据类型的内外性态。外部可见的只是数据类型上的操作及其性态，而数据的内部表示则是隐蔽的，从而达到抽象之目的。高级程序设计语言（如Pascal等）仅提供了一些标准的数据类型(如整型、实型、字符型等)及一些固定的结构类型(如数组型、记录型等)，而对问题领域中出现的其他类型对象，则必须用标准的数据类型和固定的结构类型加以模拟，无法直接定义反映问题性质的新对象。4（二）表示抽象数据抽象和过程抽象是软件规格过程中的两类重要抽象。数据抽象是利用抽象的数据结构进行对象的描述，而不关心这些抽象数据结构在计算机中是如何表示和实现的。过程抽象是指忽略任务具体完成的过程，而只精确描述该任务所要完成的功能，即描述了从输入到输出的映射，该映射的定义域和值域均使用数据抽象来刻画。Z语言基于集合理论和一阶谓词逻辑，支持了这两种类型的抽象，并分别称之为表示抽象和操作抽象。5（二）表示抽象表示抽象将数据从数据结构的表示细节抽象出来，使用了集合、关系、函数、序列、包、模式等抽象数据类型，这些类型构成了Z语言的类型系统；操作抽象描述了在数据抽象中所引入的数据上的抽象算法与操作。表示抽象通过类型定义、全局变（常）量、以及状态空间声明进行表述；操作抽象通过函数和基于一阶谓词逻辑的操作来表述。6（二）表示抽象Z语言表示抽象的要素总体上可分为两类：基于集合理论的集合、关系、函数、序列和包，以及Z独有的模式。这些表示要素构成了Z语言的类型系统。Z中的任何一个变量、常量、以及表达式都必须有一个确定的类型。每一个变量的类型是在对象声明时规定的。变量声明的形式为（其中，T是一个类型）x:T—个z文档的许多地方都会出现变量声明。例如，在如下定义集合Bigcountries时使用a:country声明a为类型country的变量。Bigcountries=={a:country|ahasmorethan40millioninhabitants}例，Evennum=={x:Z|y:Zy0x=2*y}，其中，x:Z、y:Z分别声明x、y为类型Z的变量；符号“”用来分割量词约束和谓词表达式。7（1）集合、关系及函数集合是具有一定属性的元素构成的整体，即一个集合中的元素一般是同一“类”对象。一个集合可以作为一个类型，每一个类型实际上就是一个集合。集合的基本表示方法：一种是将集合的元素按任意顺序枚举出来，称为枚举法；另一种是用规则或公式来说明集合中元素所具有的性质，称为描述法。例如，A=={a,b}，B=={y|y3+y2-y=80}分别定义了两个集合。（注：“==”表示“定义为”）集合是Z语言的基本类型，由用户通过基本类型定义来引入。基本类型定义的格式为：[basictype1,basictype2,…,basictypek]整数类型（Z）是Z中定义的一个重要基本类型，又称为内定义类型，它不需要用户的再次引入或声明。非负整数或自然数集合（N）、正整数集合（N1）也是Z语言的内定义类型。8（1）集合、关系及函数声明加限制的组合方式：声明和限制部分用竖线“|”隔开。例如，{x:Z|-5x5}表示了集合{1,2,3,4,0,-1,-2,-3,-4}。声明加限制的扩展组合方式：用竖线“|”将声明和限制分开、用黑圆点“”将限制和表达式分开。例如，{x:N|x5x2N}表示了小于5的自然数平方的集合，即，表示了集合{02,12,22,32,42}。整数类型Z上定义了+、、*（乘）、div（整除）和mod（模）等算术操作，以及、、和等关系操作。在引入了基本类型后，就可以用这些类型声明变量。但在同一个规格中，同一个元素不能声明为不同的类型。例如，若x已经被声明为Z类型的变量，则不能再将其声明为Student类型的变量。幂集：一个集合A的所有子集为元素所组成的集合称为集合A的幂集，记为PA。通过使用一个基本类型和幂集构造符，就可以产生一个新的类型，称为该基本类型的幂集类型。例如，若集合A=={a,b}，则PA=={,{a},{b},{a,b}}。幂集构造符可应用于任何集合构成另外一个集合，从而由一个类型产生另一个新的类型。例如，若S是一个集合，则PS、PPS都是合法的Z语言类型。(PPA=={,{},{{a}},{{b}},{{a,b}},{,{a}},{,{b}},{,{a,b}},{{a},{b}},{{a},{a,b}},{{b},{a,b}},{,{a},{b}},{,{a},{a,b}},{,{b},{a,b}},{{a},{b},{a,b}},{,{a},{b},{a,b}})10当某个元素属于多个集合时，它只能属于一个类型。例如，整数3是{3}、{1,3,5}、N（自然数集合）、Z、以及其他很多集合中的一个元素，但只能以它们中的某一个作为类型，这里应该是类型Z。类型就是一种特定的类的集合，它被看成是一个“最大集合”，即，一个类型代表了一个元素可以属于的最大可能的集合。如，考虑集合signal=={3}，smallodd=={1,3,5}，则可以说signal和smallodd的类型都为PZ。一个集合A的所有有限子集为元素所组成的集合，记为FA。一个集合A的所有非空有限子集为元素所组成的集合，记为F1A。Z语言的基本类型是集合，所以集合的所有操作都适合于基本类型，包括：（属于）、（不属于）、（并）、（交）、\（差）、#（基数）、（包含）、（真包含）、＝（相等）元组：对于自然数n，n个对象a1,a2,…,an按一定次序排列成的一个序列，称为n元组，记为（a1,a2,…,an）。二元组又称为序偶。二元组（x,y）经常被写为：xy。笛卡尔积：设A、B是任意两个集合，若序偶的第一元素是A的一个元素，第二元素是B的一个元素，则所有这样的序偶的集合称为集合A、B的笛卡尔积，记为：AB，即AB=={(x,y)|xAyB}。同理可得任意n个集合A1,A2,…,An的笛卡尔积：A1A2…An。给定若干个集合的笛卡儿积是一个新的类型：笛卡儿积类型，如：ZZ。再如，定义图书类型：TitleAuthorCallNumberYear，其中Title、Author、CallNumber、Year为基本类型。如：book：TitleAuthorCallNumberYear声明了变量book是一个四元组（t,a,c,y），分别表示一本书的标题、作者、编号、和出版年份。如果t1,a1,c1,y1的变量类型分别为：Title、Author、CallNumber、Year，那么就可能有：book=（t1,a1,c1,y1）。若给定了一个元组，则只要检查一下它的每个元素的类型，就可以确定该元组的笛卡尔积类型。如，如果知道t1Title、a1Author、c1CallNumber、y1Year，则可知（t1,a1,c1,y1）TitleAuthorCallNumberYear。笛卡儿积可以和幂集类型构造符一起使用，从而构造出新的类型。例如，若cities和color是已经引入的基本类型，则可构造出（Pcities）（Pcolor）和P（citiescolor）等类型。元组可以通过声明加限制的组合方式或声明加限制的扩展组合方式来表示。例如，{x:N；S:PN|S={x+1}x5}则表示了满足谓词的元组，元组的顺序由声明确定，该表示所对应的元组为{(0,{1}),(1,{2}),(2,{3}),(3,{4}),(4,{5})}；{x:Z|1x5(x,x)ZZ}表示元组{(2,2),(3,3),(4,4)}。元组是一类特殊的集合，所有基本类型的操作对于元组都适用。但是，元组的相等不仅要求其中的元素相同，而且各元素出现次序也必须相同。关系：序偶的集合称为二元关系，简称为关系。对于集合X和Y，用XY表示从X到Y的所有关系的集合，即：XY==P(XY)。从X到Y的一个关系R可以用R:XY来声明，该关系的类型为XY，并称X为关系R的源集合、Y为关系R的目标集合。例如，对于X=={a,b}，Y=={1,2}，XY=={{a1,a2,b1,b2}，{a2,b1,b2}，{a1,b1,b2}，{a1,a2,b2}，{a1,a2,b1}，{(b1,b2)，{a2,b2}，{a2,b1},{a1,b2}，{a1,b1}，{a1,a2}，{a1}，{a2}，{b1}，{b2}，}。单位关系是一种特殊的关系，任意集合X上的单位关系定义为：idX=={x:X|xXxx}。例如，对于X=={a,b,c}，那么idX=={aa,bb,cc}。关系可看作一类特殊的集合，所有集合的操作都可应用于关系。除此之外，关系还具有了更加丰富的操作。14（1）集合、关系及函数定义域和值域：关系的定义域或前域是关系源集合的一个子集；关系的值域或后域是关系目标集合的一个子集。对于关系R:XY，用domR表示R的定义域、ranR表示R的值域。domR和ranR用集合形式表示为：domR=={x:X|y:YxyR}；ranR=={y:Y|x:XxyR}.例如，对于X=={a,b}到Y=={1,2}的类型XY的关系R=={a2,b1,b2}，那么domR=={a,b}，ranR=={1,2}。关系复合：对于关系R:XY和S:YW，它们的复合关系R;S为满足下述条件的关系XW：{x:X;w:W|(y:Y(xyRywS))xw}。这种复合关系也称为右复合关系。相应地，可以定义左复合关系或者反向复合关系如下：R○S==S;R.关系R:XY自身复合R;R可简记为R2。对于任一正整数n，Rn==Rn-1;R，并称为关系R的n次迭代。一般地，R0==idX。15（1）集合、关系及函数关系的闭包：关系R的传递闭包R+、自反传递闭包R*定义为：R+==R1R2R3…R*==R0R1R2…关系的逆：对于类型XY的关系R，它的逆关系定义为：R-1=={x:X;y:Y|xyRyx}定义域限制与值域限制：对于类型XY的关系R，设S（T）是定义域（值域）类型X（Y）的一个集合，则关系R的定义域S限制定义为：SR=={x:X;y:Y|xSxyRxy}关系R的值域T限制定义为：RT=={x:X;y:Y|yTxyRxy}.例如，对于关系R=={a2,b