（计算机软件与理论专业论文）z规格说明中一阶逻辑算子自动求精的研究与实现.pdf

沈阳工业大学硕l 学位论文 摘要 随着计算机产业的快速发展，软件的开发规模不断扩大，对软件开发效率和安全性 的要求也越来越高，各种开发方法应运而生。z 语言作为一种软件工程语言和形式化方 法在软件文档规范化的应用中成效显著。近年来，国内外对z 语言的研究也逐渐增 多。z 语言与其它符号系统相比，一个显著特点是它的规格说明可以用于推理和求精。 以往的这种求精过程都由人工完成的，它自动求精实现却进展缓慢。本文以z 规格说明 的自动求精为目的，通过约束z 语言中计算机不能实现或不易实现部分，设计出z 语 言的一个子集s m a r tz ，并以标准c + + 和s t l 为工具，运用编译技术实现了s m a r tz 规 格说明中一阶逻辑算子自动求精。 判断计算机是否可以完成自动求精，关键取决于能否找到实现规格说明的语法、语 义的算法。本文将语法、语义的实现问题归约到某一个可解问题，并通过在“通用计算 机模型”图灵机上运行这个可解问题的算法，来证明规格说明求精可判定性。 s m a r tz 继承了z 语言的整型、集合和谓词等，同时保证了其规格说明可求精眭，并以 一套形式化的方法一正则表达式和e b n f 范式描述了它的语言体系。本文使用编译技 术实现s m a r tz 的语法分析、语义分析及向目标代码的转换，本文又针对规格说明的自 身特点，对相关算法加以改进，为一阶逻辑算子自动求精的实现创造条件。s m a r tz 的 一阶逻辑算子包括量词和连接词等，本文给出它们的求精算法，并以一个实例演示了规 格说明和逻辑算子的自动求精过程。 本文最后的结论是“z 语言经过适当的约束后，一阶逻辑算子的自动求精是可以实 现的”，这是z 规格说明自动求精目标实现的一个重要前提，也是为实现自动化程序设 计做出的一次有意义的尝试。 关键词：z 语言，规格说明，精化，自动机，谓词逻辑 沈阳工业大学硕j 一学位论文 r e s e a r c ha n d i m p l e m e n t a t i o n o ft h ef i r s to r d e rp r e d i c a t e l o g i c o p e r a t o r a u t o m a t i cr e f i n e m e n ti nz s p e c i f i c a t i o n a b s t r a c t t h ef o r m a ls p e c i f i c a t i o nn o t a t i o nzb a s e do i ls e t - t h e o r ya n df i r s to r d e rp r e d i c a t el o g i ci s u s e f u lf o rp r e s e m i n gc o m p u t e r - b a s e d s y s t e m w i t h o u t u n d u l ye x p r e s s i n gt h ew a y i nw h i c ht h e s e p r o p e r t i e sa l e a c h i e v e d zi sn o ta ne x e c u t a b l e l a n g u a g eg e n e r a l l y ，s ot h e r ei sn os u c h 吐l i n ga sa zc o m p i l e r l i n k e t c t h em o d e l sd e s c r i b i n gs o m ei n f o r a l a t i o ns y s t e mi nzl a n g u a g ec a nb e r e a s o n e da n dr e f i n e dm a n u a l l ya si td o e si nat r a d i t i o n a lw a y s o m e p e o p l em a k eg r e a te f f o r t s t o w a r d sa n i m a t i n gs u b s e to fzw h i l et h ew o r ki sp r e l i m i n a r y w ea t t e m p tt oi m p o s er e q u i s i t e c o n s t r a i n so nz s p e c i f i c a t i o na i m e d a tr a p i d l y p r o d u c i n g t h ep r o t o t y p ei ns p e c i f i cp r o g r a m m i n g l a n g u a g e t h ea u t o m a t i cr e f i n e m e n to f f i r s to r d e r p r e d i c a t el o g i co p e r a t o r si nzl a n g u a g ei st h em a j o r p o i n tt h a tt h i s t h e s i sf o c u s e so n f i r s t l y , t h et h e o r e t i c a l p o s s i b i l i t i e so fd a t as t r u c t u r e sa n d c a l c u l u s p r o c e e d i n ga u t o m a t i c a l l ym u s tb ep r o v e dw h e r et h eg e n e r i cc o m p u t e rm o d e lo f t u r n i n g m a c h i n ei su s e da n dt h ea u t h o r sv i e wi sp o i n t e do u tt h a ta c o m p u t e r c a ni m p l e m e n t t h ea l g o r i t h mo ns o m el e v e lw i t h o u to u t s i d e si n t e r f e r e n c e s e c o n d l y s m a r tzt h es u b s e to fz l a n g u a g ec o m e s i n t ob e i n g n a t u r a l l ya n d t h ed e s i g nd e t a i l sa n dr u l e sa r ei n t r o d u c e dt oi m p r o v e t h ea w a r e n e s so ft h en o t a t i o n ss y n t a x ，g r a m m a ra n ds e m a n t i c s f i n a l l y ，w ee m p l o yc o m p i l e r c o n s t r u c t i o na n ds t lu t i l i t i e su p o na u t o m a t i cr e f i n e m e n to ft h ef i r s to r d e rp r e d i c a t e l o g i c o p e r a t o r si nzs p e c i f i c a t i o na n d t h es t a n d a r dc + + s e r v e sa st r a n s i e n tl a n g u a g ei l l u s t r a t i n gh o w t h et r a n s f o r m e rw o r k s t h ec o n c l u s i o no ft h ea u t o m a t i cr e f i n e m e n to fs m a r tzs p e c i f i c a t i o nc o n t r i b u t e st ot h e s i g n i f i c a n tp r o j e c to f a u t o m a t i cp r o g r a m m i n g k e y w o r d s ：z n o t a t i o n ，s p e c i f i c a t i o n ，r e f i n e m e n t , a u t o m a t a , p r e d i c a t el o g i c 一2 一 独创性说明 本人郑重声明：所呈交的论文是我个人在导师指导下进行的研究工 作及取得的研究成果。尽我所知，除了文中特别加以标注和致谢的地方 外，论文中不包含其他人已经发表或撰写的研究成果，也不包含为获得 沈阳工业大学或其他教育机构的学位或证书所使用过的材料。与我一同 工作的同志对本研究所做的任何贡献均己在论文中做了明确的说明并表 示了谢意。 签名： 日期：2 1 堕：主：圭一 关于论文使用授权的说明 本人完全了解沈阳工业大学有关保留、使用学位论文的规定，即： 学校有权保留送交论文的复印件，允许论文被查阅和借阅；学校可以公 布论文的全部或部分内容，可以采用影印、缩印或其他复制手段保存论 文。 ( 保密的论文在解密后应遵循此规定) 签名： 匆略昏 导师签名：夏废气日期：加j 3 掣 沈阳t 业大学顿：l 学位论文 1 绪论 1 1 课题背景 z 语言的全称为“形式化规格说明符号系统z ”，它是一套用于描述计算机软硬 件系统的记号和规范集，其理论基础是集合论和谓词阶逻辑理论。2 0 世纪7 0 年代 未，z 浯言处于初创阶段，j e a n r a y m o n da b r i a 在这一阶段做了大量的工作。其后的若 干年旱，得益于j e a n r a y m o n da b r i a 思想的启发，牛津大学计算实验室( o u c l ) 的编 程研究组( p r g ) 和他的工业伙伴，其中包括i b m 和i n l n o s ( 半导体制造商) ，逐步发 展和完善了这了套符号系统。1 9 8 9 年，在经过了多年的研究和实践后，第一本z 符号 系统参考手册问世，它一出版就得到同行们的广泛认可。2 0 0 2 年，z 语言完成了国际 标准化“1 过程，并作为基础符号系统，应用于描述其它符号系统，如面向对象编程等。 迄今为止，z 语言已经发展成为一套比较成熟的符号体系。 用z 语言书写的形式化的文档叫做“规格说明”，它是用抽象的数学方法和符号系 统确切地描述客体必备属性，消除由于不规范的说明方法引起的对客体屙| 生的描述或理 解上的二义性。它是一种形式化方法。规格说明是描述“做什么”的，它不回答“怎么 做”的问题。规格说明的这种抽象方法对软件工程来说十分有用，它使得软件开发的目 标非常明确，而不必纠缠于代码的细节和反复强调用户说明的含义。 规格说明的使用可以贯穿软件开发的始终，例如，通过它可以了解用户需求，开发 者可用它编写实现的代码，测试人员可以用它来测试结果，文档人员可以用它编写用户 手册。规格说明不依赖于任何的编程语言或工具，所以它可以先于代码开发之前编写完 成。虽然随着需求的变化和开发人员工作的深入，规格说明会做相应的修改，作为一种 软件开发小组的交流文档，它不失为一种统一认识和明确目标的优秀工具。 可见，规格说明作为需求文档的优点有二：无二义性和代码无关性。这是因为它使 用了数学中一些数据类型。虽然数学中的数据类型不是为计算机编码而设计的，但是， 数学中的丰富的聚集类型( 如集合) 能有效的表达计算机系统的行为。计算机的这些行 为在规格说明中一般是用“谓词”来抽象地描述的，同样，“谓词”也可用来推演系统 沈阳工业人学硕士学位论文 行为，这就是z 规格说明的推理和可验证性“。 在国外，z 语言的研究已深入开展了许多年，它的研究队伍也不断地扩大，如欧 美f 1 本等国都有专门的相关研究人员，而且己形成“产、学、研”一体的良性循环 链。在欧洲，有一些形式语言的科研团体，他们的研究对象包括v d m “1 、z 语言、b 方 法等。这些研究究团体之间相互交流也比较多，比较有代表性的是z u g ，即“z 语言用 户协会”。1 ，它们每隔一两年召开一次国际性的科研交流会，每一届会议都会带来最新 的研究成果。2 0 0 3 年7 月，“z 用户研究协会”召开了第1 5 次国际年会，暨“z 规格 说明和b 方法的第三届国研讨会”( 注：b 方法是与z 规格说明类似的形式化方法) 。 来自世界各地的学者来到芬兰的旧都土尔库，在那里进行学术交流和研讨。与会的科研 院所有英国的剑桥大学和牛津大学，芬兰的a b oa k a d e m i 大学法国的g r e n o b l e 大学， 美国的华盛顿大学，美国俄勒冈微软研究所等。这次年会带来了z 规格说明的最新研究 成果和其相关的产品，下面是这次年会的议题： ( 1 ) z 规格说明和b 方法的工业应用和案例研究； ( 2 ) 在软件开发的整个周期中综合应用基于模式的说明方法； ( 3 ) 运用基于模式的说明方法构建软件或硬件的系统结构； ( 4 ) 运用形式化方法描述需求和验证需求的有效性： ( 5 ) 关于形式化方法的一些理论问题( 例如：求精问题，定理证明过程，定理的f 确性验证等) ； ( 6 ) 软件的测试和面向定理的开发方法； ( 7 ) z 规格说明和b 方法的支撑工具； ( 8 ) 运用基于模式的说明方法验证c o t s ： ( 9 ) z 和b 的扩展和标准化； 从这次会议的议题上，我们可以了解到z 规格说明的研究较多的集中在它的系统描 述功能和有效性验证上，而z 规格说明向可执行代码的自动转换问题关注较少。规格说 明向执行代码的自动转换涉及到的求精策略和智能选择问题是十分灵活的，而且要考虑 的情况比较复杂。以往的求精过程要由人来干预，自动化程度不高。因此，提高求精的 沈阳工业大学硕士学位论文 自动程度是这个课题的研究重点。由于一阶逻辑的理论已比较成熟，而且国内外关于这 方面的论述也较多，这为研究一阶逻辑算子提供了很好的基础。 近年来，z 语言的研究与工业应用相结合，扩展了z 语言的功能，如c o o z 6 1 、 z + + 等，其应用涉及网络服务、u n i x 软件开发、符号系统设计和图形界面系统的规划 等领域，尤其是对可靠性”“q 要求较高的行业，如国防安全、航天、医疗等领域。通常 来说z 是一种不可执行的语言，它只用作文档的规范化和推理验证等，但并不是说它没 有可执行化的可能。在9 0 年代初，曾有过z 语言的可执行化意义的讨论，一些学者也 发表过一些观点，但至今没有有效的办法实现可执行化“、”1 。国内对于z 规格说明 的研究是起步较晚的。国内研究z 规格说明较早的是上海大学的缪淮扣教授，那时他只 是用它作为定理证明的形式化方法。适逢中国软件产业刚刚起步，软件工程的实践尚未 成熟，z 语占并未引起业界足够的重视。随着软件业的发展和软件工程技术研究的深 入，国内对形式化方法的研究也逐渐升温。1 9 9 9 年缪淮扣教授和他的助手出版了一本 介绍z 规格说明的教材软件工程语言z ，使得国内许多高校的学生有机会 接触z 。这几年，国内的其它一些学者对z 规格说明的研究院有了进一步的深入，如： z 规格说明构造方法和从测试规格说明到测试用例的自动生成方法等。但是， z 规格说明对国内软件业影响不大，也没有用它去指导软件开发。 摒弃传统观点中“程序是计算机直接可执行的”的观点，那么规格说明和程序代码 差别就可以淡化。这样，程序可以分为若干层次：最高层是不能直接执行的程序，即规 格说明，它由抽象的描述语句构成；最低层是可以直接执行的程序，称之为程序代码 它由可执行的命令语句构成，如赋值语句、选择择语句、循环语句等：最高层和最低层 之间的系列程序称之为混合程序，既含有抽象的描述语句，又含有可执行的命令语句。 如图11 。 沈阳t 业大学硕士学位论文 易理解性增强 可执行性增强 图1 1 程序在求精过程中的状态 规格说明向程序代码的转化是一个程序的可执行性逐步增强的过程，也就是所谓的 求精”( r e f i n e m e n t ) 的过程。 自动程序设计“5 “、”1 是人工智能“”领域一项重要的研究内容。现有研究成果中，有 一些能够实现以各种不同的目的描述( 例如输入输出对，高级语言编程，甚至英语语法 描述算法) 来编写计算机程序。这方面的进展只限于少数几个完全现成的例子，例如， 将u m l “2 ”用例转化为代码框架。编写一段计算机机程序的任务既与定理证明有 关，又与机器人学习有关。自动程序设计、定理证明和机器人问题求解中大多数基础研 究是相互重叠的。从某种意义上讲编译程序已经在做着“自动程序设计”的工作。这旱 所指的自动程序设计是指某种“超级编译器”，或者是某种能够对程序要实现什么目标 进行非常高级描述的程序，并能够由这个程序生成所需的新程序。这种高级描述可能是 形式语言的一条精辟语句( 如谓词演算) ，也可能是一条松散的描述( 如用自然语 言) ，比如说，z 语言的的规格说明就是这样一种描述。z 语言的规格说明可以用传统 的词法分析，语法分析，语法制导的的语义分析，逐步的明确程序设计的目标框架，也 可以使用更为高级的语义制导。2 3 及p e t r i 网1 等技术设计出更“合格的程序”。这就要 求在系统与用户之间进一步对话以澄清模糊。 “z 规格说明中一阶逻辑算子的自动求精”并不是要把z 的规格说明转化成可执 行的代码。前面提到过，z 不是- f 更高级的编程语言，它为人而设计的，而不是为机 器设计的，这使得它向可执行代码的自动转换的实现有相当的难度。但是，从另一方面 沈阳工业大学钡十学位论文 来看，z 规格说明与计算机的软硬件模型有相当好的匹配性和描述性，使它逐步求精成 为可能。因此，在z 规格说明向可执行代码的自动转换过程中不必一步到位，通过求精 尽量的增加它的可执行性，例如，将z 规格说明转化成为某种高级语言的源程序，这样 就可以间接地将规格说明转化为可执行代码。从这个角度来看，z 规格说明的求精有些 像编译软件的前端功能，但二者之间仍有区别。一般的编译软件的端所输出的中间语言 已经与机器语言十分接近，只是逻辑层次更高一些。本课题中研究的z 规格说明的自动 求精的目标是c + + 汹1 源程序，c + + 源程序的逻辑层次要比编译程序中的中间语占还要高 很多。说到这里，z 规格说明的自动求精有些自动化程序设计的味道。但是它又不像自 动化程序设计那样对生成的程序代码的要求很高，只在底层次上验证用计算机自动求精 的可实现性。 1 2 课题研究的主要内容 “z 规格说明中一阶逻辑算子的研究与实现”是“z 规格说明向高级语言程序转 化”大课题下的子课题。由于z 是一个非常庞大的语言体系，一方面将大课题划分为小 的子课题，然后分期分批的各个击破：另一方面，以点带面，采取从局部到整体、从简 单到复杂的策略，先在大的课题中选取一块小的范围作为研究的对象，总结出研究的规 律，然后逐步的扩大范围，直至覆盖整个课题。因此，对于一个复杂的对象体系，选择 一个适当的突破口来开展对于它的研究，就显得尤为重要。于是，兼顾一阶逻辑算子的 实现，在z 语言原有语法、语义的基础上，设计一个z 语言的子集s m a r tz ，作为研究 对象，讨论并证明它的可实现性，为将来的工作打下理论基础，是本课题需要完成的一 项非常重要的工作。 z 语言是一种形式化的规格说明语言，它是用来书写规格说明的，是一种可用于精 化和推理的形式语言。本课题的研究内容就是用形式化的方法研究z 语言及其一阶逻辑 算子的求精实现。具体来说，它分以下几个内容： ( 1 ) 设计z 语言的子集s m a r t z ： ( 2 ) s m a r tz 的可求精性证明： ( 3 ) 用形式化的方法分析s m a r tz 的语法和语义； ( 4 ) 讨论s m a r tz 中一阶逻辑算子求精的具体算法与实现过程； 沈阳 = 业大学颂十学位论文 f 5 1 讨论生成程序的结构样式。 本文难点是z 语言的可行性证明，根据语义信息编出相应的正确的程序也是本课题 研究的难点。 本文涉及的知识包括：编译原理1 、可计算性与计算复杂性、集合论、一阶逻辑、 机器翻译、自动程序设计等。 1 3 课题研究方法和步骤 规格说明它有两方面的特征：一方面，它具有自然语言的通用性( 可描述的对象十 分的广泛) 、灵活性( 使用方式多种多样) 和松散性( 格式与排版可能是松散的) ；另 一方面，它又具有形式语言的形式化、准确性和逻辑性强的特点。因此，对规格说明的 自动求精研究一般包括以下几个过程： ( 1 ) 从语言学的角度提出规格说明处理的问题和理论； ( 2 ) 把需要研究的问题在语言学”1 上加以形式化，使之能以一定的数学形式，严密 而规整的表示出来： ( 3 ) 将这种数形式表示为算法，使之能在计算机上表示和实现。 由此可见，本课题涉及语言学、理学和工学三个领域的研究。因此，本课题应用的 主要技术和理论有： ( 1 ) 使用语言学的理论对规格说明自动求精问题加以形式化； ( 2 ) 使用产生式系统来定义和设计s m a r tz 的文法； ( 3 ) 使用自动机理论”3 来证明语言的可判定性； ( 4 ) 使用编译技术油1 来实现s m a r tz 中一阶逻辑算子的自动求精； ( 5 ) 使用泛型技术、s t l 的容器和算法实现对zm a t h e m a t i ct o o lk i t 的表示与实 现。 综上所述本课题的研究对象是z 语言系统及其一阶逻辑算予的求精算法，研究范 围是s m a r tz ，研究方法是“理论论证+ 系统设计+ 实验验证”，实验工具是标准c + + 和 s t l ，研究过程遵循的是从简单到复杂，从特殊到一般，以点带面直到覆盖整体的步骤 和策略。 沈阳工业大学硕：学位论文 2 z 语言约束和s m a r t z 的可判定性 本章主要从理论角度讨论z 语言是否可在计算机上实现的问题。讨论问题的主要思 路是： ( 1 ) 分析z 语言的特点，找到需要解决的问题： ( 2 ) 将问题归约到某个可解决的问题； f 3 ) 将问题的求解算法描述为某种语言； ( 4 ) 设计能够识别这种语言的图灵机，再证明语言的可判定性。 所谓的可判定性是指，如果某语言( 或算法) 是图灵可判定的，那就说这种语言 ( 或算法) 是可判定的，或者说具有可判定性。图灵机是通用计算机模型，如果一个算 法是可判定的，这意谓着这个算法可由计算机实现。 2 1z 语言的功能分析 z 语言功能强大，体系复杂，若想实现它的自动求精，必须先弄清它的功能和特 点。本文把z 语占的特点“与求精之间的关系总结为以下两条。 第一，z 语言的书写规范符合人的习惯的同时，增加了分析规格说明的难度。 z 语言是为人设计的，而不是机器。因为在很长一段时间内，z 的文档都用纸和笔 书写的。人们习惯于用z 在公式的旁边附一些版式松散的注释，所以，有时候z 的文 档显得不是那么规整。虽然初学者容易因z 的众多的方框、陌生符号和希腊字母而心生 难意，但是它很易学，而且一经掌握，这些方框和符号的优势和好处就会显现出来 在阅读z 文档之前，它的结构就已一目了然了。 然而，z 语言中众多的字母和符号为电脑录入的实现带来很多的不便。对于机算 机，最容易处理的输入便是键盘字符表，这个字符表远远不能满足z 语言符号表的要 求，例如：z 语言中大量的希腊字母、数学符号、箭头、线条、方框、特殊符号等，它 们的录入处理都很麻烦。解决办法之一就是建立z 符号与a s c i i 字串的映射，让特定 的a s c i i 字串代表z 语言中的某个符号。其缺点是会造成一些常用的字串因为被指定 为关键字而无法使用。 z 的规格说明是不可执行的。也就是说，一殷清况下，它不能够通过编译转换为可 沈阳工业大学顺一1 j 学位论文 执行的程序，它不是一门计算机编程语言，更不是一门“非常高级”的编程语言。z 语 言松散的版式为z 规格说明自动求精设置了障碍。因为每一个可执行的程序都有一个明 确的执行入口点，而规格说明内部语义关系可能是错综复杂的，在千头万绪线索中找到 一个执行的触发点也绝非易事。因此，可以考虑让z 规格说明编制的条理清楚一些，以 使自动求精的实现更容易，例如，让规格说明的书写者指定目标程序的执行入口。 第二，“数学工具箱”使z 语言更为强大，同时要求自动求精的目标语言提供有效 的功能支持。 z 语言的数学符号库比较小，为此它配备有一套较大的类型和操作符库z 的数 学工具箱( zm a t h e m a t i ct o o lk i t ) 。它不是一套软件，而是一套数学理论，其中包括对集 合、元组、关系、函数、序列和它们操作的定义及运算规则。工具箱对于z 就好像标准 库与编程语言的关系一样一工具箱虽然是一种补充，但它使得z 变得更强大，且它的 地位与z 自身的类型和符号无异，一样用于描述计算机的各种软硬件系统及组件。z 语 言的数学工具箱为z 规格说明的求精提出了挑战，因为，即使是由人手工编程实现数学 工具箱的功能，也不是一件轻松的事，更别说让计算机去实现了。值得关注得，是由 c + 十泛型技术支持的标准模板库( s t l ) 为z 的数学工具箱的实现提供了良好的支持。 如：s t l 中的容器可用来实现z 数学工具箱中的聚集类型，s t l 的通用算法可用来实现 聚集类型的运算和操作。 2 2 约束问题的提出 在绪论中我们已经知道，缩小研究范围，选取z 的子集来开展研究是由科学研究的 方法论所决定的。从另一角度来看，z 语言中的确存在着计算机无法实现的东西，因 此，为了实现规格说明的自动求精，就不得不对z 语言进行约束。在后面的小节旱，将 会讨论计算机的这个局限。 本文所谓对z 语言的约束是指从z 语言的三个层次，即词法、语法、语义进行约 束。约束结果有二，一是去掉了z 语言中对于计算机来说无法实现的和难于实现的语法 单位和语义内容：二是，约束后的z 语言，经过形式化的描述后，成为一个新的语言 s m a r t z 。 对z 的约束的应遵守以下几个原则： 沈阳工业大学顾十学位论文 ( 1 ) 保证语占的正确性； ( 2 ) 保证语占的完整性； ( 3 ) 保持s m a r t z 与z 之间的延续性； ( 4 ) 为s m a r tz 将来的扩展留有余地； 除了对z 语言的约束工作外，还有对s m a r tz 的语法、语义扩充。这种工作是必要 的，约束的的s m a r tz 不能保证它能够为自动求精提供够的信息量，因此要为s m a r tz 做必要的约定，以使用户知道如何正确的书写一份有足够信息量的规格说明。 在下面的小节中，我们将使用通用计算机模型图灵机”来考查z 语言的数据结 构和算法的可行性，并对计算机不可实现或验证以实现的部分作为约束，最后形成一个 计算机可以实现的语言模型s m a r tz 。 2 3z 语言的类型约束 2 3 1 原子类型约束 z 语言的数据类型汹1 可分为3 种：原子类型、聚集类型和基本类型。这3 种数据类 型用途异，又相互联系。聚集类型的内部由若干层次的原子类型或基本类型组成，原子 类型和基本类型是其它类型的基础。 z 语言中的原子类型主要有3 种，它们z 、n 和陂类型。z 是整数，n 是非负整数， 耐是实数。所谓的原子类型是指这各类型的数据或变量，不能再分为更小的类型。 根据z 语言中“类型那是集合”的说法z 、n 和陵都是无限集。因此，计算机无法 实现这3 种原子类型的以下两个方面的功能。 ( 1 ) 计算机的存储器的容量有限，无法在存储器中枚举无限集； ( 2 ) 计算机只表示无限集中较“小”的元素。如：2 个字节的存储空间，能表示的 最大的自然数是6 5 5 3 5 。 一般来说z 语言的类型在z 语言中有两个含义：一是“类型”用于变量的定义， 二是一个“类型”表示一个集合。单就“类型”的第一个功能来说，计算机是可以实现 的。如：在z 的规格说明中定义一个整型的变量n 的形式为“1 3 , ：z ”，我们可以用以c 语言“i n tn ；”来实现它。z 类型的另一个含义是，一个z 语言的类型是一个集合，它可 能是有限集，也可能是无限集。前面提到过，无限集是不可实现的，所以这是需要约束 沈阳工业大学侦。j 一学位论文 的地方。 因此，在s m a r tz 中，对z 、n 、p 的使用作如下的规定： ( 1 ) 他们只能用于定义变量； ( 2 ) 他们不允许用于表示一个集合，如：“a u z ”是非法的。 f 3 1 这些类型的变量值有上限和下限。 z 语言经过以上约束后，z 、n 、酸三种类型可以分别用c + + 语言中的i n t ，u n s i g n e d 和d o u b l e 类型来实现。而且z 、n 、融三种类型的允许值要与i n t ，u n s i g n e d 和d o u b l e 类 型相符。 z 语言中的类型都属于强类型，每一个变量或常量都有一个唯一确定的类型。 z 语言中z 、n 、陵都是算术数值类型，这3 种类型的变量支持运算+ 、一、+ 、d i v 、 r o o d ，即“加、减、乘、除、求模”运算。运算支持隐式类型转换，其转换规则与c + + 相同。 数值越界错误处理要在实现中给予相应的实现。 z 语言中还有一种常用的数据类型是删l ，即自然数类型，其处理方式与n 相似。 关于z 语言中的基本类型( b a s i ct y p e ) ，它是由用户引入到规格说明中的一种没有 任何内部信息的纯抽象类型。这种类型的实现应该在其它类型实现的基础上，因此可以 作为后续课题进行研究。 本课题在实现原子类型的实验中将只验证z 类型，其它几种原子类型将不在实验范 围之内。 2 3 2 幂集类型约束 z 语言中的幂集类型有4 种：幂集、无空集有限幂集、有限幂集和无空集有限幂 集，它们分别由符号p 、p 1 、f 、p l 定义。以z 语言中的z 类型为例，则以上幂集有如 下关系， pz p 1z 口z f 1z ， pz 、p 1z 与f2 、f 1z 的区别是pz 、p lz 可以包含无限集，因此必须对无限幂集加 以约束，在s m a r t z 中规定符号p 和b 的使用方法为， ( 1 ) p 目护l 的后面为集合或类型； 沈阳工业大学硕十学位论文 ( 2 ) 它们的意义约束为有限幂集； ( 3 ) p 、p l 、f 、f 1 只能用于变量的定义，而不能用做表示一个集合。 这样对z 语言约束的结果是p 、p 1 与耐、廿i 的用法就没什么区别了。由于它们的功 能相似，所以在s m a r tz 的验证实验中将只验证p 实现，而且只考l 静的一层嵌套。 相似地，笛卡儿积，关系，函数，序列和包的类型都不能用作表示一个集合，而且 不能用于定义无限聚集。 2 3 3 集合的约束与可判定性 集合是z 语言中十分重要的一个概念，z 语言中大部分聚集类型都是用集合定义 的。z 语言中的集合是一个数学概念，它的内涵十分的丰富。 集合在z 语言中主要以3 种形式出现：一是以枚举形式出现，二是以谓词描述的形 式出现，三是以集合运算的形式出现。 ( 1 ) 枚举集合。以“ e l ，e 2 ，e 。) ”形式出现的集合称为枚举集合。这种集合通常用 来表示一个集合常量。其中e ，e 2 ，e l l 为同一类型的常量，它们之间是互斥关系。这 种集合的表达方式通过枚举集合中的每一个元素，来达到再现这个集合的目的。这一类 集合的元素数量是有限的，元素之间是互异的，因此它是一种典型的离散数据结构，很 容易为计算机所实现。例如：若有枚举集合s e t - ，则它与物理存储器 m e m o r y 的映射 方式为 s e t 卅m e m o r y 。 ( 2 ) 抽象集合。以“ s c h e m a - t e x tf e x p r e s s i o n ”形式出现的集合称为抽象集合。 这种集合表示法不是通过枚举方式描述集合，它描述了集合中所有元素的共性。具体地 说，这种集合表示法给出的可能是一个谓词，你可以通过这个谓词来判断某个元素是否 是这个集合中的一员；也可能，这个表示法给出了集中每个元素的生成法则，你可以通 过这个法则写出这个集合中的每个元素。一般来说，你无法直观地了解到集合中的元素 到底是什么样的，本文称之为抽象集合。 抽象集合可以描述为2 元组( e l e s e t ，p r e d ) 或( e x p ，e l e s e h ) ，其中e l e s e t 为集合元素 的类型，p r e d 集合元素所满足的谓词，e x p 集合元素生成函数，e l e s e t 2 函数的定义域。 沈阳工业人学硕i 嘈位论文 因此如果e l e s e t 、p r e d 、e x p 、e l e s e t 2 的数据结构是明确的，那么抽象集合的数据结构 也是可以实现的。 ( 3 ) 通过集合运算得到的集合。z 语言中集合的运算符有“l j f ，、_ ，一、一”，它 们都是2 目运算符，它们代表了集合运算“并，交，差”。 两个枚举集合并、交、差运算，这几个算法可归约为两个集合的有限序列的条件并 归问题。我们可以使用多带图灵机来模拟集合运算，来证明枚举集合的并、交、差计算 机是可以实现的。 设有一多带图灵机m 其输入字母表= 0 ，1 ，存) ，纸带1 、纸带2 和纸带3 的字母 表r 1 = r 2 = f 3 = ( 0 ，1 ，样，一 ，纸带l 上的字串为“# w t 撑w 2 # 舳，捍”，纸带2 上的字串为 “# u l # u f _ u r i # ”，w l ，w 2 ，m ，h i ，u 2 ，u n 0 ，1 ) ，纸带3 为空纸带，即其上 只有空白字符“一”。纸带1 、纸带2 、为输入带，分别代表集合1 、集合2 ( 两集合不 为空，且不含空串) 纸带3 为输出带，用于计算两个集合的运算结果。两个集合并的 步骤为： 1 ) 检查纸带1 任意两个相临“# ”字符间的字串是否相异，如果有相同字串，则 拒绝，否则，转向步骤2 ： 2 ) 用相同的方式检查2 号带，如果有相同字串，则拒绝，否则，转向步骤3 ： 3 1 拷贝字串1 到字串3 ； 4 ) 扫描字串u l ，0 2 ，每扫描一个u 。( 15i 茎n ) ，检查u 是否在w i ， w 2 ，w 。中出现过，如果没出现，则将u i 拷贝到纸带3 最后一个撑后面，然后再添写 一个分隔符撑。如果读到纸带2 的最后一个# ，则接受。 同理，只要适当的修改算法的3 、4 两步即可得到“交”和“差”的算法。 出于表示集合的符号串是有限的，故上述算法总能停机，因此上述算法是可判定 的。由于图灵机是通用计算机模型，因此可以得出结论：枚举集合的“并、交、差”运 算在计算机上是可以实现的。 现在考虑枚举集合的关系运算和至算法的可行性，用图灵机模拟这两个符号的算 法。 沈阳工业大学颀= 亡学位论文 包含运算“”的图灵机m l 为双带图灵机，1 号带上的左部开头的字串为 社w l # w 2 # # w 。撑，其余的部分为空字符“一”，其中w 。( 11i sn ) 0 ，1 2 号带为输入 带，带上左起开头字串为u e o ，1 ) ，其余的字符为“一”。m 1 按如下的步骤运行。 1 ) 检查1 号带上任意两个“# ”字符间的字串是否相异，即w i ，w 2 ，w 。互不 相同。如果有相同字串则拒绝，否则进行步骤2 ； 2 ) 将2 号带上的字串u 与】号带上的字串相比，w 1 ，w 2 ，w n 若有一个与u 相 同则接受，否则拒绝。 实现“”子集运算符的图灵机m 2 为双带图灵机，l 号带上的左部开头的字串为 i w l # w 2 # # w i n # ，其余的部分为空字符“”，2 号带为输入带，带上左起开头字串为 “# u i # u 2 # 样u | 1 # ”，w l ，w 2 ，w m ，u 1 ，u 2 ，u n o ，l 一 0 ，l 一其余的字符为 g g ” 一 o 1 ) 检查1 号带上任意两个相临“# ”字符间的字串是否相异，如果有相同字串则拒 绝，否则，转向步骤2 ： 2 ) 用相同的方式检查2 号带如果有相同字串则拒绝，否则，转向步骤3 ； 3 ) 置i = l ，将2 号带上的u i 与1 号带上的字串与2 号带相比，如果w l ，w 2 ，w 中有一个字串与u i 相同，则置i - i + l ，重复步骤3 ，直到i n 为止，若没有不同则接 受，否则拒绝。 由于用于表示集合的符号串到是有限的，故上述算法总能停机，因此上述算法是可 判定的。枚举集合的所有包含和子集问题，如：正和c 都可以归约到上述的算法。因此 可以得出结论：枚举集合的包含和子集关系是可判定的。即可以找到一个算法，使计算 机自动完成集合包含和子集的判断功能，这对于z 规格说明的自动求精有很重要的意 义。 综上所述，z 语言枚举集合的运算和关系都是可判定的。因此枚举集合是不需要约 束的，还充分的实现它的作用。本文所讨论的s m a r tz 将只包含两个数据类型：z 和只 包含一级嵌套的枚举集合。一方面，它们是从z 语言中继承下来的，另一方面又做了必 要的约束，并兼顾了未来的可扩展性，因为相似的问题是可以归约到一个典型问题上 的。 沈阳工业大学倾- i _ 学位论文 至于抽象集合，其元素的抽象性决定了它相关运算的实现算法会比较复杂。若同时 考虑与枚举集合之间的运算，则处理的复杂程度将更大。在本文中将不会重点讨论抽象 集合的实现，但是可以作为后续课题研究。 2 4z 语言的谓词约束 2 4 1 谓词的约束与可判定性 由于s m a r tz 中的类型受限，自然地，s m a r tz 中的谓词也受到了制约。但是s m a r t z 谓词的其它功能并未受到任何本质上的影响。 在z 或s m a r t z 中，谓词为如下形式， q u a n t i f i e rb a s i c - d e c l l ；b a s i c d e c l n ，ip r e d i c a t e l - ，p r e d i c a t e 2 其中，q u a n t i f i e r 为量词。上面的形式等价于 ( q u a n t i f i e rb a s i c d e c l l p r e d i c a t e lap r e d i c a t e 2 ) ( q u a n t i f i e rb a s i c - d e c l 2 p r e d i c a t e l p r e d i c a t e 2 ) ( q u a n t i f i e rb a s i c - d e c l 。p r e d i c a t e l p r e d i e a t e z ) 因此，问题可以归约为 q u a n t i f i e rb a s i c - d e c l p r e d i c a t e 进一步展开， q u a n t i f i e rd e c l - n a m e l d e c l - n a m e m ：e x p r e s s i o n 。p r e d i c a t e 等价于 ( q u a n t i f i e rd e c l - n a m e l ：e x p r e s s i o n 。p r e d i c a t e ) ( q u a n t i f i e rd e c l - n a m e 2 ：e x p r e s s i o n p r e d i c a t e ) ( q u a n t i f i e rd e c l - n a m e m ：e x p r e s s i o n 。p r e d i c a t e ) 因此问题可此归结为 q u a n t i f i e ri d e n t ：e x p r e s s i o n p r e d i c a t e i d e n t 是p r e d i c a t e 的形式参数，e x p r e s s i o n 指定了形式参数的取值范围。所以z 语言的 谓词可以描述为3 元组( q u a n t i f i e r , s e t ，p r e d i c a t e ) ，其中，q u a n t i f i e r 为量词，s e t 为集 沈阳工业大学硕上学位论文 合，p r e d i c a t e 为谓词。在z 语言中s e t 是可以为无限集的集合，这对于计算机来说将无 法完成类集合的元素的遍历，因此在s m a r tz 中规定，s e t 所描述的集合，只能为有限 集。 p r e d i c a t e 为一个单参数函数，其返回值为t r u e 或f a l s e ，它可以描述为个2 元组( t p ) ，即一个实参加一个算法。这个单参数算法可由一个单带图灵机m p 来模拟，m p 是一 个7 元组( q ，f ，6 ，s ，b ，f ) ，其中是字母表，其中 ( 1 ) q 为状态集； ( 2 ) 为输入字符集，中不包含空格符e ； ( 3 ) r 为带字符集，e - - - - - f ，e r ； ( 4 ) 6 为转移函数，6 = q r q 1 1 r l ) ； ( 5 ) s 为起始状态，se q ； ( 6 ) b 为拒绝状态，be q ； ( 7 ) f 为接受状态，f q 。 因此，m 。可以被形式化为一个广义表，而这个广义表字串就可以为另一个图灵机识别 并模拟，因此我们可以设计一个图灵机调用m 。 设有图灵机m 3 识别语言( q ，s ，m p ) ，其中字符q v ，j ，s 为元素类型为t 的枚举集合，m 。为参数类型为t 的单参函数。则m 3 按如下步骤运行： (