论文部分内容阅读
堆栈机器(stack machine)作为一种计算模型,不仅执行部分高级语言的效率很高,而且其编译器也简单、快速.在形式化领域,目前已有不少定理证明器用来验证模型的正确性.本文对堆栈机器的简单编译器进行介绍,对布尔表达式和算术表达式、机器指令、编译器、机器运行行为在Isabelle/HOL中进行形式化,验证编译器的正确性.