补充资料：Z语言

Z语言
Z language

　　2 yuyanz语言(2 language)一种以状态机为模型的形式规约语言。最早由法国人J.R.Abrial提出，由C.A.R.Hmre(英国牛津大学)领导的程序设计研究小组发展而成。 Z的基本单位是模式。一个模式用一右边开口的矩形框起，中间一道横线将它分成说明部分和谓词部分。说明部分定义一些状态或模式变量;谓词部分是一般的谓词公式，它给出了变量间的限定关系。模式可定义系统的状态空间，初始状态和状态变换。如下面的模式定义了公寓出租系统的状态空间: RentAI〕artaPartnlents:P APAR飞，M五NTcustonlers:P PERSDNbx永司;APAR’1、州[E NT~Tly[E~PERSON donlh刀ked二aPartments V(ap:ApARI，M王NT}即任司〕artments. ranl功k司ap二custom二)其中Re ntA户汀1是模式名。apartments是一个公司所有的公寓;custC‘ners是该公司的客户集。h刀k司是一个部分函数，它指明某一公寓在特定时间里租给了某个客户。谓词部分指出，h刀k己的定义域(公寓)必须是该公司的财产，而租用人(饭刀k曰的值域)必须是该公司的客户。说明和谓词部分都可以有多行，行与行之间分别是“拼接(;)”关系和“与(八)”关系。模式也可以线性地表示，如上面的模式可表示为: Ren廿匆〕art三【apartnlellts:P ApARI，MENT; custonlers:P PER以〕N; 加汰司:A尸ARI，M[E NT~TIME ~PERSON {(donlh刀ked互apartments)八 V(叩eAPARI，M[E NT}aP任 aPartnlents八ran恢刀kedap 里custonl眺) ]由此可见，一个模式定义了一个(子)集合。作为集合，模式可以进行诸如并(V)，交(八)，蕴含(卫)，幂集(P)，大小(#)等集合运算，也可以移人已定义的模式。 模式既可以表示数据状态，也可以表示运算。运算通过状态变化来表示。当用来表示运算时，用酷表示模式S的状态改变，用a’表示变量a改变后的状态值。如: 1玉叉)king 山又entAPart a?: APARTMEN」， t?:TIME p?: PER又)N a?〔alxlrtrllents p?任custonlers t?氏dornl叉叉〕k己a? l刀〕ked’=lx幻k己U la?~t?~p?} apartmellts=al〕artlllellts CUStolllers=CI】St()1llerS表示，当一间公寓(a?)某个时间(t?)未租出，则将它租给客户(p?)。这里，变量后面的“?”表示该变量是输人变量;若要表示输出，则在变量后面加“!”。 一个Z规约就是一组模式和用自然语言书写的对各模式的注释。模式之间通过模式运算和移人相关联。 Z以其直观、简洁、接近功能分解模型吸引了众多的用户。利用谓词演算和模式演算的数学性质，可对Z规约进行形式分析。现已有各种Z规约辅助开发工具。针对面向对象的软件风范，Z又有了ObjectZ和Z++等扩充。
　　

说明：补充资料仅用于学习参考，请勿用于其它任何用途。