斷言語言支持自定義謂詞的程序驗證器原型.pdf

1、隨著經(jīng)濟社會的發(fā)展，各行各業(yè)對軟件的需求和依賴程度在逐漸增強，與此同時，軟件安全問題日益突出，特別是在一些安全攸關(guān)的領(lǐng)域中，軟件的可靠性變得十分必要。提高軟件可信程度的方法有很多種，如加強軟件開發(fā)的管理和流程控制，提高軟件開發(fā)人員的素質(zhì)水平等等；在眾多方法中，最嚴(yán)格的、最能提高軟件可信度的方法是形式化程序驗證，也即利用數(shù)學(xué)方法來對程序的源碼進行嚴(yán)格的推理演算和證明。
　　 在形式化程序驗證方法中，典型的形式化程序驗證器需要程序員

2、根據(jù)斷言語言書寫函數(shù)前后斷言（如果程序中有循環(huán)結(jié)構(gòu)，還需要循環(huán)不變式），而準(zhǔn)確地寫出這些斷言并不容易；不僅如此，考察現(xiàn)有的程序驗證工具，斷言語言的表達能力都一般都比較弱，這就使得很多性質(zhì)或是無法利用斷言語言表達出來，或是描述性質(zhì)的斷言十分復(fù)雜，而復(fù)雜的斷言會給定理證明器增加負(fù)擔(dān)，諸如此類的原因?qū)е鲁绦蝌炞C難以被廣泛應(yīng)用。
　　 為了解決這些問題，我們設(shè)計了形狀圖邏輯，該邏輯可以對利用我們定義的PointerC語言編寫的程序進行程

3、序分析，分析得到的結(jié)果為后面驗證條件生成和證明提供輔助；針對斷言語言表達能力不足的缺陷，本文采用在斷言語言中增加自定義謂詞、自定義函數(shù)、性質(zhì)定理等的方法來增強斷言語言的表達能力。
　　 本文的貢獻主要是：
　　 1．設(shè)計了通過在斷言語言中允許自定義謂詞、性質(zhì)定理和自定義函數(shù)的方法來增強斷言語言的表達能力。程序員可以通過自定義謂詞方便地定義出基于歸納性質(zhì)的斷言，同時基于謂詞描述程序性質(zhì)的方法減少了自動定理證明器證明失敗的情