Object-Z證明責任產生器的設計和實現(xiàn).pdf

1、近年來，為了保證各種軟件的正確性和提高軟件的可維護性、可重用性，人們對軟件形式方法的研究越來越廣泛和深入，形式方法的研究之所以能夠迅速，除了因為其本身固有的優(yōu)點，如精確、可以進行推理驗證等，對形式方法的支持工具越來越多也是一個重要的原因。 本課題研究的是形式規(guī)格說明語言Object-Z的支持工具的集成的一部分——一個證明責任產生器。證明責任產生器的工作就是對規(guī)格說明進行動態(tài)檢查，完成靜態(tài)語法分析不能完成的工作，從而使規(guī)格說明的驗

2、證工作更加完善。而整個支持工具集成系統(tǒng)的完成，可以大大推廣Object-Z，使其得到更廣泛的應用，充分發(fā)揮它的優(yōu)點。 本文從Obiect-Z的基本結構出發(fā)，提出了對規(guī)格說明產生證明責任的策略，從初始狀態(tài)、前置條件、不變式、定義域檢查這四個角度出發(fā)，驗證規(guī)格說明初始狀態(tài)的存在性、操作是否滿足前置條件、操作結果是否滿足不變式以及某些運算的操作數(shù)是否處于定義域中，從而實現(xiàn)對規(guī)格說明一致性的驗證。同時，實現(xiàn)的工具提供了一個圖形用戶接口，

3、用戶可以通過該接口來輸入自己想證明的性質，更進一步實施對規(guī)格說明一致性的驗證。 本課題研究開發(fā)的證明責任產生器，以LATEX風格的Object-Z規(guī)格說明為輸入，經過轉換后產生證明責任，最終保存在”.tex”文件中，從定理證明器Z/EVES中導入即可證明。 由于采用了純Java技術、Unicode碼和字符流的輸入輸出方式，因此本軟件是一個跨平臺、跨語種的編輯器。只要通過Internet下載本軟件，只要用戶機器上有相應的J