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

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

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

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