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

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

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

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

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