基于項重寫技術(shù)的規(guī)格和模型檢測研究.pdf

1、數(shù)學(xué)和邏輯中把一個公式中的某個子項替換成另一個子項的操作過程就是項重寫。項重寫系統(tǒng)的理論是計算的基礎(chǔ)理論。本文屬于項重寫技術(shù)在形式化方法領(lǐng)域的應(yīng)用研究。主要貢獻在于:成功地把項重寫的基本思想應(yīng)用在通用語言模型檢測當(dāng)中,給出基于通用語言源文件模型檢測的思想框架和具體方案,并最終用實驗表明這個方案的可行性。這項工作建立在對項重寫系統(tǒng)概念背景和發(fā)展歷史的考察基礎(chǔ)上,借鑒了現(xiàn)代主流形式化工具的設(shè)計思想,并充分利用現(xiàn)代通用編程語言的高級特性,使得

2、形式化建模更加容易。論文的全部工作包括:
　　項重寫技術(shù)用于系統(tǒng)規(guī)格和模型檢測的實踐現(xiàn)代軟件技術(shù)的發(fā)展已經(jīng)把項重寫系統(tǒng)的理論用于軟件實踐,一些功能比較完備的基于重寫技術(shù)的程序設(shè)計語言和工具已經(jīng)被開發(fā)出來。使用這樣的一種工具Maude在系統(tǒng)規(guī)格和模型檢測方面做了一些實踐:嘗試用Maude表達Petri網(wǎng)模型,分析了軟件形式化中Maude代替Petri網(wǎng)的可能性;使用Maude的search命令和LTL工具進行模型檢測實踐,并把模型檢

3、測方法用于求解智力游戲問題;參考別人代碼基礎(chǔ)上,完成了對簡單微處理器建立Maude模型的實踐。實踐表明,基于重寫技術(shù)的軟件工具可以在一定程序上被當(dāng)做通用編程語言使用,而不是僅僅作為軟件形式化方法和軟件測試中的專門技術(shù)。
　　通用語言實現(xiàn)模型檢測命令式語言和基于重寫技術(shù)的語言(函數(shù)式語言)在其發(fā)展過程中都在向?qū)Ψ綄W(xué)習(xí)借鑒,取長補短。當(dāng)今流行的一些命令式編程語言(如 Python)也有函數(shù)式編程的語法風(fēng)格。嘗試使用通用語言直接對源文件