编译器的定义就是一段程序，它能读一些用抽象(几乎是数学的)记号表述的用户程序并将其翻译成更晦涩难懂的但能在计算机上直接运行的机器码。一个严重的问题是许多编译好的程序含有错误，一些错误甚至会导致程序崩溃。检测和消除这些错误就需要艰辛的劳动，即费时耗力的调试过程。 为了减少错误或者写出正确的编译程序，并且尽量避免艰辛的调试过程，计算机科学家在这几十年来做了大量的工作：比如最初的为程序加入断言，到后来的精化程序。 本文就是用软件实现编译器代码生成的一篇论文。它能把OCCAM语言翻译成自定义的类汇编代码。 OCCAM语言是一种简洁的面向过程的语言，它非常类似于流行于世的C、Pascal等语言，而且比C更加简洁明了。更为重要的是，OCCAM语言以其能够处理并行和通信的特性，使其在21世纪仍有重要的研究价值。因此，对OCCAM的编译就显得尤为重要，这也是本文选用OCCAM的原因。 本文的特色就在于综合了前人的证明思路，不但给出了完整的OCCAM语言编译子句，而且用数学定理和模拟的方法证明了编译程序的正确性(无需测试，代码生成是完全正确的)。具体来说，本文采用精化的理论，证明OCCAM语言和类汇编代码之间是有精化关系的，而这种证明过程中的数学定理形式，被直接写成编译程序的子句。因此，编译程序本身的正确性就毋庸质疑。但数学定理的形式与常用的C、JAVA等语言有一定差距，为了不节外生枝，我们采用人工智能的PROLOG语言对OCCAM语言实行编译。对于处理并行和通信的OCCAM部分，直接采用定理的方式是有困难的，因此本文采用仿真的办法，来说明我们最后完成的类汇编代码，执行的操作都在源程序允许的范围之内，来说明编译程序的正确性。本文的独创性也就在这里：第一次将两种方式用在一起来证明编译的正确，并且在文章的后面，给出了完全模拟编译的环境并给出实验结果。