Imperative Spec 的一些细节

语法

Stmt ::= skip ::= ∣ if Expr then Stmt else Stmt ::= ∣ while Expr do Stmt ::= ∣ return Expr ::= ∣ let x := Expr ::= ∣ x := Expr ::= ∣ Stmt; Stmt

最直觉的规则：

[[skip; s]] [[if (c) then s_{t} else s_{e}; s]] [[while (c) do s_{t}; s]] [[return e]] [[let x := e; s]] p [[x := e; s]] p = [[s]] = if [[c]] then [[s_{t}; s]] else [[s_{e}; s]] = if [[c]] then [[s_{t}; while (c) do s_{t}; s]] else [[s]] = [[e]] = [[s]] p [[e]] = [[s]] p {x / [[e]]}

携带 $e n v$ （表示当前环境中的变量/参数）：

[[if (c) then s_{t} else s_{e}; s]]_{e n v} [[while (c) do s_{t}; s]]_{e n v} [[return e]]_{e n v} [[let x := e; s]]_{p} [[x := e; s]]_{p} = if [[c]]_{e n v} then [[s_{t}; s]]_{e n v} else [[s_{e}; s]]_{e n v} = if [[c]]_{e n v} then [[s_{t}; while (c) do s_{t}; s]]_{e n v} else [[s]]_{e n v} = [[e]]_{e n v} = [[s]]_{(p, x)} p [[e]]_{p} = [[s]]_{p} p {x / [[e]]_{p}}

语义中采用的模式为通过 Seq 连接语句，而实际的语言中使用语句块来表示多条语句。

BStmt ::= skip ::= ∣ if Expr then BStmt else BStmt ::= ∣ while Expr do BStmt ::= ∣ return Expr ::= ∣ let x := Expr ::= ∣ x := Expr ::= ∣ {BStmt *}

转换模式：计算每条语句的第一条可执行语句和剩余的语句列表。对于嵌套语句块，直接展平。

head :: [BStmt] \to Stmt tail :: [BStmt] \to [BStmt]

于是翻译规则可以定义如下：

translate S = head S; translate tail S

展平语句块后，块作用域的信息丢失了。我们需要在翻译时保留块作用域的信息。

int x = 2;
{ int x = 1; }
return x;

对嵌套作用域内的变量提前重命名：

int x = 2;
{ int x' = 1; }
return x;

带有语句命名的语法：

NStmt SStmt Stmt ::= ⟨ nam e, SStmt ⟩ ::= end ::= ∣ Stmt; NStmt ::= if Expr then NStmt else NStmt ::= ∣ while Expr do NStmt ::= ∣ return Expr ::= ∣ let x := Expr ::= ∣ x := Expr

BStmt ::= skip ::= ∣ if Expr then BStmt else BStmt ::= ∣ while Expr do BStmt ::= ∣ return Expr ::= ∣ let x := Expr ::= ∣ x := Expr ::= ∣ {BStmt *} ::= ∣ Label l : BStmt \leftarrow explicit label

从语句块到带命名的语句的转换：

head tail translate :: [BStmt] \to ⟨ nam e : string, Stmt ⟩ + end :: [BStmt] \to [BStmt] :: [BStmt] \to NStmt

translate S = ⟨ nam e, (h e a d; translate tail S) ⟩ translate S = ⟨ \emptyset, end ⟩ when head S = ⟨ nam e, h e a d ⟩ when head S = end