Prog2

本来感觉没啥难的，半路杀出一个和 Prog1 一样恶心的语法，记录一下。

Formal Semantics

这里依然是取一个子集, 我们叫它 C0.

Tokens

Prog p ::= Seq(s,p)
        | Term
        | Crash

Stmt s ::= Assign[l,e]
        | Block[p]
        | If[e,s1,s2]
        | While[e,s]
        | Abort

LExpr ::= Var_x
Expr ::= l  L-value
        | Const_x
        | Binary_x expr

Op o ::= r | m
Aop r ::= Arithmetic Ops
Cop m ::= Comparison Ops

两个函数

我们有两层抽象：

1. 变量名到地址，用 $\rho$ 表示
2. 地址到储存的值，用 $\mu$ 表示

理论上来说， state $\Sigma = \rho \times \mu$, 但有了语法糖我们直接写变量名到值的语法糖也行。

注意如果有 NULL 地址的话好像还是得分开写。

Config & Execution Trace

进一步，我们定义 Config $c$ 为 $Prog \times \Sigma$

然后 Execution Trace 就是一个程序执行后 $c$ 的集合。所以是：

$$\langle p|\sigma \rangle =c_1c_2c_3\dots$$

Eval

这里分为两种 Eval ： R and L

R 出 Val， L 出地址。

两个可以通过 $\mu$ 互转

Termination

到这里应该可以看出来这个是状态机模型了。

这里 Terminate 的定义是对于一个 Execution Trace $c1,\dots,c_n$, 不存在 $c'$ 使得 $c_n\rightarrow c'$, 那么有 $\langle p|\sigma\rangle \downarrow c_n$， 也即这个 Config terminate 于 $c_n$. 反之就不 Terminate。

Pointer Support

记住 R 出 Val， L 出 地址

这个需要在 Eval 部分新加两个语法：

$$R[\&l]\sigma = L[l]\sigma L[*e]\sigma = R[e]\sigma$$