可證編譯器.pdf

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

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

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