（计算机软件与理论专业论文）xml数据库类型系统研究.pdf

华中科技大学硕士学位论文 摘要 随着电子商务、电子政务等网络应用需求的不断增长，可扩展标志语言数据库 ( e x t e n s i b l em a r k u p l a n g u a g ed a t a b a s e ，x m ld a t a b a s e ) 技术成为了现代数据库技术 的重要研究领域之一。为了实现对多源异构数据信息的有效管理，x m l 数据库必须 拥有完善的类型系统和灵活的类型处理机制，因此x m l 数据库技术的迅速发展，直 接推动了对x m l 类型系统的研究与开发。基于目前x m l 类型处理问题的研究现状， 对x m l 数据库类型系统的形式化建模、类型验证和类型检验等问题进行了研究探讨。 首先采用一种基于类型原理的形式建模技术创建了一个基于x m l 模式( x m l s c h e m a ) 的x m l 类型系统形式化模型，给出了整个模型的形式化描述，并对模型进 行了扩展，通过对扩展模型的应用实例分析体现了该模型易于扩展、实用性强等优点。 针对x m l 数据库类型验证问题，对几种x m l s c h e m a 类型验证方法进行了分析 与比较，然后选择其中一种基于树自动机的类型验证方法进行深入研究，指出该方法 所用算法存在局限性，继而对算法提出了改进，分析了改进后算法的正确性和复杂度。 针对x m l 数据库类型检验问题，以基于文档类型定义( d o c u m e n tt y p e d e f i n i t i o n ， d 1 m ) 的x m l 类型检验的研究为基础，对基于x m l s c h e m a 的类型检验问题的可确 定性和检验算法进行了讨论，证明只有对发布或转换程序的处理能力加以限制后，一 些可确定的基于d t d 的类型检验问题在基于x m ls c h e m a 时才可确定，最后将两个 基于d t d 的类型检验算法引入基于x m ls c h e m a 的类型检验中，分析了算法的适用 范围和复杂度。 最后为x m l 数据库x d m 的类型处理系统提出总体设计方案，基于已改进的类 型验证算法实现了x m ls c h e m a 类型验证，采用引入的类型验证算法实现了x q u e r y 中的类型检验。 关键词：可扩展标志语言数据库，类型系统，形式化建模，类型验证，类型检验 华中科技大学硕士学位论文 a b s t r a c t w i t ht h ei n c r e a s i n gd e m a n do fv a r i o u sw e b a p p l i c a t i o n s ，x m l d a t a b a s et e c h n o l o g yh a s b e c o m ea ni m p o r t a n tr e s e a r c ha r e ao fa d v a n c e dd a t a b a s et e c h n o l o g i e s t h er e s e a r c ho ft h e t y p es y s t e mo ft h ex m l d a t a b a s ei sak e yf i e l do fr e s e a r c h i n gx m ld a t a b a s es y s t e m a c c o r d i n gt o t h ec u r r e n tr e s e a r c hs t a t u so fx m l t y p ep r o c e s s i n gp r o b l e m s ，w e w i l l i n v e s t i g a t et h et y p e v a l i d a t i o na n d t y p ec h e c k i n gp r o b l e m s f o rt h et y p es y s t e m so ft h ex m l d a t a b a s ed e e p l y w ef i r s tp r o p o s e sab a s i cf o r m a lm o d e lf o rt h ex m l t y p es y s t e mu s i n gap a r t i c u l a r l o g i c a lf o r m a l i s mm o d e l i n gt e c h n i cb a s e d o nt y p et h o e r y , w h i c hc a nr e a l i z e st h ef u n c t i o no f t y p ed e f i n i n ga n dt y p ev a l i d a t i n go f x m ld a t a a f t e rt h a tt h eb a s i cm o d e li sw e l le x t e n d e d t os a t i s f yx q u e r y t y p e c h e c k i n gr e q u i r e m e n t 。 f o rt h et y p ev a l i d a t i o np r o b l e m ，w ec o m p a r ea n da n a l y s i ss e v e r a lm e t h o d st od e a lw i t h t h i sk i n do f p r o b l e m ，e s p e c i a l l yf o c u so nt h em e t h o db a s e do nt r e ea u t o m a t o n s ，a n dp r o p o s e am o d i f i c a t i o nf o rt h ea l g o r i t h mu s e db ys u c ham e t h o d f o rt h et y p e c h e c k i n gp r o b l e m ，w ef i r s td i s c u s st h et w op a r t i c u l a ra p p l i c a t i o n s ，t h eo n e d u r i n g t h ex m l p u b l i c a t i o n o fr e l a t i o n a l d a t a b a s e , a n d t h eo n e d u r i n g t h ex m l t r a n s f o r m a t i o n t h e nw ed i s c u s s e dt h ed e c i d a b i l i t yo f 的t hp r o b l e m sw h e nu s i n gx m l s c h e m at op r e s e n tt h et y p eo nt h eb a s eo ft h er e s e a r c ho fs u c hk i n do fp r o b l e m sw h e nu s i n g d t dt o p r e s e n t t h et y p e w ep o i n to u to n l yw i t ht h ec o n s t r a i n so ft h ep u b l i s h i n go r t r a n s f o r m a t i o no ft h ex m lt h et y p e c h e k i n gp r o b l e mi sd e c i d a b l ea n da l g o r i t h m sc a nb e a v a i l a b l ew h e n u s i n gx m l s c h e m ai n s t e a do fd t d t op r e s e n tt h e t y p e f i n a l l yw ep r o p o s e t h ed e s i g no ft h et y p e p r o c e s s i n gs y s t e m o fx m ld a t a b a s ex d ma n d r e a l i z ei tb a s e do nt h ea l g o r i t h m sa l r e a d yi n t r o d u c e d k e y w o r d s ：x m l d a t a b a s e ，t y p es y s t e m ，l o g i c a lf o r m a l i s mm o d e l i n g ，t y p ev a l i d a t i o n ， 甜p e c h e c k i n g 独创性声明 本人声明所呈交的学位论文是我个人在导师指导下进行的研究工作及取得 的研究成果。尽我所知，除文中已经标明引用的内容外，本论文不包含任何其他 个人或集体已经发表或撰写过的研究成果。对本文的研究做出贡献的个人和集体， 均已在文中以明确方式标明。本人完全意识到本声明的法律结果由本人承担。 学位论文作者签名：未1 一f r 日期：- 2 嘶年占月p 日 学位论文版权使用授权书 本学位论文作者完全了解学校有关保留、使用学位论文的规定，即：学校 有权保留并向国家有关部门或机构送交论文的复印件和电子版，允许论文被查阅 和借阅。本人授权华中科技大学可以将本学位论文的全部或部分内容编入有关数 据库进行检索，可以采用影印、缩印或扫描等复制手段保存和汇编本学位论文。 保密口，在年解密后适用本授权书。 本论文属于 不保密口。 ( 请在以上方框内打“”) 学位论文作者签名：蟊1 4 - 日期：o 印牟年占月7 日 ；鳓燧名：冯 小牛年s 月c 7 日 华中科技大学硕士学位论文 1 绪论 1 1 课题研究背景、目的及意义 电子商务、搜索引擎、电子政务等领域的兴起极大地刺激了w e b 信息管理技术 的迅猛发展。作为x m l 技术与数据库技术紧密结合的产物，x m l 数据库既具有x m l 在多源数据交换和信息传递方面的天然优势，又体现出数据库在处理多元信息时的 系统性和高效性，因此为多数据源的w e b 信息管理开辟出一片新天地【”。随着对x m l 数据存储、查询、转换、压缩等技术的深入研究，x m l 数据库技术已成为现代数据 库技术的重要研究课题【2 】。 虽然所有的x m l 数据库专家中有一个共识：x m l 数据库不会代替传统的关系 型数据库，但是，由于x m l 应用是个新兴的成长领域，且有着潜在而广大的市场， 不管是传统的关系型数据库厂商的介入，还是新x m l 数据库厂商的全面突入，都可 能给主流数据库市场格局带来变数【卦。目前，x m l 技术已开始在越来越多的新兴行 业中发挥主导作用，如在数字图书馆中，如果数据源都是以x m l 格式为基础，那么 必须使用x m l 数据库来对各种数据进行有效管理；又如专利局也是x m l 数据库的 应用领域，它使用x m l 数据库对其电子文档进行高效管理；再如，对未来的医疗保 险行业而言，依靠以往的关系型数据岸已经无法有效地描述和交换病历文档：又如 在电子政务应用领域中，传输的文件多是文档信息，且侧重描述、查询以及管理方 面的应用，而不是计算和分析处理，因此关系型数据库不能最佳地处理这些数据文 档。与一般的数据文件不同，x m l 不建立在任何应用程序之上，文件传输交换存取 及操作不会受到应用程序的制约，因此可以对其进行广泛的使用【4 1 。 为了实现对多数据源信息的有效管理，x m l 数据库必须拥有完善的类型系统和 灵活的类型处理机制，以实现对各种x m l 数据的类型定义和类型处理。x m l 数据 库技术的迅速发展，直接推动了x m l 类型系统的研究与开发。一个完善的x m l 类 华中科技大学硕士学位论文 型系统应具有类型定义( t y p ed e f i n a t i o n ) 和类型检验( t y p ec h e c k i n g ) 两项基本功 能【5 】。通过定义类型，x m l 文档中的属性和元素的数值范围可以得到明确界定，具 有相同或相似特性的数值可以得到有效的分类管理，应用程序的可重用性也将得到 提高；通过类型检验，在静态编译阶段就可以发现和避免程序动态执行时可能出现 的类型错误，从而保证了程序的稳定性和可靠性。一个与类型定义密切相关的问题 是类型验证( t y p ev a l i d a t i o n ) 问题。与类型检验不同，类型验证技术主要是用于验 证x m l 数据是否符合相应的类型特性，而类型检验则是判断数据发布或转换的结果 是否符合相应的输出类型【6 】。 针对国家电子政务、网络教育等应用领域在数据处理方面的应用需求，我们在 自主版权的国产数据库管理系统d m 的基础上开发能直接存储和检索x m l 数据的数 据库管理系统x d m ，为x m l 数据管理提供基于关系数据库架构的解决方案。作者 承担了其中“x m l 类型处理系统”的研究和开发工作，其目的是使通过对x m l 类 型系统的形式化建模、类型验证以及类型检验问题的研究，为x d m 设计并实现一个 x m l 类型处理系统，使x d m 能在管理x m l 数据时更高效准确地处理类型。 1 2 国内外研究概况 1 2 1x m l 数据库技术概况 1 关系数据库对x m l 的支持 x m l 正快速成为网络数据交换的国际语言，而在数据库领域内，x m l 数据库 的理论研究和应用开发也成为众人瞩目的焦点。2 0 0 2 年，一些主要的关系型数据库 供应商，如m m 、o r a c l e 、m i c r o s o f t 分别在它们的数据库产品中加强了对x m l 的支 持，以寻找x m l 技术的突破点，增强自身产品竞争的技术“亮点”。而且，m m 、 o r a c l e 和m i c r o s o f t 都公开声称它们对x m l 的支持将使数据库的运行速度更快。 o r a c l e 数据库营销副总裁r o b e r ts h i m p 说，o r a c l e9 i 第二版发布时，将会是一 个“完全一体化的x m l 和关系数据库”；i b m 则强调，其d b 2 和x m l e x t e n d e r 的 华中科技大学硕士学位论文 蹈合将提供闻o r a c l e 公司炎似的x m l 技术；s y b a s e 公司最新版企业级智能数据管 理系绞a s e 已可实现在数据库中避圣亍x m l 文档鲍存储霸检索；阏时，微软推出 款代号为y u k o n 的新s q ls e r v e r ，也提供对x m l 的支持。 来鸯德国s o f t w a r e a g 的技术麟闻武强表示，一些关系漤数摇鼯厂商蠢对乡 夸大 它们x m l 支持能力的嫌疑，认为它们不可能属于真正意义的x m l 数据麾。面对这 种争议，著名的x m l 技术专栏作家k e v i nw i l l i a m s 曾这样分析：“对于什么才是x m l 数提疼一豢骞嚣秽不嚣意煲：一部分人认为，只骞数摆痒凌部鞋x m l 穆式存馕熬数 据库才叫做x m l 数据库；另一部分人则认为，只婴能存储和处理x m l 文件，就可 阻称之为x m l 数据库。”为了平患这场争论，静者被定义为本源x m l 数据洚 ( n a t i v e x m l d a t a b a s e ，n x d ) ，聪者则被定义为支持x m l 的数掇库( x m l e n a b l e d d a t a b a s e ，x e d ) 。随着x m l 技术的不断擞展，又出现了第三种x m l 数据库，即混 合x m l 数据痒( m i x e d 。x m l d a t a b a s e ，m x d ) ，它鼍嗣翼雩爨青蘸嚣者熬莱蹙特毪纠。 目前，主流的关系型数据库供应商都采用x e d 方式提供对x m l 的支持，它们 静数据库内部仍然采用原有的表格式存储，当用户进行x m l 查询成其他处理时，邋 避各辩技术实现关系数据到x m l 数据的映射或转换，从焉在关系数据瘴上剁建x m l 视图，使用户或商业伙伴能在网络上更方便地进行数据交换。然而，由于数据库必 缀耋毅整合原有的数据，数据躬楚毽速度鑫然会受爨影穗蚪越。 2 本源x m l 数据库 n x d 则不存谯上述这些问题，因为它在存储x m l 文件时会创建一个基于x m l 豹模型，蒸中包搀多层嵌囊，壹予宠整遗像存了x m l 的分层结稳，因此在处理数攥 时无需进行格式转换，从而可以拥有更高的处理效率【皓】。 t a m i n o 是s o f t w a r e a g 公司推出的、韭莽第一个本源x m l 数据库。它掇供了对辩 种信息的程取，其整合的接口模块允许t a m i n o 从不同的数据源读取船部傣息，这魑 数据源包括d b 2 、o r a c l e 替主流关系数据库和面向对象数据库，甚至是使用o l e ，d b 豹o f f i c e 系统。翔渠金鼗蠲户穰蠢多i 孛粪整豹轰台数攥瘁以及不鲻类型黥应曩，粼 华中科技大学硕士学位论文 在应用层和厝台数据库之间增加对x m l 的支持会需要很高的技术成本，而t a m i n o 提供豹编程按日和数据访滴方法支持多释应阁和数箍源，无辩取代蔫户已有数据源。 n x d 在其中就充当逑接后台数据源与前端成用的中闻缓冲层，执行x m l 转换、存 储、检索等操作，从而解放了后台数据库，让它在执行更为煎要的事务处理。不过， 懿巢金监熬数据源擎一，裁没鸯太大必要镬溺这群鹣系统，蠢为鬟麓擎一数据添麴 x m l 处理能力相对采说不需臻太高的费用。 除了s o f t w a r ea g 公司的t a m i n o 外，x y z f i n d 公司的x y z f i n d 服务器以及 & i a s o 建公司斑晶的t e x t m l 服务器都蹙典型戆n x d 产品。嚣内在这方西的磺究虽起 步较晚，但也取得了一些成果，如武汉华工迭梦数据库有限公司自主开发的数据库 管璞系统x d m 纛黧，莪器经实魏了对x m l 鼗猫静存镶功姥瞄及对壹诲语言 x p a t h l 。0 的支持。 1 2 2x m l 数据库类型系统问题研究概况 嚣翦，太 f l 对x m l 数据痒类型系统戆类型验迁移类型捡验淹题逐在进露不叛的 研究。由于存在众多被广泛使用的x m l 发布和转换语言，如x p a t h l l 4 l ，x h t m l l l 5 l ， x q u e r y 1 6 t “，x m ls q l 1 8 , 1 9 1 ，x d 粥e 图等，校罐臻巢一稀形式的语荫来进行统一酌 描述。此外述存在各式各样的x m l 横式语言，如x m l s c h e m a 2 1 2 2 1 ，r e l a x ，t r e x ， r e l a xn g ，s c h e m a t r o n 等例。发布和转换语言以及模式语畜的多样性无疑都使得 x m l 类鍪骏涯窝类蘩捡验滔蘧懿磅究对象遘予繁杂，绘类羹验证嚣类型捡验润嚣静 解决带来了一定的困难。然而，困难并不能阻止人们前进的步伐，圈内外的很多专 家学者经过多年的研究，已缀提出了些解决特定润题的技术帮方豢。 1 类型系统的形式化建模 炎型系统的形式化建模技术最早是由l u c ac a r d e l l i 在文献【2 4 】中提出的。在该文 献中，l u c a 放蒋统穗惠理论蓿手，袋雳逻辚化形式建模技术，捷密了个鏊于类墅 原理的类型系统形式化模型方法：为实现类泌定义和类型检验功能，类型系统被建 模成词汇衰( s y n t = ) 、判断集( j u d g m e n ) 和类型规则集( t y p e r u l e ) 三部分：词汇 4 华中科技大学硕士学位论文 表和判断集的一部分绘出各尝型的形式化描述，用于实现类型定义功能，另一部分 判断榘则给出各种类跫处理梳制的形式纯描述，并通过类型瓶鲻集中的逻辑化公式 提供这些处瑗极剑黪援则以及规则阈浆推导关系，零鼹这些类型处溅枧制可以实现 类型检验功熊。这种技术已缀被广泛应用各种传统的过程式和函数式语言的类型系 统静镬建帮分耩。 2 x m l 类型验证与类型检验 文献 2 5 3 0 1 对于x m l 的模式语商以及类型系统进行了深入研究，讨论了x m l 模式与关系数握模式之凌鲍涎、联系以及提蔓转换黪方法。文簸 3 0 1 孛还绘出了一穆 基于x m ls c h e m a 的x m l 类型验诞系统的原型，通过使用树自动机来描述x m l s c h e m a 实魂辩输入文档的类挺验证。可敬证嘲在一般清况下，徐定两种类鍪t l 和t 2 ， 验 正楚否t l - - t 2 的问题的复杂性为指数级，蕊当t 2 能由一个确定树舞动机产生时， 其复杂度为多项式级1 3 l i 。在文献【3 2 】中，m n i c o l a 和j j o h n 则从x m l 解析器的分 辑凄发，逶遘增热其有类垄检验珐畿瞧过滤绥来实瑷对类壁羧谨豹支撩。 在x m l 类型检验问题的研究领域，国际上一些学者做了比较多的研究。例如在 文献【3 3 中，d a n s u c i u y i 等入指出：警对x m l 文档的处理包含数值阮较时，处理过 程中驹类型梭验闯磁变褥不w 确定。他们对嚣翦x m l 类型检验的应用实例进霉亍了分 类统计，发现可归纳为两类应用需求，一种是在x m l 数搦库的数据发布( x m l p u b l i s h i n g ) 道程孛透孳亍类型捡验，一耱羯莛在x m l 数据的转换( x m l t r a n s f o r m a t i o n ) 过程中进行，在这两种情况下都存程着类型检验的可确定性范围。文章还分析了类 型掖导( t y p ei n f e r e n c e ) 问题，以及用类型推导的方法解决类型验诞问题的有效性 蠢爨疆性，实际上类型推导淘题浆鲻决姆蹇接导致类裂检验鲻题的鳃决。 文献3 4 ，3 6 对在关系数据库中发布x m l 数据过程中的类型检骏问题进行了深 入研究。其中，文献【3 4 】专门针对嗣d t d 表示输入输岛类型瓣情况避行了搽讨。文 献【3 5 3 6 】则通过对发布函数、关系数据库约东集合以及输出结果类型这三个霪要参 数进行讨论，得到了各种情况下类型检验问题的可确定性区间，并掇出了一种特定 5 华中科技大学硕士学位论文 情况下的多项式时间级的类型检验算法。 。在文献 3 7 】中，t o v am o l i 等人对不考虑结点上数据值连接时的类型检验进行了 深入研究，他们发现大多数对x m l 文档的处理操作都可由一个k - p e b b l e 树转换器 来描述，而x m l 文档则可以被抽象成为一棵带标记的有序树，这种情况下的类型检 验问题是可以确定的。他们还使用s i l k r o u t e 技术和t r e e q l 语言对一些x m l 发布中 的操作进行了形式化描述，实现了处理过程中的类型检验。 在文献 3 8 1 中，m a r t e n s 等人使用自上而下的无阶转换器描述对x m l 的转换， 并对输出类型为d t d 和树自动机两种情况都进行了分析。 在文献 3 9 1 中，t o v am i l o 和d a ns u c i u 再次分析了x m l 转换过程中的类型检验 问题，这一次他们考虑了结点上的值连接问题，通过分析指出：当转换程序的处理 能力被限定在一定的范围内，且对输入输出类型都作进一步的限制的时候，可以实 现这种情况下的类型检验。在提供相应算法的同时也指出，这种考虑了结点上值连 接的类型检验问题的复杂度相当高。 在文献【4 0 中a t o z a w a 对x s l t 转换语言的静态类型检验进行了深入的分析， 提出了一种新的类型检验算法。 x m l 数据库类型系统是一个比较新的研究领域，国内致力于x m l 类型系统问 题研究的学者并不多。目前国内还没有一个系统能够实现较高级别的类型检验要求， 对一些特定的类型检验功能，也没有相应的工具予以支持。 1 - 3 课题主要研究工作 随着x m l 技术的不断发展和在电子商务、搜索引擎、电子政务等全新领域的广 泛应用，x m l 数据库的开发与研究越来越成为人们关注的焦点。设计和开发x m l 数据库管理系统的一个重要目标就是为网络中的异构数据源提供良好的存储访问管 理和数据交换机制。 本课题来源于国家8 6 3 高技术研究发展计划资助项目( 2 0 0 2 a a 4 2 3 1 1 0 ) “国产分 6 华中科技大学硕士学位论文 布式数据库管理系统d m 4 的研究与开发”。该课题要求开发能直接存储和检索x m l 数据的x m l 数据库管理系统d m 4 ，为x m l 数据管理提供基于关系数据库架构的解 决方案，为实现这一目的，我们首先为d m 4 设计一个x e d 的原型系统x d m 。作者 负责其中的x m l 类型处理系统的研究和开发工作，主要包括：对x m l 类型的体系 结构进行分析，实现对x m l 的类型验证功能，并对x m l 发布和转换过程中的类型 检验机制进行研究与实现等。在研究过程中，由于受时间所限，作者主要致力于基 于x m l s c h e m a 的类型验证和x q u e r y 查询处理过程中的类型检验技术的研究。 概括来说，本课题的主要研究工作有以下几个方面： 1 对类型原理进行深入研究，利用形式化模型的形式简洁、逻辑性强等优点， 运用一种逻辑化形式建模技术对x m l 类型系统进行形式化建模，并利用形式化模型 易于扩展的特点对其进行扩展； 2 深入研究x m l 数据库类型验证问题，重点讨论基于x m ls c h e m a 的类型验 证问题，分析和比较几种类型验证方法的优点与缺点，提出更完善的类型验证算法： 3 分析研究x m l 数据库类型检验问题，重点讨论在关系数据库中进行x m l 数据发布以及x m l 转换过程中的类型检验问题； 4 为x m l 数据库类型处理系统提供有效可行的设计方案，并予以实现。 7 华中科技大学硕士学位论文 2x m l 数据库类型系统形式化建模 由于x m ls c h e m a 支持多种数据类型的定义以及类裂的继承与复用，且易于扩 展，因而极大地弥补了d t d 在处理数据炎型方面的不足。为了使x d m 原型系统支 持更丰富靛x m l 数据类激，本耄烽怼一移基于类型原理瓣形式建模技术邈行骚究， 并采用该技术为x d m 创建一个熬于x m l s c h e m a 的类型系统形式化模型。 2 1 x m l 模式语言对汪l 类型系统的扩袋 嚣兹的x m l 模式语蠢有许多零申，如x m ls c h e m a ，r e l a x ，x d r 等，担出予 x m ls c h e m a 是唯一受到国际互联网联照( w 3 c ) 承认和推广的建议标凇，因此本 露将重煮对x m l s c h e m a 中提盘静各穆类整以及炎垄定义方式遂聿亍讨论。 x m l 是一种界定文本数据的简便而标准的方法，用户可以通过自定义标记来按 照自己的要求自由地组织x m l 文档，但怒当用户需要与其他人交流自己的x m l 文 撼瓣，努须透过蘩秘逶薅爨方式对其辏式绘予说甥，这秘方式豹懿体体现裁是文挡 类型定义( d o c u m e n tt y p ed e f i n i t i o n ，d t d ) 或x m l 模式( x m l s c h e m a ) 的编鬻， 两用来存储和管瓒x m l 数据的x m l 数撵库也楚通过这黧元数据对数据的类整特性 进行描述的。 d t d 描述了一类x m l 文档中标记及标记间嵌套的层次关系，重点强调结构的 约寒，露凝数据类墼绞索方瑟髓力缀嚣，它不支持数撂类囊定义。2 0 0 1 霉5 胃2 臻， w 3 c 推出了著名的x m ls c h e m a 规范，它层次化地描述了x m l 文档中数据的结构 关系和类型信息。与基本上只支持文本类型的d t d 不同，x m l s c h e m a 规范提供了 丰富魏数据类型： x m l s c h e m a 不仅定义了一燎内建的基本数据类型，还提供怒义新类型的功能， 镪括定义篱莘类黧和复杂类鍪。x m l s c h e m a 预定义了1 9 耱内建的简单炎鳖，热： 字符串数据( s t r i n g ) ，二元类型的布尔类型( b o o l e a n ) ，熬数( d e c i m a l ) 簿，此外逐 8 华中科技大学硕士学位论文 预定义了2 5 种常用的派生数据类型，并提供类型操作符“，”、“i ”和“& ”以及类 型出现次数限定符“* ”、“+ ”和“? ”来构造复杂数据类型。所有的复杂类型由 c o m p l e x t y p e 元素定义，它通常至少含有一个n a m e 属性，用在声明其他元素时被引 用，它也可以直接位于某一元素之内。此外复杂类型还包含一个内容定义类型，其 主要功能是定义类型所包含的内容模式。用户可以使用x m ls c h e m a 预定义的内建 数据类型，也可以自定义复杂的派生数据类型，这种模式语言的提出极大地丰富了 x m l 数据类型的描述方法，实现了对x m l 类型系统表达能力的有效扩充。 为了支持更丰富的x m l 数据类型，本章将以x m ls c h e m a 为基础，创建支持 x m l s c h e m a 的x m l 类型系统。 2 2 类型系统形式化建模技术 逻辑化形式建模【2 4 】是一种基于类型理论的形式化建模技术，它建立在严格的逻 辑数学基础上，创建的模型形式简洁、易于扩展且实用性强，因而被广泛应用于传 统程序语言的类型系统设计，成为各级别的类型系统设计开发的首选工具。 为实现类型系统的类型定义和类型处理功能，类型系统被建模成词汇表 ( s y n t a x ) 、判断集( j u d g m e n ) 和类型规则集( t y p e r u l e ) 三部分。词汇表和一部分 判断集给出各种类型的形式化描述，用于实现类型定义功能，而另一部分判断集则 给出各种类型处理机制的形式化描述，并通过类型规则集中的逻辑化公式提供这些 处理机制的规则和规则问的推导关系，利用这些类型处理机制可以实现类型系统的 类型验证和类型检验功能。下面分别介绍模型的各组成部分。 1 词汇表：一个标识符集，以标识符形式定义类型系统中的基本概念，并给 出语义说明。 2 判断集：一个判断式集合，它以判断式的形式描述了类型系统中所有的类 型处理机制。判断式的形式为“r l - 窍”，“l - j ，左边的r 为形式为 中，v i ：a i ，v z ：a 2 ， v 3 ：a 3 ，v 。：a i l l 的“值：类型”说明序列，它给出某静态类型环境( r e 所有数值v 9 华中科技大学硕士学位论文 的集合记为r 的值域d o m ( r ) ) 。“r 右边的窍为一个断言式( a s s e r s i o n ) ，它指出r 环 境下所采取的某种类型处理机制( 9 中出现的数值都在r 中给予声明) 。如：判断式 “fi t r u e ：b o o l e a n ”表示在静态类型环境r 下数值t r u e 具有类型b o o l e a n 。 3 类型规则集：一个逻辑公式集合，它以逻辑公式的形式给出各判断式之间的 逻辑推导关系，它们是整个类型系统进行类型推导的规则依据。类型规则式的描述 形式如表达式2 1 所示。 ( r u l en a m e ) p r e m i s e l ，p r e m i s e 2 p r e m i s e n ( 2 ，1 ) c o n c l u s i o n 括号中为规则名，横线上方为一组前提条件( p r e m i s e ) ，下方为结论( c o n c l u s i o n ) ， 前提和结论都以判断式形式给出。利用这种形式化模型，本文可以对x m l 类型系统 中的类型定义和类型处理机制进行简洁清晰的形式化描述。利用类型理论知识，还 可以扩充和修改词汇表、判断集和类型规则集，实现对模型的进一步扩展和完善。 2 3x m l 类型系统的形式化建模 将这种建模技术运用到x d m 的类型系统设计与开发中，能为其创建一个基于 x m l s c h e m a 的x m l 类型系统形式化模型。首先创建一个类型系统的基本模型，基 于它能对x m l 数据进行类型定义和类型验证，下一节中将对该模型作进一步扩展。 2 3 1 创建词汇表 首先，给出表2 1 所示的词汇表。表中将值划分为外部值和内部值两种：外部值v 是直接从x m l 文档中得到的文本值或节点值，内部值v 则是带有类型注释的语义层次 的数值，它通过对x m l 文档和对应的x m l s c h e m a 文档进行类型验证后得到。表中的 基本类型k 对应x m l s c h e m a 中定义的“种内建数据类型( 包括整型、浮点型、日期 类型等1 9 种简单数据类型和2 5 种常用的派生数据类型) ，类型操作符“，”、“i ”和“” 以及类型出现次数限定符“一、“+ ”和“? ”则用于构造复杂数据类型。除此之外还给 华中科技大学硕士学位论文 出了静态类型环境、空类型和空值的形式化定义。利用此词汇表，我们可以描述x m l s c h e m a 预定义的内建数据类型，也可以描述用户自定义的派生数据类型，也为判别 文档的有效性提供了便利。 表2 1词汇表 词汇说明 r静态类型环境 中空类型 ( ) 空值 k 基本类型 不含类型注释的外部值 v a含类型注释的内部值，其中下标标明其类型 a 。类型，其中大写字母代表类型名，下标代表类型结构体 ，j &类型操作符 o +?类型出现次数 2 3 2 创建判断集 基于上述词汇表，我们给出表2 2 所示的判断集，给出了“类型环境完备”、“类 型有效”、“定义为类型( d e f i n ea s ) ”和“具有类型( h a s ) ”等不同语义信息的形 式化描述，此外还给出了类型匹配、类型消除、类型验证以及类型的约束派生等类 型处理机制的形式化定义，这些处理机制将在类型规则集中给出具体的处理规则和 各规则间的推导关系。 表2 2 判断集 判断集说明 r l o k1 1 是一个完备的类型环境 r i a 在r 环境下a 是一个有效类型 华中科技大学硕士学位论文 袭2 2 判断集( 续) 判断鬃说明 f l d e fv ：&在r 环境- fv 蛉类型蔹定义为其有续撬体a 的类麓a ( d e f i n ea s ) r l v ：a在r 环境下v 具有类型a ( h a s ) r i v c c程r 环境下v 静模式结构与类型结构体匹配( m a t c h ) r l v = ) v a在f 环境下对外部德v 进行娄型验证褥到内部馕v a ( v a l i d a t i o n ) r i v = v程r 环境下对内部值v a 进行类型消除彳寻到外部值v ( e r a s u r e ) f l a b 函数类型( f u n c t i o n t y p e ) e 表达式( e x p r e s s i o n ) 2 4 。2 判断纂扩展 袭2 5 中给出判断集扩展部分的形式化播进。 表2 5掰增判断集 i词1 汇说明 f l d e f x ：a强境f 下变量x 的类型定义为a r i - d e f e ：a环境r 下表达式e 的结果类型定义为a r i e ：a环境r 下表达式e 的结粱具有粪挺a f ，a y ：a - b环境r 下函数f ( x ) - y 的类型定义为小) b r | ，f ( x ) 一 y ：缸8环穗f f 基数f ( x ) 一 y 其有类鍪a 一 b 1 4 华中科技大学硕士学位论文 2 4 3 类型规则集扩展 表2 _ 6 中给出类型规则集扩展部分的形式化描述。 表2 6新增类型规则集 规则式说明 ( s u b t y p e l ) 环境r f a 是自身的子类型。 r i a y ：a _ b r i y ：b 的类型定义为a 一 b ，则f ( x ) 一 y 具有类型a 一 b 。 r i f ( x ) 一 y ：a - b ( i f - e l s ee x p r e s s i o nt y p e ) 环境rfv l 的类型为b o o l e a n ，v 2 v 3 的类型为 r l v l ：b o o l e a nf i v 2 ：a r l v 3 ：b a ，b ，则i f v l t h e n v 2e l s e v 3 的类型为a lb 。 r l - ( i f v l t h e n v 2e l s e v 3 ) ：( a ib ) ( 1 e te x p r e s s i o nt y p e ) r i v ：a r ，x ：al f ( x ) _ y ：a - b环境r 下v