Object-Z證明責(zé)任產(chǎn)生器的設(shè)計(jì)和實(shí)現(xiàn).pdf

1、近年來，為了保證各種軟件的正確性和提高軟件的可維護(hù)性、可重用性，人們對(duì)軟件形式方法的研究越來越廣泛和深入，形式方法的研究之所以能夠迅速，除了因?yàn)槠浔旧砉逃械膬?yōu)點(diǎn)，如精確、可以進(jìn)行推理驗(yàn)證等，對(duì)形式方法的支持工具越來越多也是一個(gè)重要的原因。 本課題研究的是形式規(guī)格說明語(yǔ)言O(shè)bject-Z的支持工具的集成的一部分——一個(gè)證明責(zé)任產(chǎn)生器。證明責(zé)任產(chǎn)生器的工作就是對(duì)規(guī)格說明進(jìn)行動(dòng)態(tài)檢查，完成靜態(tài)語(yǔ)法分析不能完成的工作，從而使規(guī)格說明的驗(yàn)

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

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