OMDoc在數(shù)學(xué)文檔中的應(yīng)用研究.pdf

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

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

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

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