可證編譯器.pdf

1、編譯器的定義就是一段程序，它能讀一些用抽象(幾乎是數(shù)學的)記號表述的用戶程序并將其翻譯成更晦澀難懂的但能在計算機上直接運行的機器碼。一個嚴重的問題是許多編譯好的程序含有錯誤，一些錯誤甚至會導致程序崩潰。檢測和消除這些錯誤就需要艱辛的勞動，即費時耗力的調(diào)試過程。 為了減少錯誤或者寫出正確的編譯程序，并且盡量避免艱辛的調(diào)試過程，計算機科學家在這幾十年來做了大量的工作：比如最初的為程序加入斷言，到后來的精化程序。 本文就是用軟

2、件實現(xiàn)編譯器代碼生成的一篇論文。它能把OCCAM語言翻譯成自定義的類匯編代碼。 OCCAM語言是一種簡潔的面向過程的語言，它非常類似于流行于世的C、Pascal等語言，而且比C更加簡潔明了。更為重要的是，OCCAM語言以其能夠處理并行和通信的特性，使其在21世紀仍有重要的研究價值。因此，對OCCAM的編譯就顯得尤為重要，這也是本文選用OCCAM的原因。 本文的特色就在于綜合了前人的證明思路，不但給出了完整的OCCAM語言

3、編譯子句，而且用數(shù)學定理和模擬的方法證明了編譯程序的正確性(無需測試，代碼生成是完全正確的)。具體來說，本文采用精化的理論，證明OCCAM語言和類匯編代碼之間是有精化關(guān)系的，而這種證明過程中的數(shù)學定理形式，被直接寫成編譯程序的子句。因此，編譯程序本身的正確性就毋庸質(zhì)疑。但數(shù)學定理的形式與常用的C、JAVA等語言有一定差距，為了不節(jié)外生枝，我們采用人工智能的PROLOG語言對OCCAM語言實行編譯。對于處理并行和通信的OCCAM部分，直接