斯坦福cs231(编译原理)の 6 Cool Operational semantics

本文是斯坦福cs143编译原理的笔记，内容大部分来自于课件和自己的理解，笔者能力和精力有限，如果有错误欢迎指出。

引言

类比：

parser阶段，我们要给每种token设置对应的action

语法分析阶段，有一系列的文法式，要在每个文法式规约的时候设置action，规定对应的行为

类型分析阶段：对每一种表达式设置对应的语义动作，进行语义分析

同样的优化阶段：对每一种表达式设置对应的代码生成及优化动作。

如何形式化表示这些表达式对应动作（语义，我理解就是表达式的动作）

Denotational semantics: 数学函数表示

Axiomatic semantics: 通过逻辑公式描述程序行

Operational sematics: 通过执行规则描述程序评估

操作语义

在类型推断和检查的时候，引进过这样一种符号： \[ Context \vdash e: C 在给定大的上下文context里，表达式是类型C \] 同样的，评估阶段(代码生成阶段之前的准备工作)，也会用类似的符号： \[ Context \vdash e: v 在给定大的上下文context里，表达式会被评估为值v \] 🌰： \[ \frac{Context \vdash e1: 5 \quad Context \vdash e2: 7}{Context \vdash e1 + e2: 12} \] > 在语境Context下e1被评估为5，e2被评估为7，那么e1+e2就是12，当然这种是常量比较简单哈，没什么用处，实际情况下有变量的情况下就复杂了； >

考虑评估：y <- x + 1

由于存在局部作用域，所以评估一个值，需要：

Environment: where in memory a variable is

Store: what is in the memory

简单来说就是两个映射表：

Enviroment：va r => loc

Store: loc => value

形式化表示：

\[ E = [a: l1, b: l2] \quad 变量a在内存中的l1处，b在内存的l2处 \\ S = [l1 => 5, l2 => 7] \quad l1处存储的值是5，l2处存储的值是7 \\ S' = S[l2/l1] \quad defines \quad a \quad store \quad S'\quad such \quad that \\ S'(l1) = 12 \quad and \quad S'(l) = S(l) \quad if \quad l \neq l1 \\ 简单理解下S'就是S在l1处做了单点修改 \]

cool里的语义

cool里面值都是对象（cool是面向对象的语言）

X(a1 = l1, ..., an = ln) 表示为一个cool 对象，其中

X是类
ai是其属性，包含继承的属性
li是对应ai被存储的内存位置

cool内置类：

Int(5),
Bool(true)
String(4, "cool") the string "Cool" of length 4
特殊值：void，该对象上没有方法，如果调用isvoid将会抛出异常，cool里对void的具体实现时NULL（Cpp里的空指针，因为cool是用cpp实现的）

考虑如下评估式： \[ {so, E, S \vdash e: v, S'} \] so(self object)， E 是当前的变量环境，S是当前Store；

e获得了评估结果后值是v，并且新的store是S‘

评估的结果实际是值v和新的Store，新的Store是有副作用(副作用是值引用修改，而不是copy)

但是在评估后有一些事不会改变的：

变量环境
self
操作语义允许递归

下面具体介绍了cool的一些操作语义评估，我就简单那几个比较经典的：

变量使用：在E中找到id的位置，然后在S中找对应的值 \[ \frac{E(id) = I_{id} \quad S(I_{id}) = v}{so, E, S \vdash id: v, S} \] ------

self: \[ {so, E, S \vdash self: so, S} \] ------

变量赋值：就是对id处做单点修改返回新的Store，id的评估结果就是e的评估结果v \[ \frac{so, E, S \vdash e: v, S_1 \quad E(id) = I_{id} \quad S_2 = S_1[v/id]}{so, E, S \vdash id=e: v, S2} \] e1+e2：先递归对e1评估，评估后e1的值是v1，并产生新的Store S1，接着对e2递归进行评估，评估后e2的值是v2，并产生新的Store S2，最终e1+e2的评估结果就是值为v1 + v2，新的Store S2 \[ \frac{so, E, S \vdash e: v, S_1 \quad so, E, S1 \vdash e: v2, S_2}{so, E, S \vdash e1 + e2: v1 + v2, S2} \] ------

🌰：{ X = 7 + 5; 4;}

先对一个表达式X=7+5评估 \[ {so, [X<-1], [l<-0] \vdash x=7+5: ?, ?} \] 继续递归对7+5进行评估 \[ {so, [X<-l], [l<-0] \vdash 7+5: ?, ?} \] 继续递归对7评估： \[ {so, [X<-l], [l<-0] \vdash 7: Int(7), [l<-0]} \] 同样的对5评估： \[ {so, [X<-l], [l<-0] \vdash 5: Int(5), [l<-0]} \]

返回到上一层7+5: \[ {so, [X<-l], [l<-0] \vdash 7+5: Int(12), [l<-0]} \] 继续返回到上一层x=7+5：

这个时候已经处理完了7+5，继续处理x，这是声明变量，得到单点更新后的Store： \[ [l<-0](12/l) => [l/12] \] 这个时候子表达式都处理完了，继续处理最外层的第一个表达式 \[ {so, [X<-l], [l<-0] \vdash x=7+5: 12, [l<-12]} \] 继续处理同级别的表达式4 \[ {so, [X<-l], [l<-12] \vdash 4: Int(4), [l<-12]} \]

\[ \frac{...}{so, [X<-1], [1<-0] \vdash \{X=7+5;4;\}: Int(4), [1<-12]} \]

if-else

\[ \frac{so, E, S \vdash e1: Bool(false), S1}{so, E, S \vdash while \quad e1 \quad loop \quad e2 \quad pool: void, S1} \] ------

while

声明变量： \[ \frac{so, E, S \vdash e1: v1, S1 \quad so, ?, ? \vdash v, S2}{so, E, S \vdash let \quad id: T = e1 \quad in \quad e2: v2, S2} \] e2应该在什么环境下评估呢（问号处应该填什么呢）？

—仍然是E，但是E里应该新增映射id => Inew，表示为id新分配了一块内存，同样的Store应该是有新的映射 Inew => v1

新增符号：Inew = newloc(S)，表示Inew是一个新分配的内存，newloc可以理解为是一个内存分配函数 \[ \frac{so, E, S \vdash e1: v1, S1 \quad I_{new} = newloc(S1) \quad so, E[I{new}/id], S1[v1/I_{new}] \vdash v2, S2}{so, E, S \vdash let \quad id: T = e1 \quad in \quad e2: v2, S2} \]

new对象的评估语义：

首先，为对象的所有参数分配内存（本质上就是分配对象）
为对象设置缺省值
评估对象的初始化语句，并重新设置属性值
返回被分配的对象

每个对象都有默认值

int： Int(0)
bool: Bool(false)
String: String(0, '')

类A的形式化表示：

class(A) = (a1: T1 <-e1, ..., an: Tn <- en)，其中：

ai是属性，包含继承属性
Ti是属性的类型
ei是初始化表达式

在评估初始化表达式阶段：

self is the current object
only the attributes are in scope()，作用域内只有属性
属性的初始值都是默认值，主要是防止在初始化语句里面会用到这些初始值，比如:Class A { a <- a }，用a初始化a，如果a没有默认值，可能会有异常；

Informal semantics of class e0.f(e1, ..., en)：