OMDoc在數(shù)學文檔中的應用研究.pdf

1、不同的形式化方法不僅在學術(shù)研究中得到支持與倡導，而且目前已經(jīng)廣泛應用到實際工業(yè)項目的各個方面。由于計算機系統(tǒng)越來越復雜，可能在一個系統(tǒng)中需要用到多種形式化方法，因此十分有必要將不同的形式化方法進行集成，這對于建立正確而嚴密的系統(tǒng)很有幫助。所有的形式化方法都是基于數(shù)學符號和知識之上，OMDoc(開放數(shù)學文檔)作為一種XML應用，提出了一種針對數(shù)學注釋與概念的內(nèi)容標記模式，為建立一種作為基于不同形式化方法的系統(tǒng)之間的交互的內(nèi)容語言提供了可能

2、的基礎。 本文首先對形式化語言交換格式(OpenMath和它的擴展OMDoc)的有效性進行了系統(tǒng)的研究，并在此基礎上針對目前點對點翻譯的不足，提出了一種新的基于中間格式的集成方法，即以OMDoc作為中間語言，將SPARK驗證語言FDL翻譯為PVS，從而自動地實現(xiàn)了兩個著名的驗證系統(tǒng)-SPARK和PVS之間的集成。并且作為中間文檔，產(chǎn)生的OMDoc格式能夠轉(zhuǎn)換為其它的形式化語言從而將其它形式化方法進行集成。由于OMDoc格式的數(shù)學

3、理論具有一致的XML樹型結(jié)構(gòu)，對于各種可以與OMDoc文檔進行交互的系統(tǒng)而言，為其理論的修改和重用提供了可能。最后設計并實現(xiàn)了一個簡單的翻譯器進行仿真實驗，正確地實現(xiàn)了FDL與PVS之間的單步和自動轉(zhuǎn)換。 論文的主要創(chuàng)新點：1.在語義層上，基于OpenMath和OMDoc機制，提出一種以OMDoc為中間語言，進行SPARK-FDL和PVS語言之間的轉(zhuǎn)換，從而進一步實現(xiàn)兩種驗證系統(tǒng)的集成方案。對于N個系統(tǒng)之間的集成而言，傳統(tǒng)的點對

4、點轉(zhuǎn)換需要進行N2次轉(zhuǎn)換，而這種基于OMDoc的轉(zhuǎn)換方法則只需要2N次，降低了翻譯過程中復雜度。 2.為了保證集成的完整性和有效性，自主研究并定義了私有字典，提供多個自定義標記模式，實現(xiàn)SPARK-FDL語法與OMDoc格式的轉(zhuǎn)換，從而生成包含標準字典和私有字典的OMDoc文檔，并通過一個經(jīng)過修改的接口，將該文檔定制為特定的、面向PVS的OMDoc文檔，最后基于XSLT樣式表來實現(xiàn)與PVS的語法轉(zhuǎn)換。 3.針對FDL中的