C程序證明策略在Coq中的設(shè)計(jì)和實(shí)現(xiàn).pdf

1、計(jì)算機(jī)系統(tǒng)已在國(guó)防、通訊、金融、能源、交通、醫(yī)療等關(guān)鍵領(lǐng)域中得到廣泛應(yīng)用，構(gòu)建高可信系統(tǒng)已成為世界范圍的重要課題。其中操作系統(tǒng)內(nèi)核的安全可靠性是構(gòu)建高可信計(jì)算機(jī)系統(tǒng)的關(guān)鍵，任何一個(gè)微小的內(nèi)核錯(cuò)誤都有可能導(dǎo)致整個(gè)計(jì)算機(jī)系統(tǒng)崩潰。形式化程序驗(yàn)證是使用邏輯推理系統(tǒng)來(lái)保證計(jì)算機(jī)程序的正確性，對(duì)于規(guī)模相對(duì)較小而設(shè)計(jì)復(fù)雜的內(nèi)核程序而言，它是保證其安全可靠的有效方法之一。底層的系統(tǒng)軟件大都采用C語(yǔ)言編寫(xiě)，而C程序中的指針操作和系統(tǒng)軟件中數(shù)據(jù)結(jié)構(gòu)間復(fù)雜

2、的邏輯關(guān)系，使得驗(yàn)證系統(tǒng)軟件的程序邏輯的斷言語(yǔ)言需要具有足夠的表達(dá)能力。然而，具有足夠表達(dá)力的斷言語(yǔ)言推理的不可判定性導(dǎo)致推理驗(yàn)證的過(guò)程無(wú)法完全自動(dòng)化，而手動(dòng)驗(yàn)證系統(tǒng)軟件需要耗費(fèi)大量的人力和物力。因此，如何在不犧牲邏輯斷言的表達(dá)力的前提下，盡可能的提高C程序的驗(yàn)證效率是一個(gè)亟待解決的問(wèn)題。
　　本文通過(guò)開(kāi)發(fā)證明策略來(lái)提高C程序在定理證明工具Coq中的驗(yàn)證效率。由于人工交互的手動(dòng)證明在驗(yàn)證復(fù)雜系統(tǒng)軟件中不可避免，因此在提供自動(dòng)化支持

3、的過(guò)程中同時(shí)需要兼顧以下兩個(gè)方面:一方面，需要盡可能的減少手動(dòng)證明的工作量;另一方面，當(dāng)證明策略失敗時(shí)，能夠產(chǎn)生對(duì)用戶(hù)有用的出錯(cuò)提示信息，這樣用戶(hù)可以根據(jù)提示信息快速地定位問(wèn)題所在，或者手動(dòng)證明那些無(wú)法自動(dòng)證明的命題，或者通過(guò)調(diào)整規(guī)范或代碼來(lái)完成證明?；谏鲜隹紤]，本文開(kāi)發(fā)了一組C程序的實(shí)用證明策略，包括自動(dòng)證明分離邏輯斷言之間蘊(yùn)含關(guān)系的證明策略和自動(dòng)產(chǎn)生驗(yàn)證條件并證明Hoare三元組的證明策略，它們同時(shí)兼顧驗(yàn)證效率和易用性。
　

4、　本研究主要內(nèi)容包括：⑴將數(shù)據(jù)結(jié)構(gòu)形狀相關(guān)的領(lǐng)域?qū)Ｓ弥R(shí)（譬如單鏈表）引入到證明策略的實(shí)現(xiàn)中，并對(duì)相關(guān)歸納謂詞做自動(dòng)展開(kāi)來(lái)減少手動(dòng)證明的工作量，從而提高C程序的驗(yàn)證效率。⑵通過(guò)在證明策略中引入預(yù)處理階段來(lái)反饋出錯(cuò)提示信息幫助用戶(hù)定位自動(dòng)證明失敗的問(wèn)題所在，這在進(jìn)行人工交互式證明時(shí)極大地提高了證明策略的可用性和易用性。⑶根據(jù)上述兩個(gè)想法在定理證明工具Coq中實(shí)現(xiàn)了一組C程序證明策略（約一萬(wàn)行Coq代碼），它們能用于全自動(dòng)的驗(yàn)證一些簡(jiǎn)單的操