程序语言与编译原理：期末复习

Last updated on December 14, 2025 pm

本文为 SJTU-CS2612 程序语言与编译原理课程的期末复习。

Lecture 1：词法分析

1. 词法分析的基本知识

核心任务：词法分析是编译器前端的第一步，它的主要任务是将源代码的字符串切分成一个个有意义的标记 (token)
标记的分类：根据标记在语法中承担的功能，可以将它们分为不同的类别，以 While+DB 语言为例
- 运算符：+ - * / % < <= == != >= > ! && ||
- 赋值符号：=
- 间隔符：( ) { } ;
- 自然数：0 1 2 ...（归为一类 TOK_NAT）
- 变量名：a0 __x ...（归为一类 TOK_IDENT）
- 保留字：var if then else while do
- 内置函数名：malloc read_char read_int write_char write_int
- 事实上，在上述标记除了所有自然数分为一类、所有变量名分为一类之外，其他每个标记应当单独分为一类

enum token_class {
  // 运算符
  TOK_OR = 1, TOK_AND, TOK_NOT,
  TOK_LT, TOK_LE, TOK_GT, TOK_GE, TOK_EQ, TOK_NE,
  TOK_PLUS, TOK_MINUS, TOK_MUL, TOK_DIV, TOK_MOD,
  // 赋值符号
  TOK_ASGNOP,
  // 间隔符号
  TOK_LEFT_BRACE, TOK_RIGHT_BRACE,
  TOK_LEFT_PAREN, TOK_RIGHT_PAREN,
  TOK_SEMICOL,
  // 自然数
  TOK_NAT,
  // 变量名
  TOK_IDENT,
  // 保留字
  TOK_VAR, TOK_IF, TOK_THEN, TOK_ELSE, TOK_WHILE, TOK_DO,
  // 内置函数名
  TOK_MALLOC, TOK_RI, TOK_RC, TOK_WI, TOK_WC
};

标记的存储:
- 大部分标记（如运算符、保留字）只需要记录它们的类别 (Token Class) 即可
- 一些标记需要存储额外的信息，例如：
  - 自然数 (TOK_NAT)：需要存储它表示的无符号整数值 n
  - 标识符 (TOK_IDENT)：需要存储它对应的字符串的地址 i
- 可以使用 union 结构来高效地存储这些额外信息，因为一个 token 不可能既是自然数又是标识符

union token_value {
  unsigned int n;
  char * i;
  void * none;
};

2. 正则表达式 (Regular Expression)

定义：正则表达式是一种用来描述字符串集合的语言，它是定义词法分析器匹配规则的基础
核心构成与优先级:
- $c$ ：单个字符
- $\epsilon$ ：空字符串
- $r_1 r_2$ ：两个字符串的连接
- $r_1 | r_2$ ：两个字符串的并集
- $r*$ ：重复出现一类字符串 0 次 1 次或多次
- 优先级： $* > \text{ 连接 } > |$
例子：
- (a|b)c 表达的字符串有 ac , bc
- (a|b)* 表达的字符串有空串, a , b , ab , aaaaa , babbb 等
- ab* 表达的字符串有 a , ab , abb , abbb , abbbb 等
- (ab)* 表达的字符串有空串, ab , abab 等
常见简写形式：
- 字符的集合：[a-cA-C] 等价于 a|b|c|A|B|C
- 可选的字符串： $r?$ 等价于 $r|\epsilon$ (出现 0 次或 1 次)，例如 a?b 表达的字符串有 b , ab
- 字符串：例如 "abc" 表示字符串 abc
- 重复至少一次：例如 a+ 表达的字符串有 a , aa , aaa 等
- 自然数常量："0"|[1-9][0-9]*
- 标识符（不排除保留字、内置函数名）：[_a-zA-Z][_a-zA-Z0-9]*

3. Flex 词法分析工具

Flex 是一个词法分析器生成器，它能自动地将描述标记的规则（正则表达式）转换成一个高效的 C 语言词法分析器。

工作流程：
- 输入：一个 .l 文件，包含基于正则表达式的词法分析规则
- 生成：运行 flex 命令处理 .l 文件，生成一个 C 语言实现的词法分析器 lexer.c，其中包含 yylex() 函数
- 编译：使用 C 编译器（如 gcc）编译生成的 lexer.c 和其他业务逻辑代码（如 main.c），最终得到一个可执行文件
输入文件头 (.l)：
- 说明 Flex 生成词法分析器的基本参数
- 指定所生成的词法分析器的文件名
- 词法分析器所需头文件 (.h 文件) 与辅助函数
1
2
3
4
5
%option noyywrap yylineno %option outfile="lexer.c" header -file="lexer.h" %{ #include "lang.h" %}
词法分析用到的辅助函数和全局变量 (lang.h)：

extern union token_value val;
unsigned int build_nat(char * c, int len);
char * new_str(char * str, int len);
void print_token(enum token_class c);

词法分析规则：
- 所有词法分析规则都放在一组 %% 中
- 每一条词法分析规则由匹配规则和处理程序两部分构成
- 匹配规则用正则表达式表示
- 处理程序是一段 C 代码

%%
0|[1-9][0-9]* {
  val.n = build_nat(yytext , yyleng);
  return TOK_NAT;
}
"var" { return TOK_VAR; }
...
%%

Flex 专有 C 程序变量：
- yytext：指向当前匹配到的字符串的指针
- yyleng：当前匹配到的字符串的长度
Flex 的匹配规则：
- 最长匹配原则：如果有多种切分方案，Flex 会选择匹配尽可能长的字符串的那个规则
- 最先出现规则优先：如果同一种切分方案符合多个词法分析规则（正则表达式），Flex 会选择在 .l 文件中最先出现的那个规则
  - 这个特性常用于处理关键字，将关键字的规则放在通用标识符规则之前
词法分析器的使用：main.c（只打印词法分析结果）
- yylex()：每次调用返回一个 token

#include "lang.h"
#include "lexer.h"
int main() {
  enum token_class c;
  while (1) {
    c = yylex();
    if (c != 0) {
      print_token(c);
    }
    else {
      break;
    }
  }
}

词法分析全流程：Makefile

lang.o: lang.c lang.h
        gcc -c lang.c
lexer.c: lang.l
        flex lang.l
lexer.o: lexer.c lang.h
        gcc -c lexer.c
main.o: main.c lang.h lexer.c
        gcc -c main.c
main: main.o lang.o lexer.o
        gcc main.o lang.o lexer.o -o main
%.c: %.l

词法分析器的算法流程：
- 先根据输入的字符串找到正则表达式的匹配结果（若有多种结果则选最长、最靠前的）
- 再更新字符串扫描的初始地址，并执行匹配结果对应的处理程序
在处理程序中不返回的方案：
- 在规则对应的动作代码中，return 语句会中断 yylex() 的执行并返回一个 token，下次调用 yylex() 会从上一次扫描结束的位置继续
- 如果动作代码中没有 return 语句，yylex() 会在执行完动作后，自动继续进行下一次的词法分析

4. 有限状态自动机

有限状态自动机是识别正则表达式所描述的字符串集合的数学模型。

基本概念：
- 有限状态自动机包含一个状态集（图中的节点）与一组状态转移规则（图中的边）
- 每一条状态转移规则上有一个符号
- 状态集中包含一个起始状态，和一组终止状态；起始状态也可能是一个终止状态
例子：

两类自动机：
- 确定性有限状态自动机 (DFA - Deterministic Finite Automata)：
  - 每一条状态转移规则上的符号都是 ascii 码字符。
    – 从任何一个状态出发，每个字符至多对应一条状态转移规则
- 非确定性有限状态自动机 (NFA - Nondeterministic Finite Automata)：
  - 每一条状态转移规则上的符号要么是 ascii 码字符，要么是 $\epsilon$
    – 从一个状态出发，每个符号可能对应多条状态转移规则
    – 通过 $\epsilon$ 转移规则时，不消耗字符串中的字符
接受字符串的定义：一个自动机能接受一个字符串，当且仅当存在一种状态转移的方法，可以从自动机的起始状态出发，依次经过这个字符串的所有字符，到达一个终止状态

5. 将正则表达式转化为 NFA

这是将理论（正则表达式）应用到实践（构建词法分析器）的关键步骤之一。

对于任何一个正则表达式，都可以构造出一个与之等价的 NFA
- 即一个字符串能被这个 NFA 接受当且仅当这个字符串是正则表达式表示的字符串集合的元素
Thompson 构造法：构造方法是递归的，针对正则表达式的五个基本操作进行：
- 为单个字符 $c$ 构造 NFA
- 为空串 $\epsilon$ 构造 NFA
- 为连接 $r_1r_2$ 构造 NFA
- 为并集 $r_1 | r_2$ 构造 NFA
- 为闭包 $r*$ 构造 NFA
这些构造出的 NFA 都有一个唯一的起点和一个唯一的终点
- 但是注意：起点也可能在图中有入度，终点也可能在图中有出度

6. 将 NFA 转化为 DFA

这是将理论（正则表达式）应用到实践（构建词法分析器）的关键步骤之一。

子集构造法 (Subset Construction)：由于 NFA 的不确定性，在某个时刻它可能处于多个状态的集合中，DFA 的每一个状态就对应 NFA 的一个可能的状态集合
步骤：
- DFA 的起始状态是 NFA 起始状态以及所有可以从它通过 $\epsilon$ 转移到达的状态的集合
- 从一个 DFA 状态（即一个 NFA 状态集）开始，计算在接收某一个输入字符后，可以到达的新的 NFA 状态集（同样要包含所有 $\epsilon$ 转移可达的状态），这个新的集合就是 DFA 的一个新状态
- 重复此过程，直到没有新的 DFA 状态产生
- 任何包含 NFA 终止状态的 DFA 状态，都是 DFA 的终止状态
例子：
- 正则表达式：if|[_a-zA-Z][_0-9a-zA-Z]*
- NFA：
- 起始状态: { INIT, A, G }
  i: { INIT, A, G } $\to$ { B, C, D, E, F, H, I, K }
  f: { B, C, D, E, F, H, I, K } $\to$ { D, E, F, J, K }
  _0-9a-zA-Z: { D, E, F, J, K } $\to$ { D, E, F, K }
  _0-9a-zA-Z: { D, E, F, K } $\to$ { D, E, F, K }
  _0-9a-eg-zA-Z: { B, C, D, E, F, H, I, K } $\to$ { D, E, F, K }
  _a-hj-zA-Z: { INIT, A, G } $\to$ { B, C, D, E, F, K }
  _0-9a-zA-Z: { B, C, D, E, F, K } $\to$ { D, E, F, K }
- 构造生成的 DFA：

Lecture 2：语法分析

Lecture 3：简单编译器

Lecture 4：程序语言语法的 Coq 定义

Lecture 5：表达式指称语义

Lecture 6：利用集合与关系定义指称语义

Lecture 7：霍尔逻辑

Lecture 8：用单子表示计算

1. 单子的定义

假设 $M$ 是一个单子， $M(A)$ 是一个集合，表示一类计算结果（或返回值）类型为 $A$ 的计算
$M$ $M$ 单子应配有两个算子：
- bind 算子：表示计算的复合，即 bind： $\forall A B . M(A) \rightarrow(A \rightarrow M(B)) \rightarrow M(B)$
- return 算子：表示直接返回一个特定值，即 return： $\forall A . A \rightarrow M(A)$

Class Monad (M：Type -> Type)：Type := {
  bind：forall {A B：Type}, M A -> (A -> M B) -> M B;
  ret：forall {A：Type}, A -> M A;
}.

Lecture 9：不动点定理

Lecture 10：单子程序上的霍尔逻辑

Lecture 11：分离逻辑

基本概念

考虑 WhileDeref 语言中有关内存地址的读写，需要新的程序逻辑推理规则。

断言 $P * Q$ 表示：可以将程序状态中的内存拆分成为互不相交的两部分，其一满足 $P$ 另一个满足 $Q$ ；
即，程序状态 $s$ 满足性质 $P * Q$ 当且仅当存在 $s_1$ 与 $s_2$ 使得：
– $s_1$ 满足 $P$ ，
– $s_2$ 满足 $Q$ ，
– $s.\text{vars} = s_1.\text{vars} = s_2.\text{vars}$ 并且 $s.\text{mem} = s_1.\text{mem} \uplus s_2.\text{mem}$
简写为 $s_1 \oplus s_2 \Downarrow s$ ，
$P * Q$ 中的星号称为分离合取

例如：

* x == m && * y == n && x != y 可以写作 store(x, m) * store(y, n)
* * x == 0 && * x != x 可以写作 exists u. store(x, u) * store(u, 0)

这里，我们使用 $\mathrm{store}(a, b)$ 表示地址 $a$ 上存储了 $b$ 这个值，并且仅仅拥有此内存权限。

下面是一些霍尔三元组的例子：

1
2
3

{ store(0x40, 0) }
* 0x40 = 0x80
{ store(0x40, 0x80) }

1
2
3

{ store(0x40, 0) * store(0x80, 0) }
* 0x40 = 0x80
{ store(0x40, 0x80) * store(0x80, 0) }

假设 $0 \le m \le 100$ ，

1
2
3

{ store(x, m) * store(y, n) }
* x = * x + 1
{ store(x, m + 1) * store(y, n) }

1
2
3

{ store(x, m) * store(y, n) }
* x = * y
{ store(x, n) * store(y, n) }

直观上，断言 $P * Q * R$ 表示：可以将程序状态中的内存拆分成为互不相交的三部分，分别满足 $P$ 、 $Q$ 与 $R$ 。容易发现， $*$ 具有交换律和结合律。

1 2	`* x == n && * y == m && * z == 0 && x != y && y != z && z != x`

可以写作：store(x, n) * store(y, m) * store(z, 0)

1
2
3

* x == 10 && * (x + 8) == u &&
* u == 100 && * (u + 8) == 0 &&
x != u && x + 8 != u && x - 8 != u

可以写作：store(x, 10) * store(x + 8, u) * store(u, 100) * store(u + 8, 0)，这其实是一个长度为 2 的链表

以下霍尔三元组成立：

1
2
3

{ store(x, 10) * store(x + 8, u) * store(u, n) }
* x = * * (x + 8)
{ store(x, n) * store(x + 8, u) * store(u, n) }

霍尔逻辑规则

内存赋值规则（正向）

如果 $P$ 能推出
– $e_1$ 能够安全求值并且求值结果为 $a$
– $e_2$ 能够安全求值并且求值结果为 $b$
– $\exists u. \mathrm{store}(a, u) * Q$
那么 $\{P\} \, * e_1 = e_2 \, \{\mathrm{store}(a, b) * Q\}$
其中 $a$ 与 $b$ 都是与内存无关的数学式子

变量赋值规则（正向）

如果 $P$ 能推出 $e$ 能够安全求值并且求值结果为 $a$
那么 $\{P\} \, x=e \, \left\{\exists x^{\prime} . a\left[x \mapsto x^{\prime}\right]=x \, \& \& \, P\left[x \mapsto x^{\prime}\right]\right\}$
其中 $a$ 是与内存无关的数学式子

框架规则

如果 $F$ 中不出现被 $c$ 赋值的变量，并且 $\{P\} \, c \, \{Q\}$
那么 $\{P * F\} \, c \, \{Q * F\}$

存在量词规则

如果对于任意 $a$ 都有，并且 $\{P(a)\} \, c \, \{Q\}$
那么 $\{\exists a, P (a)\} \, c \, \{Q\}$

例子 - 交换地址上的值

{ store(x, m) * store(y, n) }
  t = * x;
  * x = * y;
  * y = t
{ store(x, n) * store(y, m) }

例子 - 单链表取反

下面程序描述了单链表取反的过程。

while (x != 0) do {
  t = x;
  x = * (x + 8);
  * (t + 8) = y;
  y = t
}

`sll(p)` 谓词的定义

利用分离逻辑，我们可以定义一些新的谓词，从而简洁描述数据结构。以单链表为例：

谓词 sll(p) 表示以 p 地址为头指针存储了一个单链表，定义为：

1 2	`p == 0 && emp \|\| exists u q, store(p, u) * store(p + 8, q) * sll(q)`

其中 emp 表示占据空内存。

利用 sll(p) 谓词，可以如下描述单链表取反程序的内存安全性性质：

{ y == 0 && sll(x) }
while (x != 0) do {
  t = x;
  x = * (x + 8);
  * (t + 8) = y;
  y = t
}
{ x == 0 && sll(y) }

循环不变量的验证

可以选用 sll(x) * sll(y) 作为循环不变量。

首先，前条件可以推出循环不变量。

    y == 0 && sll(x)
|-- y == 0 && emp * sll(x)
|-- (y == 0 && emp) * sll(x)
|-- sll(y) * sll(x)
|-- sll(x) * sll(y).

其次，循环体能保持循环不变量。

{ x != 0 && sll(x) * sll(y) }
{ exists u z, store(x, u) * store(x + 8, z) * sll(z) * sll(y) }
  // Given u z,
{ store(x, u) * store(x + 8, z) * sll(z) * sll(y) }
  t = x;
{ t == x && store(x, u) * store(x + 8, z) * sll(z) * sll(y) }
  x = * (x + 8);
{ exists x', x == z && t == x' && store(x', u) * store(x' + 8, z) * sll(z) * sll(y) }
{ x == z && store(t, u) * store(t + 8, z) * sll(z) * sll(y) }
  * (t + 8) = y;
{ x == z && store(t, u) * store(t + 8, y) * sll(z) * sll(y) }
  y = t
{ exists y', y == t && x == z && store(t, u) * store(t + 8, y') * sll(z) * sll(y') }
{ exists y', store(y, u) * store(y + 8, y') * sll(x) * sll(y') }
{ sll(x) * sll(y) }

最后，退出循环时后条件成立。

1
2
3

    !(x != 0) && sll(x) * sll(y)
|-- (x == 0) && sll(x) * sll(y)
|-- (x == 0) && sll(y).

例子 - 单链表的连接 1

下面程序描述了单链表的连接。

//@ require sll(x) * sll(y)
//@ ensure sll(res)
if (x == 0)
then {
  res = y
}
else {
  res = x;
  nx = * (x + 8);
  while (nx != 0) do {
    x = nx;
    nx = * (x + 8)
  };
  * (x + 8) = y
}

`sllseg(p, q)` 谓词的定义

用谓词 sllseg(p, q) 表示以 p 地址为头指针开始到 q 为止是单链表中的一段（注意不包含 q），定义为：

1 2	`p == q && emp \|\| exists u r, store(p, u) * store(p + 8, r) * sllseg(r, q)`

循环不变量的验证

//@ require sll(x) * sll(y)
//@ ensure sll(res)
if (x == 0)
then { res = y }
else {
  res = x;
  nx = * (x + 8);
  //@ [generated] v == nx && x == res && store(x, u) *
  store(x + 8, v) * sll(v) * sll(y)
  //@ inv exists u, sllseg(res, x) * store(x, u) *
  store(x + 8, nx) * sll(nx) * sll(y)
  while (nx != 0) do {
    x = nx;
    nx = * (x + 8)
  };
  * (x + 8) = y
}

例子 - 单链表的连接 2

下面是用二阶指针实现的单链表连接。

{ exists u, store(phead , u) * sll(x) * sll(y) }
  * phead = x;
  pt = phead;
  while ( * pt != 0) {
    pt = * pt + 8;
  };
  * pt = y;
  res = * phead
{ exists u, store(phead , u) * sll(res) }

`SllSeg(p, q)` 谓词的定义

1 2	`p == q && emp \|\| exists u r, store(p, r) * store(r, u) * SllSeg(r + 8, q)`

参考资料

本文参考上海交通大学程序语言与编译原理课程 CS2612 曹钦翔老师的讲义，课程网站为 https://jhc.sjtu.edu.cn/public/courses/CS2612/。

程序语言与编译原理

#课程笔记 #知识点整理 #程序语言 #编译原理

程序语言与编译原理：期末复习

https://cny123222.github.io/2025/11/26/程序语言与编译原理：期末复习/

Author

Nuoyan Chen

Posted on

November 26, 2025

Licensed under

数字图像处理(6)：图像压缩 Previous

数字图像处理(5)：图像复原 Next

程序语言与编译原理：期末复习

Lecture 1：词法分析

1. 词法分析的基本知识

2. 正则表达式 (Regular Expression)

3. Flex 词法分析工具

4. 有限状态自动机

5. 将正则表达式转化为 NFA

6. 将 NFA 转化为 DFA

Lecture 2：语法分析

Lecture 3：简单编译器

Lecture 4：程序语言语法的 Coq 定义

Lecture 5：表达式指称语义

Lecture 6：利用集合与关系定义指称语义

Lecture 7：霍尔逻辑

Lecture 8：用单子表示计算

1. 单子的定义

Lecture 9：不动点定理

Lecture 10：单子程序上的霍尔逻辑

Lecture 11：分离逻辑

基本概念

霍尔逻辑规则

内存赋值规则（正向）

变量赋值规则（正向）

框架规则

存在量词规则

例子 - 交换地址上的值

例子 - 单链表取反

sll(p) 谓词的定义

循环不变量的验证

例子 - 单链表的连接 1

sllseg(p, q) 谓词的定义

循环不变量的验证

例子 - 单链表的连接 2

SllSeg(p, q) 谓词的定义

参考资料

`sll(p)` 谓词的定义

`sllseg(p, q)` 谓词的定义

`SllSeg(p, q)` 谓词的定义