Application Study On OMDoc For Mathematical Documents

Different formal methods have been advocated in academic research and now even applied in many industrial projects from different aspects. As computer systems become more complex integration among different formal methods is necessary and can be helpful in providing a correct and rigorous system. All formal methods are based on mathematical symbols and knowledge. OMDoc(Open Mathematical Documents), as an XML application,presents a content markup scheme for mathematical notations and concepts.OMDoc provides a possible infrastructure to serve as a content language for communication of different systems based on formal methods.In this thesis, we first study systematically the effectiveness of the exchange format of formal language (Openmath and its extension OMDoc),based on which a brand new integration method is presented:Using OMDoc as the interlingua to translate SPARK verification language into PVS aiming at current point-to-point translation. Moreover, as intermediate documents, the generated OMDoc fomat can be transformed into other languages so as to intergrate other formal methods. For the high consistency of XML tree structure of the mathematical theory of OMDoc, it provides possibility for the theories modify and reuse of systems which can interact with OMDoc. In the end, realize a simple translator automatically transforming FDL into PVS correctly.The main innovations of this thesis include:1. At semantic level, based on the mechanism of OpenMat and OMDoc, prents a integration solution used OMDoc as a mediate language to translate SPARK FDL into PVS so as to futher realize these two verification systems. For the integration of N system, this OMDoc-based method needs only 2N times thansformation instead of N2 in point-to-point translation, which reduces the complexity of integration.2. Selfstudy and define a private dictionary offering several self-defined markup schema so as to transfer the SPARK FDL syntax into OMDoc fomats, thus generates an OMDoc document including standard and private dictionaries, which is customized into a special and PVS-orient OMDoc documents via an updated interface, based on XSLT to realize syntax tranfomation ultimately.3. Aiming at declarations, rules and verification in FDL, respectively define variable, const and type declaration rules translating all FDL declarions into symbol and definition elements fragments; rules translating all rule declarations into axiom element fragments; and verification conditions, and all verification conditions are translated into assertation element fragments.