代码正确性的验证
编译器正确性的验证
直观的正确性判定
在经过一系列的数据变化，最终正确的结果会被放到桟式抽象机的顶部，如果与预期结果一致，那么我们可以认为编译器在结果上正确。
如何描述这一个过程？
- 代码执行一步，多步到最终的执行结束？
- 符号表与代码对应地址的表述
- 加减法的形式化表述等
定义语义动作
语义动作的定义主要为描述过程提供简化的思路。
对应字母的说明如下
定义符号表映射函数
假设 \(\rho\) 是一个用于将对应变量与地址对应的函数。然后用该函数将对应的变量取值过程进行描述。如果T后面跟的是一个整数N,那么我们直接取其值生成代码，如果是变量用函数映射出其地址，然后取其值，如果是一个表达式，那么递归的进行调用。即如下图所示
直观上看，如果该函数对变量 \(x\) 做相应映射，能够得到一个自然数，即该变量在栈中分配到的地址，如果为空，代表着该变量没有被分配空间。同时，上述过程用数学的方法描述了变量的分配过程。
定义表达式运算函数
首先根据加法表达式的对应BNF含义，一个加法表达式TS可以是一个加号后面跟一个具体的项T，对其定义描述函数为用上面的G函数映射出其值与后面的表达式相加。或者一个加法表达式也可以是两个加法表达式相加，即递归的定义。那么此时的表达式运算函数除了执行上述过程外还需要在G中得到一个输出。减法表达式的情况类似。如下图所示
这样我们就把一段抽象机代码从变量映射到执行取值的过程表示出来，接下来我们只需要表示出程序的运行。
变量与值的映射
我们定义一个函数 \(\sigma\) 来简化变量x到其对应值的映射关系，即一次 \(\sigma\) 映射等价于一次 \(\rho\) 函数映射和G函数映射。
那么很容易我们可以得到下面的定义
即
- 字面值的映射仍是字面值。
- 获取变量的值就调用 \(\sigma\) 映射
- 一个带括号表达式的值就是括号里面的运算结果用 \(\sigma\) 函数映射得到的值。
表达式用 \(\sigma\) 函数表达
那么自然的一个加法表达式就可以用 \(\sigma\) 函数来进行简化的表达。即 \([+T]_{TS}(\sigma)\) 就是对应的项的取值用 \(\sigma\) 函数映射得到的值。\([+T TS]_{TS}(\sigma)\) 就是两项分别用 \(\sigma\) 函数映射得到的值。 减法的分析类似。如下图所示
程序的执行表示
我们用如下的方式定义一个程序的运行
\((c,s,pc) -> (c,s^{'},pc^{'})\)
c表示代码，s是栈顶的运算结果，pc是指示程序的运行。上述过程的表述为，当程序执行一步，pc指向下一条指令，s变化为当前运算结果。于是，加法和减法的描述就为
其中 z1，z2表示栈顶的两个元素。
正确性的陈述
于是在前面的铺垫下，我们可以得出我们对编译器的判定理论： 如果对于任意的变量，我们都为其分配了地址，在一系列的运算后，我们得到的栈顶元素值和最终预期值相同，我们认为程序的正确性得到了证明，反之不正确。如下
