陈飞扬，徐文涛，孙绍山，朱 浩，钱振江

（常熟理工学院 计算机科学与工程学院，江苏 常熟 215500）

1 引言

堆栈机器（stack machine）是计算机科学的一种计算模型，它利用“后进先出”的堆栈来存储临时变量，在执行相关指令时，指令操作数从堆栈“弹出”，然后把计算结果“推进”堆栈. 因为大部分算术表达式可以较为容易地转换为后缀表示法，所以用堆栈形式执行部分高级语言的效率很高. 由于堆栈机器的特点，其编译器（compiler）也相比其他结构机器的编译器要简单、快速.

形式化方法（formal methods）是用于计算机软件工程和硬件工程的开发和验证技术. 基于数学分析，它有助于保证设计的可靠性和鲁棒性. 如今，借助内置的决策程序和定理证明器，越来越多的人开始使用交互式定理证明（Interactive Theorem Proving）工具来对设计进行形式化验证.

本文基于Isabelle/HOL对堆栈机器的简单编译器进行形式化验证，证明对于由算术类型表达式和布尔类型表达式构成的语言，堆栈机器编译器的正确性.

2 相关研究

目前在形式化领域，要验证模型的正确性，有不少定理证明器（theorem provers）可供使用，如Isabelle［1］、HOL-light［2］和HOL4［3］等. 较为相关的是许多操作系统安全验证，如Walker等人对UCLA Secure Data Unix内核的验证［4］，Bevier博士对KIT的形式化验证［5-8］，由澳大利亚国家ICT实验室（NICTA）在2004—2006年实施发起的L4.verified项目［9］.

3 编译表达式简介

3.1 表达式简介

为了便于模拟，把表达式分为两类：布尔类型表达式由变元、常元、布尔类型一元运算符、布尔类型二元运算符构成；算术表达式由变元、常元、算术类型一元运算符、算术类型二元运算符、条件表达式构成.其中，条件表达式特指根据布尔表达式的真假，计算第一或第二个算术表达式的值.

3.2 堆栈机器指令简介

把堆栈机器的指令分为两类：布尔表达式相关的指令和算术表达式相关的指令.

布尔表达式相关的指令包括：（1）载入布尔类型常量；（2）载入布尔类型地址内容；（3）对一个栈顶元素应用布尔类型一元运算并以计算结果代替它；（4）对两个栈顶元素应用布尔类型二元运算并以结果代替它们.

算术表达式相关的指令包括：（1）载入算术类型常量；（2）载入算术类型地址内容；（3）对一个栈顶元素应用算术类型一元运算并以计算结果代替它；（4）对两个栈顶元素应用算术类型二元运算并以结果代替它们；（5）根据栈顶布尔类型的值来决定选取两个算术表达式中哪一个的值，如果为真则取第一个的值，反之取第二个的值.

3.3 编译器简介

根据要生成的指令类型，把编译器分为布尔表达式编译器和算术表达式编译器. 对布尔类型表达式，用布尔表达式编译器把相关操作编译为布尔表达式相关的指令，并存放于布尔表达式相关指令的指令表中. 同理，对于算术类型表达式，用算术表达式编译器把相关操作编译为执行算术表达式相关的指令，并存放于算术表达式相关指令的指令表中.

3.4 堆栈机器运行行为简介

堆栈机器运行需要依靠指令表、存储器、堆栈3个部分. 处理器执行指令表中的指令，存储器保存表达式地址，堆栈存储程序运行时的数据. 其中，存储器堆栈用表来模拟，而对于布尔表达式相关的指令和算术表达式相关的指令，分别由两个函数来模拟处理器的行为.

4 编译器在Isabelle/HOL中的形式化

4.1 表达式形式化

因为算术表达式的条件表达式依赖布尔表达式，所以需要先形式化布尔表达式，如图1所示.

参照布尔表达式，形式化算术表达式，如图2所示.

为了得到表达式计算的结果，需要对两类表达式的求值进行形式化，如图3所示.

4.2 堆栈机器指令形式化

同样，先形式化布尔表达式相关的指令，再形式化算术表达式相关的指令，如图4所示.

4.3 编译器形式化

编译器的行为可以用函数来模拟，根据表达式的类型，分别用两个函数来模拟编译布尔表达式和算术表达式的行为，如图5所示.

图1 布尔表达式形式化

图2 算术表达式形式化

图3 表达式求值形式化

4.4 处理器形式化

为了验证编译器的正确性，需要模拟处理器来执行编译过的表达式. 同样，用两个函数分别模拟处理器执行布尔表达式相关指令的行为和处理器执行算术表达式相关指令的行为，如图6所示.

图4 堆栈机器指令形式化

图5 编译器形式化

4.5 编译器正确性证明

要证明编译器的正确性，即证明处理器执行编译器编译过的表达式能得到正确的值.

首先，证明编译器编译布尔表达式的正确性. 为了证明处理器能正确执行编译过的多条表达式，需要证明布尔表达式相关指令是可以合并的（引理1）.

引理1append_bool： "∀bs. execute_bool （xs @ ys） s bs = execute_boolys s （execute_boolxs s bs）"

根据引理1，可以证明处理器执行布尔表达式相关指令能得到正确的值（定理1）.

定理1correct_bool： "∀bs. execute_bool （compile_bool e） s bs = （value_bool e s） # bs"

然后，证明编译算术表达式的正确性. 同理，先证明算术表达式相关指令可以合并（引理2）.

引理2append_arith："∀ vs. execute_arith （xs @ ys） env s vs = execute_arithysenv s （execute_arithxsenv s vs）"

根据引理2和定理1，可以证明处理器执行算术表达式相关指令也能得到正确的值（定理2）.

定理2correct_arith： "∀ vs. execute_arith （compile_arith e） env s vs = （value_arith e env s） # vs"

综上，编译器能正确编译布尔表达式和算术表达式，完成编译器正确性证明，引理1、定理1、引理2、定理2的证明过程见图7.

最终的证明结果如图8所示，“No subgoals!”表示证明完成.

图6 处理器形式化

图7 引理1、定理1、引理2和定理2的证明脚本

5 结语

本文借助定理证明器Isabelle/HOL，对布尔表达式和算术表达式、堆栈机器指令、编译器、堆栈机器运行行为进行形式化，验证了堆栈机器简单编译器的正确性. 目前对于编译器形式化验证的工作较少，本文仅对堆栈机器的简单编译器进行验证，考虑到实际应用中编译器的复杂度，仍有大量的课题有待研究.

图8 证明结果