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

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

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