指針程序的分析以及循環(huán)不變形狀圖的推斷.pdf

1、近年來(lái)，計(jì)算機(jī)軟件系統(tǒng)在日常生活和工作中的地位越來(lái)越重要，而計(jì)算機(jī)軟件規(guī)模也日漸龐大，其安全問(wèn)題也因此而受到更多的重視。在一些安全攸關(guān)的領(lǐng)域，軟件的高可信已經(jīng)變得十分必要。提高軟件可信程度的一個(gè)重要方法就是形式程序驗(yàn)證。在典型的形式程序驗(yàn)證過(guò)程中，程序員通常需要手工書(shū)寫(xiě)函數(shù)前后條件以及循環(huán)不變式，給程序員帶來(lái)了極大的不便。同時(shí)，循環(huán)不變式的自動(dòng)推斷問(wèn)題又遲遲沒(méi)有解決。這都是形式程序驗(yàn)證在工業(yè)界的應(yīng)用進(jìn)展緩慢的原因。
　　 研究自

2、動(dòng)推斷循環(huán)不變式的方法，不僅對(duì)程序驗(yàn)證，而且對(duì)程序分析等領(lǐng)域也具有重要的意義。對(duì)指針程序而言，數(shù)據(jù)結(jié)構(gòu)的形狀分析給循環(huán)不變式的推斷乃至程序驗(yàn)證提供很多有用的信息。
　　 本文使用一種新的方式來(lái)解決指針程序分析驗(yàn)證中的困難及循環(huán)不變式的自動(dòng)推斷問(wèn)題。我們?cè)O(shè)計(jì)了一個(gè)形狀系統(tǒng)，要求程序員聲明各種遞歸結(jié)構(gòu)類(lèi)型參與構(gòu)建的數(shù)據(jù)結(jié)構(gòu)的形狀，并聲明指針變量所指向的形狀，以換取編譯器或其他軟件工具檢查程序是否有形狀錯(cuò)誤，幫助排除所構(gòu)建的形狀偏離程

3、序員期望的程序。與此同時(shí)，我們還設(shè)計(jì)了一種基于形狀圖邏輯的形狀分析方法，為程序驗(yàn)證提供指針相關(guān)的循環(huán)不變形狀圖和函數(shù)前后條件形狀圖。
　　 形狀圖是表達(dá)程序所操作的聲明指針和動(dòng)態(tài)分配的結(jié)構(gòu)體中域指針的指向的一種圖形，它不僅準(zhǔn)確地表達(dá)了指針之間的相等關(guān)系，還能提供其他有用信息，例如可用來(lái)查詢(xún)?cè)L問(wèn)路徑的別名。循環(huán)不變形狀圖是循環(huán)不變式中關(guān)于指針部分的形狀圖表示，描述了循環(huán)不變式中指針之間的相等關(guān)系等信息。形狀圖邏輯把形狀圖看作程序中

4、指針信息斷言的一種圖形表示，并在此基礎(chǔ)上對(duì)Hoare 邏輯進(jìn)行擴(kuò)展，可用于對(duì)操作易變數(shù)據(jù)結(jié)構(gòu)的指針程序的分析和驗(yàn)證。
　　 基于形狀圖邏輯，采用先形狀分析，后程序驗(yàn)證的方法，我們實(shí)現(xiàn)了一個(gè)程序驗(yàn)證器。該驗(yàn)證器能夠驗(yàn)證本文所定義的各種形狀的程序，并且不需要程序員提供有關(guān)數(shù)據(jù)結(jié)構(gòu)形狀的函數(shù)前后條件和循環(huán)不變式，但需要程序員提供非指針型數(shù)據(jù)的函數(shù)前后條件和循環(huán)不變式。本文所設(shè)計(jì)實(shí)現(xiàn)的方法在一定程度上解決了循環(huán)不變式自動(dòng)推斷的難題，為程