1、現今計算機和互聯網技術的迅速發(fā)展不僅帶來了具有更強計算能力的計算機、更加便捷的信息交流方式，而且也對計算機軟件的安全性和可靠性提出了更高的要求。目前軟件安全性的保證主要是依靠程序設計者自身的能力以及軟件測試。在軟件開發(fā)過程中使用形式化方法進行程序驗證是提高軟件安全性的一個有效途徑。 出具證明編譯器是近些年來結合程序設計和程序驗證技術所出現的研究方向。作為驗證編譯研究的一個分支，出具證明編譯器的主要設計思想是整個系統能夠在編譯獲得

2、目標代碼的同時也為這些目標代碼生成用于說明目標代碼滿足某些程序性質的證明。 本文所介紹的工作基于我們的出具證明編譯器原型系統項目，是我們進行出具證明編譯研究的一次嘗試。原型系統的設計和實現主要涉及到編譯器技術、基于Hoare邏輯的程序驗證技術等。此外，為了更好地考察與動態(tài)存儲管理相關的程序性質，我們不僅在源語言的設計中保留了指針類型以及動態(tài)存儲管理的語句，而且也設計了指針邏輯。 本文重點介紹了出具證明編譯器原型系統中主要

3、功能模塊的實現，這些模塊包括位于原型系統前端的驗證條件生成器，位于后端的代碼生成器和證明生成器。文中不僅描述了這些模塊所使用的數據結構的設計以及它們各自的工作流程，而且也對設計和實現這些模塊的過程中的經驗進行了總結。同時，由于目標代碼級程序性質證明框架的實現使用了定理證明輔助工具Coq，因此原型系統在設計和實現的過程中也加入了與Coq系統接口問題的考慮。 通過整個原型系統的構建，我們初步解決了出具證明編譯中的若干問題，特別是源語