OMDoc在数学文档中的应用研究

摘要

不同的形式化方法不仅在学术研究中得到支持与倡导，而且目前已经广泛应用到实际工业项目的各个方面。由于计算机系统越来越复杂，可能在一个系统中需要用到多种形式化方法，因此十分有必要将不同的形式化方法进行集成，这对于建立正确而严密的系统很有帮助。所有的形式化方法都是基于数学符号和知识之上，OMDoc(开放数学文档)作为一种XML应用，提出了一种针对数学注释与概念的内容标记模式，为建立一种作为基于不同形式化方法的系统之间的交互的内容语言提供了可能的基础。 本文首先对形式化语言交换格式(OpenMath和它的扩展OMDoc)的有效性进行了系统的研究，并在此基础上针对目前点对点翻译的不足，提出了一种新的基于中间格式的集成方法，即以OMDoc作为中间语言，将SPARK验证语言FDL翻译为PVS，从而自动地实现了两个著名的验证系统-SPARK和PVS之间的集成。并且作为中间文档，产生的OMDoc格式能够转换为其它的形式化语言从而将其它形式化方法进行集成。由于OMDoc格式的数学理论具有一致的XML树型结构，对于各种可以与OMDoc文档进行交互的系统而言，为其理论的修改和重用提供了可能。最后设计并实现了一个简单的翻译器进行仿真实验，正确地实现了FDL与PVS之间的单步和自动转换。 论文的主要创新点：1.在语义层上，基于OpenMath和OMDoc机制，提出一种以OMDoc为中间语言，进行SPARK-FDL和PVS语言之间的转换，从而进一步实现两种验证系统的集成方案。对于N个系统之间的集成而言，传统的点对点转换需要进行N2次转换，而这种基于OMDoc的转换方法则只需要2N次，降低了翻译过程中复杂度。 2.为了保证集成的完整性和有效性，自主研究并定义了私有字典，提供多个自定义标记模式，实现SPARK-FDL语法与OMDoc格式的转换，从而生成包含标准字典和私有字典的OMDoc文档，并通过一个经过修改的接口，将该文档定制为特定的、面向PVS的OMDoc文档，最后基于XSLT样式表来实现与PVS的语法转换。 3.针对FDL中的声明、规则以及验证条件，分别定义常量、变量、类型声明转换规则将所有的FDL声明都转换为symbol和definition元素片段；定义规则声明转换，将所有规则都变为axiom元素片段；验证条件表达式转换规则，将所有的验证条件转为assertion元素片段。