VeriJava中靜態(tài)驗證器的設(shè)計與實現(xiàn).pdf

1、軟件的可靠性一直是工業(yè)界和學(xué)術(shù)界關(guān)注的焦點，隨著軟件系統(tǒng)的規(guī)模和復(fù)雜度的不斷增長，如何保證其可靠性成為了亟待解決的問題。軟件開發(fā)方法和軟件工程也在不斷發(fā)展，當(dāng)今主流的面向?qū)ο蠓椒ㄒ呀?jīng)走過了20多個年頭，它在提供給系統(tǒng)良好的靈活性和可復(fù)用性的同時，并沒有忽略它的可靠性，契約式設(shè)計就是一種用于構(gòu)建高可靠的面向?qū)ο筌浖到y(tǒng)的系統(tǒng)化方法。Bertrand Meyer在90年代提出了契約式設(shè)計，并且發(fā)明了Eiffel編程系統(tǒng)來大力推廣這種方法。契

2、約式設(shè)計中使用契約來檢查程序正確性的方法來源于早期的程序驗證思想，雖然其主要價值體現(xiàn)在其面向?qū)ο蟮脑O(shè)計方面，但是它的出現(xiàn)也為程序驗證提供了一條新的途徑。在21世紀(jì)初，圖靈獎獲得者C.A.R.Hoare將60年代提出的“驗證編譯器”（verifying compiler）的構(gòu)想作為計算機科學(xué)的重大挑戰(zhàn)重新提出，并且號召全世界范圍內(nèi)的計算機科學(xué)家參與到這個宏大的項目當(dāng)中。 本文介紹的VeriJava項目旨在構(gòu)建一個全面支持契約式設(shè)計

3、的面向?qū)ο缶幊滔到y(tǒng)。VeriJava是Verifiable Java的縮寫，它通過針對Java語言在語言層面上進行的擴展，提供了程序契約的表達方法，并同時提供了一套動態(tài)檢查和靜態(tài)驗證機制。 本文重點研究了VeriJava項目中的靜態(tài)驗證器模塊的設(shè)計和實現(xiàn)，其目的是構(gòu)建一個靜態(tài)驗證程序，用以驗證含有契約信息的VeriJava程序的正確性。靜態(tài)驗證器與動態(tài)檢查的不同之處在于它可以在運行程序之前發(fā)現(xiàn)程序中潛在的錯誤，并能夠結(jié)合契約所提

4、供的信息，排除某些錯誤存在的可能性。與傳統(tǒng)的程序驗證所追求的嚴(yán)格的正確性不同，VeriJava靜態(tài)驗證器所要處理的是VeriJava語言中輕量級契約信息，它的目標(biāo)是發(fā)現(xiàn)最為常見的錯誤，并且消耗較少的時間和空間。在研究和設(shè)計過程中，本文主要參考了ESC/Java、Spec＃項目，并且回顧了Floyd、Dijkstra以及Hoare等人的程序驗證理論，在比較和分析之后確定了VeriJava靜態(tài)驗證器的理論基礎(chǔ)以及設(shè)計和實現(xiàn)的策略。本文詳細(xì)的