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

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

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

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

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