（计算机应用技术专业论文）omdoc在数学文档中的应用研究.pdf

江苏大学硕士学位论丈 摘要 不同的形式化方法不仅在学术研究中得到支持与倡导，而且目前已经广泛应 用到实际工业项目的各个方面。由于计算机系统越来越复杂，可能在一个系统中 需要用到多种形式化方法，因此十分有必要将不同的形式化方法进行集成，这对 于建立正确而严密的系统很有帮助。所有的形式化方法都是基于数学符号和知识 之上，o m d o c ( 开放数学文档) 作为一种x m l 应用，提出了一种针对数学注释 与概念的内容标记模式，为建立一种作为基于不同形式化方法的系统之间的交互 的内容语言提供了可能的基础。 本文首先对形式化语言交换格式( o p e n m a t h 和它的扩展0 m d o c ) 的有效性进 行了系统的研究，并在此基础上针对目前点对点翻译的不足，提出了一种新的基 于中间格式的集成方法，即以o m d o c 作为中间语言，将s p a r k 验证语言f d l 翻译为p v s ，从而自动地实现了两个著名的验证系统s p a r k 和p v s 之间的集成。 并且作为中间文档，产生的o m d o c 格式能够转换为其它的形式化语言从而将其它 形式化方法进行集成。由于o m d o c 格式的数学理论具有一致的x m l 树型结构， 对于各种可以与o m d o e 文档进行交互的系统而言，为其理论的修改和重用提供了 可能。最后设计并实现了一个简单的翻译器进行仿真实验，正确地实现了f d l 与 p v s 之间的单步和自动转换。 论文的主要创新点： 1 在语义层上，基于o p e n m a t h 和o m d o c 机制，提出一种以o m d o c 为中间 语言，进行s p a r k - f d l 和p v s 语言之间的转换，从而进一步实现两种验证系统 的集成方案。对于n 个系统之间的集成而言，传统的点对点转换需要进行n 2 次转 换，丽这种基于o m d o c 的转换方法则只需要2 n 次，降低了翻译过程中复杂度。 2 为了保证集成的完整性和有效性，自主研究并定义了私有字典，提供多个自 定义标记模式。实现s p a r k - f d l 语法与o m d o c 格式的转换，从而生成包含标准 字典和私有字典的o m d o c 文档，并通过个经过修改的接口，将该文档定制为特 定的、面向p v s 的o m d o c 文档，最后基于x s l t 样式表来实现与p v s 的语法转换。 3 针对f d l 中的声明、规则以及验证条件，分别定义常量、变量、类型声明 转换规则将所有的f d l 声明都转换为s y m b o l 和d e f i n i t i o n 元素片段：定义规则声 明转换，将所有规则都变为a x i o m 元素片段：验证条件表达式转换规则，将所有 的验证条件转为a s s e r t i o n 元素片段。 关键词：形式化方法，集成，o m d o c 方法，s p a r kf d l ，p v s ，中间语言 江苏大学硕士学位论文 a b s t r a c t d l n e r e n tf o r m a im e t h o d sh a v eb e e na d v o c a t e di na c a d e m i cr e s e a r c ha n dn o we v e n a p p l i e di nm a n yi n d u s t r i a lp r o j e c t sf r o md i f f e r e n ta s p e c t s a sc o m p u t e rs y s t e m sb e c o m e m o r ec o m p l e xi n t e g r a t i o na m o n gd i f i e r e n tf o r m a lm e t h o d si s n e c e s s a r ya n dc a r lb e h e l p f u li np r o v i d i n gac o r r e c ta n dr i g o r o u ss y s t e ma l lf o r m a lm e t h o d sa r eb a s e do n m a t h e m a t i c a ls y m b o l sa n dk n o w l e d g e o m d o c ( o p e nm a t h e m a t i c a ld o c u m e n t s ) ，a sa n x m la p p l i c a t i o n p r e s e n t sac o n t e n tm a r k u ps c h e m ef o rm a t h e m a t i c a ln o t a t i o n sa n d c o n c e p t s o m d o cp r o v i d e sap o s s i b l ei n f r a s t r u c t u r et os e r v ea sac o n t e n tl a n g u a g ef o r c o m m u n i c a t i o no f d i f f e r e n ts y s t e m sb a s e do nf o r m a lm e t h o d s i nt h i st h e s i s ，w ef i r s ts t u d ys y s t e m a t i c a l l yt h ee f f e c t i v e n e s so f t h ee x c h a n g ef o r m a t o ff o r m a ll a n g u a g e ( o p e n m a t ha n di t se x t e n s i o no m d o c ) ，b a s c do nw h i c hab r a n dn e w i n t e g r a t i o nm e t h o di sp r e s e n t e d ：u s i n go m d o ca st h ei n t e r l i n g u at ot r a n s l a t es p a r k v e r i f i c a t i o nl a n g u a g ei n t op v sa i m i n ga tc u r r e n tp o i n t - t o p o i n tt r a n s l a t i o n ，m o r e o v e r , a si n t e r m e d i a t ed o c u m e n t s t h eg e n e r a t e do m d o cf o m a tc a nb et r a n s f o r m e di n t oo t h e r l a n g u a g e ss oa st oi n t e r g r a t eo t h e rf o r m a lm e f i m d s f o rt h eh i g hc o n s i s t e n c yo fx m l t r e es t r u c t u r eo ft h em a t h e m a t i c a lt h e o r yo fo m d o c ，i tp r o v i d e sp o s s i b i l i t yf o rt h e t h e o r i e sm o d i f ya n dr e u s eo fs y s t e m sw h i c hc a ni n t e r a c tw i t h0 m d o c i nt h ee n d ， r e a l i z ea s i m p l et r a n s l a t o ra u t o m a t i c a l l yt r a n s f o r m i n gf d l i n t op v sc o r r e c t l y t h em a i ni n n o v a t i o n so f t h i st h e s i sj n c l u d e ： 1 a ts e m a n t i cl e v e l b a s e d0 nt h em e c h a n i s mo fo p e n m a ta n do m d o c ，p r e n t sa i n t e g r a t i o ns o l u t i o nu s e do m d o ca sam e d i a t el a n g u a g et ot r a n s l a t es p a r k f d li n t o p v ss oa st of u t h e rr e a l i z et h e s et w ov e r i f i c a t i o ns y s t e m s f o rt h ei n t e g r a t i o no fn s y s t e m t h i so m d o c b a s e dm e 血o dn e e d so n l y2 nt i m e st h a n s f o r m a t i o ni n s t e a do f n i n p o i n t t o p o i n tt r a n s l a t i o n ，w h i c hr e d u c e st h ec o m p l e x i t yo fi n t e g r a t i o n 2 s e l f s t u d ya n dd e f i n eap r i v a t ed i c t i o n a r yo f f e r i n gs e v e r a ls e l f - d e f i n e dm a r k u p s c h e m as oa st ot r a n s f o rt h es p a r kf d ls y n t a xi n t oo m d o cf o m a t s ，t h u sg e n e r a t e sa n o m d o cd o c u m e n ti n c l u d i n gs t a n d a r da n dp r i v a t ed i c t i o n a r i e s ，w h i c hi sc u s t o m i z e di n t o as p e c i a la n dp v s o r i e n to m d o cd o c u m e n t sv i aa l lu p d a t e di n t e r f a c e ，b a s e do nx s l t t or e a l i z es y n t a xt r a n f o m a t i o nu l t i m a t e l y 3 a i m i n ga td e c l a r a t i o n s ，r u l e sa n dv e r i f i c a t i o ni nf d l ，r e s p e c t i v e l yd e f i n e v a r i a b l e ，c o n s ta n dt y p ed e c l a r a t i o nr u l e st r a n s l a t i n ga l lf d l d e c l a r i o n si n t os y m b o la n d d e f i n i t i o ne l e m e n t sf r a g m e n t s ；r u l e st r a n s l a t i n ga l lm l ed e c l a r a t i o n si n t oa x i o me l e m e n t f r a g m e n t s ；a n dv e r i f i c a t i o nc o n d i t i o n s ，a n da l lv e r i f i c a t i o nc o n d i t i o n sa r et r a n s l a t e di n t o a s s e r t a t i o ne l e m e n tf r a g m e n t s k e yw o r d s ：f o m a lm e t h o d s ，i n t e g r a t i o n ，o m d o ca p p r o a c h ，s p a r kf d l p v s ，i n t e r l i n g u a 儿 学位论文版权使用授权书 本学位论文作者完全了解学校有关保留、使用学位论文的规定，同意学位保留并向国家 有关部门或机构送交论文的复印件和电子版。允许论文被查阅和借阅。本人授权江苏大学可 以将本学位论文的全部内容或部分内容编入有关数据库进行检索，可以采用影印、缩印或扫 描等复制手段保存和汇编本学位论文。 ， 本学位论文属于 保密口，在年解密后适用本授权书。 不保密 学位论文作者签名 构襁 工口d f 年占月f 日 指导教师签名 、 少s 年( ) 月莎日 0 磐 本人郑重声明：所呈交的学位论文，是本人在导师的指导下，独立进 行研究工作所取得的成果。除文中已注明引用的内容以外，本论文不 包含任何其他个人或集体已经发表或撰写过的作品成果。对本文的研 究做出重要贡献的个人和集体，均已在文中以明确方式标明。本人完 全意识到本声明的法律结果由本人承担。 学位论文作者签名： 物栖 日期：瑚。岁年二月譬日 江苏大学硕士学位论文 第一章绪论 我们目前处在的是一个科学同益发达、信息高速发展的世界。计算机系统阻 及计算机的应用逐渐地成为了人们日常生活、工作中的一个重要的组成部分，帮 助人们的衣食住行、提供新的社会交流方式甚至是产生直接的利润。计算机技术 的发展本来是为了让事务的处理方式变的简捷和更加方便，然而从某种程度上来 说并不是我们所想的这样。有的时候计算机系统工作异常、出现错误甚至会导致 最终的失败。而对于关键应用系统来说，旦它们不能正常的工作，可能会给我 们带来极大的不便，甚至造成严重的经济损失和意想不到的后果，面对于以任务 和安全为主要设计目标的系统来说，它们的工作异常将肯定会给生活、学习、工 作和研究带来更大的、无法预计的不良后果，甚至是生命和财产的惨重代价，这 些绝对不是危言耸听。 随着计算机系统的普及，系统的规模和复杂度也随之不断的增加，因此对于 系统正常运作的要求也越来越迫切。尤其是在以安全为主要设计目标的系统中， 因为大多数这样的系统都需要符合自身正常运作的标准。这些相关的标准主要是： 美国国防部的d o d s t d 2 1 6 7 a 标准，以及加拿大原子能控制委员会( a c e b ) 的 2 2 3 4 1 【2 1 标准。但是，仅仅通过传统的编码和测试软件周期方法并不能满足更高的 标准以及系统的需求，因为这些系统必须要得到尽可能严格和形式化的规定和验 证。 1 1 问题的提出 对于安全关键系统，普遍倡导、接受和使用的是形式化方法，同时在安全领 域，大量的标准也采用了形式化方法【2 1 。形式化方法主要是在数学符号和逻辑的基 础上，对系统进行严格的规定说明和检验。形式化方法通常包含一种形式化语言 和一个形式化推理系统【3 1 ，形式化语言是由严格的语法和语义进行定义，而形式化 推理系统则包括形式化语言相关的证明工具。 1 1 1 研究背景 多年来在学术研究和工业领域产生了大量基于形式化方法的语言、方法和工 具，这些语言、方法和工具在系统的设计和开发方面得到了广泛的应用。例如： s d l 语言( s p e c i f i c a t i o na n dd e s c r i p t i o nl a n g u a g e ) 一1 ，v d m ( v i n n ad e v e l o p m e n t 江苏大学硕士学位论文 m e t h o d ) 方法1 5j ，以及“z 注释”【6 ，它主要用于需求说明；s m v ( s y m b o l i cm o d e l v e r i f i e r ) 】和s p i n 8 1 则是用于有限状态系统的自动化验证工具：而p v s 系统1 9 1 ( p r o t o t y p ev e r i f i c a t i o ns y s t e m ) j j 是另一个推理验证系统；s p a r k d o l 是拥有多个基 于z 注释的分析工具。在安全和商业应用系统方面，已经有很多使用形式化的方 法来对系统正确性进行规定和验证的成功的案例。例如，l o c k h e e d 公司使用s p a r k 来对其c 1 3 0 航班上的软件代码进行分析；i b m 的c i c s ( 客户信息控制) 系统是 一个全球范围的在线事务处理系统，i b m 使用z 注释方法成功地对其进行了形式 化处理。 如上所述，形式化方法是系统说明和验证领域最有前途和最成功的方法。总 的来讲，形式化说明使用形式化语言来描述某一具体系统的属性。譬如前面提到 的s p a r k ，它可能是用于系统功能、行为说明的最成功的形式化语言。s p a r k 包 括一个形式化说明语言，即s p a r k 语言，s p a r k 语言是a d a t l i j 语言的一个子集， 它在现实世界中的应用标志了形式化说明方法的成功。 在系统验证领域，通过使用验证工具来分析对系统的描述是否符合并满足规 定，形式化方法已经不仅仅用于进行说明。在形式化方法领域，有两种著名的验 证方法应用：模型检验和定理证明。模型检验是用于验证系统特征的自动化验证 方法，它与传统的仿真和测试工具不同，模型检验方法在有限模型系统的基础上 构建，随后进行穷举验证。s m v 和s p i n 是建立在模型检验技术基础上的两种模 型检验工具。与模型检验方法相比，定理证明方法是另外一种验证技术，它能够 直接处理无限状态的问题。定理证明技术通常使用数学公式、原理和推理规则对 属性进行演绎和推理。s p a r k 就包括了一个基于定理证明技术的推理系统，该推 理系统有一整套的工具，包含了定理产生器和半自动验证工具，定理产生器能够 产生基于s p a r k 说明的定理，同时，s p a r k 中所包含的验证工具可以用来证明 定理的合理性以便于验证相关的规定和说明。然而，s p a r k 只能处理静态的、函 数功能级别的行为，它里面所用到的定理证明技术还相对原始，只能验证运行时 的、非行为的属性( 诸如性能和实时约束) 。p v s 系统是另一个广泛使用的验证系 统，它和s p a r k 相似，也包括了一种说明语言和半自动化验证工具，与s p a r k 只能处理静态分析和函数行为不同的是，p v s 既能处理连续代码，也能处理系统 的并发行为。 正如前面所提到的，每一种普遍采用的形式化方法都有着各自的优点和缺点， 在所给定的条件下，并非只有一种形式化方法是最佳解决方案，基于不同的目标， 江苏大学硕士学位论文 需要在不同的阶段使用不同的形式化方法。对于特定类型的系统来说，某些形式 化方法总要比使用其他方法更加合适。所以，在实际操作中，需要使用不同的形 式化方法和工具的联合，尤其是在对一个庞大而复杂的系统进行说明和验证的时 候。 1 1 2 研究现状及目标 近几年来，形式化方法的集成成为一个流行的课题【31 2 1 3 】，但对形式化方法 集成的研究和应用目前还处于初步的阶段。在形式化方法集成领域，不同形式化 说明语言中语义和语法层次的集成是一个基本的有前景的研究方向，已经出台了 许多的建议，其中些已经得到实施 1 4 15 川1 7 。然而，这些方法都是一些 点对点的翻译( 例如：一种说明语言区别与另一种语言的特征) ，集成的结果是函 数功能级别的，与特定的说明语言耦合紧密，这就带来了许多的不便：诸如互操 作、分布式以及模块化的问题。这种翻译方法缺乏开放的标准，或通用的接口， 工作量还相当巨大，同时过程相当复杂。针对上述的不足，我们提出了一神全新 的集成方法：基于o m d o c 作为中间语言，进行形式化方法的转换，这种集成的方 法能够有效的解决上述的点对点翻译中所遇到的互操作、分布式、模块化等问题， 并且还具有开放的标准、通用的接口，同时还能降低集成过程中的复杂度。这种 方法能够适用目前规模日益扩大、复杂度不断增加的系统。 包括说明语言和验证方法在内的所有形式化方法都是基于数学知识的，数学 是所有这些技术的基础。过去，进行数学计算都由手工完成，但是现在，基于w e b 的数学分析系统提供了支持数学计算的基础框架，人们已经提出了多种数学交换 格式，其中的一些已经拥有了一定的标准，例如m a t h m l ( 数学标记语言) f 2 。2 j 是第一个w 3 c e 2 2 1 组织推荐使用的用于在w e b 进行数学计算的x m l 语言23 1 ，另一 方面，另外一种x m l 应用o p e n m a l h l 2 4 ”j ，不再关注于表示层的数学计算， 它提出了一系列基于语义层次上的数学对象多信息文本的标准，o p e n _ m a t h 使用特 殊的称为o p e n m a t h 对象的x m l 注释和扩展机制，即内容字典( c o n t e n td i r e c t i o n ， c d ) 来对数学符号和表达式进行编码：另外，数学文档开放标记格式( o m d o c ) 2 6 作为o p e n m a t h 的扩展，从文档和理论层次更进一步地扩展了数学对象和内容，这 一点非常必要。因为o p e n m a t h 并没有为对象定义、定理和理论这样的概念提供足 够的标记模式。类似于o p e n m a t h ，o m d o c 文档可以看作是x m l 文档，它拥有一 种特殊的标记模式来表达基于数学理论及证明层次的丰富的数学对象和表达式。 作为x m l 应用，o p e n m a t h 、m a t h m l 和o m d o c 的一个基本目标是为数学计 江苏大学硕士学位论文 算软件系统提供一种交流语言1 2 “，为了达到这一目标，m a t h m l 从表示层上为数 学公式提供了一套标准的标记模式，m a t h m l 着眼于从语义层次为数学对象提供通 用的标记语言，另外，o m d o c 通过数学表达式和数学理论添加标记模式，提供了 一套被普遍接受的语言标准( 或中间语言) 来支持自动化推理系统和形式化说明 系统，从而使得在n 个系统互相转换中只使用2 n 种魏译方法而不是n 2 种【2 。为 达到该目标，o m d o c 甚至提供了x s l t 27 】格式的多个接口，这些接口可以用来将 0 m d o c 文档转换为其他格式嘶2 8 2 9 1 ，这些格式包括用于显示的h t m l 、d h t m l 和l a t e x ，还有一些软件系统特别是定理证明系统的说明语言，诸如1 n k a ，t p s 和p v s 等【2 6 】。作为新兴的方法，0 p e n m a t h 和o m d o c 还处在发展阶段。对我们来 说，不需要在评估这些格式化语言将会对现实世界的描述和验证中发挥多大的作 用方面花费过多的精力，本文的一个目标是研究这些领先的形式化语言交换格式 ( o p e n m a t h 和它的扩展0 m d o c ) 的有效性。 前面介绍过，在形式化说明领域，s p a r k 系统在工业上得到了广泛的应用， 用来设计、开发和验证复杂的安全系统以确保工业规则的需求。s p a r k 语言为系 统功能行为的说明提供了严格而明确的语义，s p a r k 的相关工具不仅作为标准编 译器来主导静态语义分析和运行时的错误检测，更重要的是，它们还能完成程序 验证分析。验证分析可以分为两步进行，第一步：s p a r k 工具从s p a r k 代码中 生成各种类型的声明、规则和相关的定理，这些声明、规则和定理均由一种形式 来进行表达，即f d l ( f u n c t i o n a ld e s c r i p t i o nl a n g u a g e ) 建模语言 3 0 1 ：第二步：s p a r k 中的验证工具进一步通过证明来验证是否遵守在s p a r k 代码中所声明的特定的属 性，然而，正如前面所提到的，s p a r k 所提供的验证技术还相对简单和原始，所 以它只支持顺序s p a r k 程序属性的分析和验证，而且f d l 验证语言基于一阶逻 辑而不是更丰富的高阶逻辑【3 2 33 1 。另一方面，f d l 只能支持简单的命题逻辑和 谓词逻辑，例如关系、量词，而不能支持高阶逻辑的特征，例如函数能将函数视 为变量，量词可以作为函数变量等，因此，即便是对函数进行验证，s p a r k 也有 它的局限所在。 最近，添加了一个扩展，即s p a r kr a v e n s c a r 概要1 3 4 ，用于处理确定性的并 发实时问题，但是这种扩展仍然不能满足非确定性行为的程序，例如时限【3 5 j 问题 以及其他一些并发问题口6 】( 例如受保护对象、抢先和资源使用) 。其他的验证方法， 例如定理证明或模型检验技术都需要进一步对那些非行为化属性进行推证。前面 所提到的p v s 系统，它作为一个得到最广泛应用的验证系统，可能和s p a r k 系 4 江苏大学硕士学位论文 统进行集成来处理对非行为化特征的验证，而且，p v s 是基于高阶逻辑的，它包 含了比一阶逻辑更为丰富的逻辑，甚至是在对函数行为的验证上，p v s 都比s p a r k 更为强大。所以，本文的另一个目标是使用o m d o c 方法，在语义层次上，实现 s p a r k 和p v s 系统的集成。 1 1 3 解决方案 首先，本文将提出一个利用o m d o c 将s p a r kf d l 语言译为p v s 语言的一个 解决方案，基于o p e n m a t h 和o m d o c 方法，我们将实现一个翻译器，能够对s p a r k f d l 语法进行自动解析，并生成相应的o m d o c 文档作为输出；同时，所生成的 o m d o c 文档能够自动地转换为有效的p v s 语法：更重要的是，这一o m d o c 文档 作为一个中间格式，可以看作是通用的交互语言，它能够被翻译为其他的形式化 说明验证语言。 本文所给出的翻译方法证明，能够使用o m d o c 方法实现对s p a r k 和p v s 两 种验证系统的集成，另外，作为翻译的中间结果，o m d o c 文档提供了开放的标准 格式来代表它所要求的数学概念和知识。总的来说，通过本文第三、四章的研究， 我们可以得出结论：在理论上，基于语义和语法层次，不同形式化语言之间的互 译也能通过o m d o c 方法实现，于是，在理想情况下，可以实现不同定理证明系统 之间的互操作。 通过本文的研究，我们也能发现了o m d o c 方法所存在的缺点。虽然f d l 和 p v s 都是说明和验证语言，它们也包含了许多和其他程序设计语言相类似的数据 类型，诸如枚举类型、数组类型和记录等等。然而o p e n m a t h 以及它的扩展o m d o c 虽然是说明和验证语言，但主要用于处理数学对象、符号及表达式。因此，从根 本讲，o p e n m a t h 和o m d o c 并没有一个显式的方法来表示这些数据类型，而这些 数据类型却是s p a r kf d l 和p v s 以及其他说明和验证语言的基础。所以，我们 基于o p e n m a t h 和o m d o c 机制，作了一些定义以支持这些数据类型。 1 2 研究内容 本文使用数学交换格式0 p e n m a i h 和o m d o c 将s p a r kf d l 验证语言译 为p v s 语言，从而实现前面所提到的两个研究目标： 1 形式化语言交换格式( o v e n m a h 和它的扩展o m d o c ) 的有效性研究。 2 使用o m d o c 方法，在语义层次上，实现s p a r k 和p v s 系统的集成。 由于第二个研究目标十分复杂，所以我们将第二个研究目标中的主要内容归 江苏大学硕士学位论文 统进行集成来处理对非行为化特征的验证，而且，p v s 是基于高阶逻辑的，它包 含了比一阶逻辑更为丰富的逻辑，甚至是在对函数行为的验证上，p v s 都比s p a r k 更为强大。所以，本文的爿一个目标是使用o m d o c 方法，在语义层次上，实现 s p a r k 和p v s 系统的集成。 11 3 解决方案 首先，本文将提出一个利用o m d o c 将s p a r kf d l 语言译为p v s 语言的一个 解决方案，基于o p e n m a t h 和o m d o c 方法，我们将实现一个翻译器，能够对s p a r k f d l 语法进行自动解析，并生成相应的o m d o c 文档作为输出；同时，所生成的 o m d o c 文档能够自动地转换为有效的p v s 语法；更重要的是，这一o m d o c 文档 作为一个中间格式，可以看作是通用的交互语言，它能够被翻译为其他的形式化 说明验证语言。 本文所给出的翻译方法证明，能够使用o m d o c 方法实现对s p a r k 和p v s 两 种验证系统的集成，另外，作为翻译的甲问结果，o m d o c 文档提供了开放的标准 格式来代表它所要求的数学概念和知识。总的来说，通过本文第三、四章的研究， 我们可以得出结论；在理论上，基于语义和语法层次，不同形式化语言之间的互 译也能通过o m d o e 方法实现，于是，在理想情况下，可以实现不同定理证明系统 之间的互操作。 通过本文的研究，我们也能发现了o m d o c 方法所存在的缺点。虽然f d l 和 p v s 都是说明和验证语言，它们也包含丁许多和其他程序设计语言相类似的数据 类型，诸如枚举类型、数组类型和记录等等。然而o p e n m a t h 以及它的扩展o m d o c 虽然是蜕明和验证语言，但主要用于处理数学对象、符号及表达式，因此，从根 本讲，o p e n m a t h 和o m d o c 并没有一个显式的方法来表示这些数据类型，而这些 数据类型却是s p a r kf d l 和p v s 以及其他说明和验证语言的基础。所咀，我们 基于o p e n m a t h 和o m d o c 机制，作了一些定义以支持这些数据类型。 1 2 研究内容 本文使用数学交换格式- o p e n m a t h 和o m d o c 将s p a r kf d l 验证语言译 为p v s 语言，从而实现前面所提到的两个研究目标： 1 形式化语言交换格式( o p e n m a t h 和它的扩展o m d o c ) 的有效性研究。 2 使用o m d o c 方法，在语义层次上，实现s p a r k 和p v s 系统的集成。 由于第二个研究目标十分复杂，所阻我们将第二个研究目标中的主要内容归 出于第二个研究目标十分复杂，所以我们将第二个研究目标中的主要内容归 江苏大学硕士学位论文 纳如下： 基于o p e n m a t h 和o m d o c 机制，在翻译器中定义多个自定义标记模式。 从s p a r kf d l 中生成o m d o c 文档作为中间语言。 提供一个接口的更新版本以便将其正确转换为p v s 语法。 3 根据以上研究内容，最终设计并实现一个简单的翻译器，进行f d l 与p v s 的单步和自动转换，展示一些可以运行的转换过程。 1 3 本文的组织结构 本文的组织结构如下： 第一章对课题的研究背景及意义进行了简短的论述，并且提出了本文的研究 内容。 第二章将简单的介绍本文中的相关技术，主要是本文中所用到的几种形式化 语言。源语言s p a r k 及s p a r kf d l ；接下来介绍中间o p e n m a t h 方法以及其扩展 o m d o c ；最后是目标语言p v s 。 第三章是本文的重点以及难点，包含了本文的大部分研究内容。首先概述使 用0 m d o c 方法进行翻译的方法，讨论了o m d o c 方法好处并简要介绍了翻译的步 骤，接下来详细论证了如何转换及制定的相应规则，并且阐述了进行翻译的难点 及解决方法，以及在案例研究和相应的解决方案中所碰到的一些问题。 第四章是在第三章的理论研究的基础上实现基于o p e n m a t h 和o m d o c s p a r kf d l 与p v s 之间的转换，并详细介绍了其转换的流程，通过实验性的翻译 器实现具体的仿真。 第五章是本文最后一章，对前面所讨论的文档转换方法作出结论，指出未来 的研究方向和所需要做的下一步工作。 江苏大学硕士学位论文 第二章相关技术及研究现状 本章将对本文所涉及到的三种形式化语言作出相应的介绍，分别阐述这三种 形式化语言的属性与规范。 2 1源语言 21 1s p a r k 语言 s p a r k 是一种被设计用于编写安全关键系统软件的高级编程语言，它构成了 a d a 语言的核心。s p a r k 包含了一些附加的注解，用相关的工具来执行程序分析、 运行时的错误检测以及程序正确性的检验。这些相关工具包括了：s p a r k e x a m i n e r ，s i m l i f i e r 和证明检验程序f p r o o f c h e c k e r ) 1 3 m 。 s p a r k 的理论基础是：作为类属的编程语言，a d a 语言由于它的定义并不明 确且过分复杂，因此不适合用来设计严格而精确的系统。对于安全关键系统的开 发，需要a d a 的一个“安全子集”来保证系统的正确性，s p a r k 利用a d a 的一些 优点来消除系统设计中潜在的多义性和不安全性；s p a r k 的附加注解以a d a 注释 的形式出现( 这些注释通常都会被a d a 编译器所忽略) ，它们包含了一些和说明与 需求分析相关的附加信息。利用s p a r k2 1 2 具s p a r j 江re x a m i n e r 来处理这些 注解以及a d a 子集的s p a r k 核心部分。s p a r k e re x a m i n e r 首先扮演编译器的角 色柬完成每个编译单元的静态分析，静态分析可能包括词法和语法分析、语义 校验以及数据流和信息流的分析；更重要的是，s p a r k e re x a m i n e r 可以产生基于 s p a r k 代码和注解的定理。一旦定理得到证明，s p a r k 程序就表现为：已获得特 定的属性，并且其编码符合对程序的说明和规定。 在s p a r k 中可以将一个定理引用为验证条件( v e r i f i c a t i o nc o n d i t i o n ，缩写为 v c ) 。除了定理和v c ，s p a r k e re x a m i n e r 还产生相应的证明声明及辅助规则来 证明定理。所有这些，包括证明声明、规则和验证条件被称为证明合同，而证明 合同就以f d l ( 功能描述语言) 语言3 0 1 的形式进行表达。 s p a r k 注解有以下几种形式： 全局定义：声明过程、函数子程序中的全局变量。 依赖关系：说明导入和导出变量之间的信息流。 证明上下文：包含子程序的预处理条件和后续条件，以及断言语句。 7 江苏大学硕士学位论文 前两种注解是用于静态和语义分析的强制性说明；证明上下文是非强制性的 注解，e x a m i n e r 可以使用它柬生成定理。这罩的预处理条件和后续条件是用来约 束子程序变量的谓词。在这里我们需要指出：对于s p a r k 语言的全部描述不在本 文的研究范围之内，可以参考“s p a r k9 5u s e r m a n u a l ”1 3 7 1 和j o h n b a r n e 的著作“h i g h i n t e g r i t ya d a t h es p a r ka p p r o a c h 【3 0 。 21 2s p a r kf d l 语言 2 1 2 1e x a m i n e r 输出 前面提到，s p a r ke x a m i n e r 以称作f d l 建模语言的形式来生成证明合同。对 每一个s p a r k 子程序，这一形式生成的证明合同实际上保存在下面讲到的三个分 离的输出文件中，如表2 1 所示： 表2 1 e x a m i n e r 的输出文件 文件 扩展名 f d ld e c l a m t i o n sf d i r u l e sr l s a n a l y s i s ( 定理或验证条件)v c g e x a m i n e r 拥有一套命名机制来保证f d l 输出文件和子程序的名字保持一致。 例如，对于s w a p e l e m e n t 子程序，相应的输出文件就是s w a p e l e m e n t f d l ， s w a p e l e m e n t r l s 和s w a p e l e m e n t v c g ，也就是上面文件内容的第一至第三部分。 图2 1 显示出整个证明过程以及s p a r k 工具之间的关系： 2 1 。2 2形式化语言f d l 与s p a r k 不同，f d l 是一种说明和建模语言，而不是编程语言。f d l 使用一 阶逻辑【3 l 建模并对属性行为进行描述，换句话说，作为一阶逻辑，f d l 不仅能够 表达布尔表达式，比如“真”、“假”、“与”、“或”、“异或”等，还能处理另外两 种重要的逻辑操作符：全称量词和存在量词。在f d l 中，这两种量词由保留字和 “f o rs o m e ”来标识。前面的第三部分文件内容中，实际上就有“f o ra l l ”表达式。 另外需要强调的是，作为一种说明和建模语言，f d l 关注的是基于数理方面 的声明( 包括数据类型声明、函数声明等) 、规则和验证条件表达式。本文下一部 分将详细论述这一方面的内容。 江苏大学硕士学位论文 图2 1 证明过程以及s p a r kt 具之间的关系 2 1 2 3f d l 保留字、数值常字和标识符 作为一种说明和建模语言，f d l 包含了一系列保留关键字。f d l 中所有来自 s p a r k 的数值常字都将转换为十进制。 f d l 中所有由s p a r k 映射而来的标识符均变为小写，并且将任何前缀中的句 号替换为双下划线以避免冲突。 2 1 2 4f d l 声明 由s p a r k e x a m i n e r 生成的证明声明保存在f d l 文件中。f d l 声明由类型声明、 常量声明、变量声明和函数声明所组成。 9 江苏大学硕士学位论文 类型声明 f d l 有两种类型的数据：简单类型和结构类型。简单类型的值没有组件，构 成一个有序集合；结构类型是一种组合类型，由它的组件和结构方法所描述，结 构类型包括数组类型和记录类型。 f d l 类型声明与类型标识符相联系：标识符标注类型。类型声明也可能定义 一个具体的类型；类型定义可能是未确定的，用“p e n d i n g ”关键字标注，意味着 该类型是抽象类型。简单类型和结构类型都可以既是具体类型也可以是抽象类型。 曲整型：标识符“i n t e g e r ”标注整数类型，s p a r k 中的所有整数正数或 负数都可以映射为f d l 整数类型。 b ) 实数类型：标识符“r e a l ”标注实数类型，与整数类型相似，s p a r k 中的 所有实数定点或浮点类型都可以转化为f d l 实数类型。 c ) 布尔类型：标识符“b o o l e a n ”标注布尔类型，其值为“真”或“假”。 d ) 枚举类型：枚举类型通过对标识符的穷举定义了一个有序值的集合，值的 顺序由列举的标识符的排列顺序决定，例如，如果x 在y 的前面，则x 小于y 。与整型不同，f d l 枚举类型只是其等价s p a r k 枚举类型的简单 替换。 e ) 数组类型：数组类型是结构类型，它由固定数量的元素组成。数组的一个 元素由一个或多个属于已声明的枚举或子类型所指定。 f 1记录类型：记录类型也是由固定数量的元素所组成的结构类型，记录类型 说明了每一个字段、标识符和类型。需要指出的是，f d l 使用分号作为分 隔符，但如果记录的一个字段没有紧跟一个分号，则浣明该字段是记录类 型定义的最后个字段。 常量声明 标识符“c o n s t ”标注常量类型，由e x a m i n e r 所产生的常量总是被声明为 “p e n d i n g ”。 常量的实际值由适当的、自动生成的证明规则所产生，这些规则保存在f d l 的规则文件中，f d l 规则文件将在文章的后面讨论。 变量声明 标识符“v a r ”标注变量。变量声明由一系列标识符来标注，后面紧跟变量的 类型。 1 0 江苏大学硕士学位论文 函数声明 标识符“f u n c t i o n ”标注函数声明，f d l 中的函数是纯粹的数学函数，与s p a r k 中不同的是，f d l 中没有过程声明。 2 1 2 5f d l 表达式 f d l 表达式由操作数、操作符、函数指定符、量词、集合、顺序结构和属性 组成。 操作符 a ) 算术操作符： 乘法操作符：= + l 】d i v i r o o d + + ( 求幂) 加法操作符：= + i 一 关系操作符：= = i l i = 一目减算符：= 一 b ) 布尔操作符：如表2 2 所示。 表2 2f d l 布尔操作符 操作符操作