面向?qū)ο筌浖男问津?yàn)證技術(shù).pdf

1、上海大學(xué)博士學(xué)位論文面向?qū)ο筌浖男问津?yàn)證技術(shù)姓名：文志誠申請學(xué)位級別：博士專業(yè)：控制理論與控制工程指導(dǎo)教師：繆淮扣20070501上海大學(xué)博士學(xué)位論文作。本文提出了一種關(guān)于多態(tài)性的推理方法，并實(shí)現(xiàn)推理的重用。一個形式規(guī)格說明是有用的，那它應(yīng)該是一致的或非沖突的，本文研究了對形式規(guī)格說明的性質(zhì)驗(yàn)證的方法，討論了如何抽取滿足相關(guān)性質(zhì)的待證定理，即產(chǎn)生驗(yàn)證形式規(guī)格說明是否一致的，是否具有所需性質(zhì)的證明責(zé)任(ProofObligation)。

2、如果一個證明責(zé)任能夠被證明，則說明此證明責(zé)任所相關(guān)的規(guī)格說明部分是一致的。設(shè)計(jì)和開發(fā)驗(yàn)證工具對于提高驗(yàn)證效率，改善軟件開發(fā)過程，保證軟件質(zhì)量具有重要意義，本文設(shè)計(jì)了一個ObjectZ規(guī)格說明的證明責(zé)任產(chǎn)生器，可以產(chǎn)生相關(guān)的證明責(zé)任，這些證明責(zé)任可以輸入到定理證明器Z／EVES中去證明之：先以O(shè)bjectZ規(guī)格說明文件作為證明責(zé)任產(chǎn)生器的輸入，接著按Z／EVES定理格式抽取證明責(zé)任，再把它作為Z／EVES定理證明器的輸入文件。其中，所有的