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

Last updated on January 8, 2026 am

本文为 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：语法分析

1. 语法分析的任务

语法分析的主要任务是在词法分析结果的基础上，进一步得到解析树（parsing tree）。

2. 上下文无关语法与解析树

上下文无关语法（Context-Free Grammar，CFG）：是用于描述程序设计语言语法结构的形式化工具，一套 CFG 包含：
- 初始符号 (Start Symbol): 语法的起点，通常表示一个完整的程序或语句，例如 S
- 终结符 (Terminal Symbols) 集合: 构成语言的基本符号，也就是词法分析器生成的标记 (token) 集合，例如 ID NAT , ; ( ) + :=
- 非终结符 (Nonterminal Symbols) 集合: 表示语法结构的变量，可以被进一步展开，例如 S E L
- 产生式 (Productions) 集合: 定义了非终结符如何被展开成终结符或非终结符序列（可以为空）的规则
  - 格式为 A -> β，其中 A 是一个非终结符，β 是一个符号序列

S -> S ; S              E -> ID             L -> E
S -> ID := E            E -> NAT            L -> L , E
S -> PRINT ( L )        E -> E + E
                        E -> ( E )

派生 (Derivation): 从初始符号开始，反复应用产生式，将非终结符替换为其产生式的右侧，最终得到一个只包含终结符的序列，这个过程称为派生

S -> S; S
  -> ID := E; S
  -> ID := E + E; S
  -> ID := ID + E; S
  -> ID := ID + NAT; S
  -> ID := ID + NAT; PRINT(L)
  -> ID := ID + NAT; PRINT(L, E)
  -> ID := ID + NAT; PRINT(E, E)
  -> ID := ID + NAT; PRINT(ID, E)
  -> ID := ID + NAT; PRINT(ID, ID)

解析树 (Parsing Tree): 是派生过程的图形化表示，它具有以下性质：
- 根节点是语法的初始符号
- 每个内部节点是一个非终结符，每个叶子节点是一个终结符
- 每一个父节点和它的所有子节点共同对应一条产生式规则

         E
      /  |  \                   E
    E    *    E                 -> E * E
  / | \       |                 -> E + E * E
 E  +  E      ID                -> ID + E * E
 |     |                        -> ID + ID * E
ID     ID                       -> ID + ID * ID

3. 歧义与歧义的消除

定义: 如果一个文法对于某个特定的标记串可以产生两棵或更多不同的解析树，那么这个文法就是有歧义的 (ambiguous)
- 问题: 歧义会导致一个程序的含义不确定，因为不同的解析树可能对应不同的执行逻辑
常见的歧义类型：优先级歧义、结合性歧义
消除歧义的方法: 通过引入新的非终结符和产生式来强制规定优先级 (precedence) 和结合性 (associativity)

例子：下面上下文无关语法有歧义

1	`E -> ID E -> E + E E -> E * E E -> ( E )`

歧义1：加法和乘法的优先级

    E                      E
  / | \                  / | \
 E  +  E                E  *  E
 |   / | \            / | \   |
ID  E  *  E          E  +  E  ID
    |     |          |     |
   ID     ID        ID     ID

为了消除该歧义，引入了新的非终结符 F，并将文法改写为：

1 2	`E -> F E -> E + E F -> F * F F -> ( E ) F -> ID`

这时，加法的因子 E 可以继续展开产生乘法，但乘法的因子 F 无法再展开产生加法，从而规定了乘法的优先级高于加法。

    E                    
  / | \                  E 
 E  +  E                 -> E + E     
 |     |                 -> E + F
 F     F                 -> E + F * F
 |   / | \               -> E + F * ID
ID  F  *  F              -> E + ID * ID
    |     |              -> F + ID * ID
   ID     ID             -> ID + ID * ID

歧义2：加法的结合律 / 乘法的结合律

    E                     E  
  / | \                 / | \   
 E  +  E               E  +  E   
 |   / | \           / | \   |
 F  E  +  E         E  +  E  F     
 |  |     |         |     |  | 
ID  F     F         F     F  ID
    |     |         |     |    
   ID     ID        ID    ID

为了消除该歧义，再次引入新的非终结符 G，并将文法改写为：

1 2	`E -> F E -> E + F F -> F * G F -> G G -> ( E ) G -> ID`

这时，只有加法左侧的因子 E 能够继续展开产生加法，从而规定了加法是左结合的。乘法同理。

      E                    
    / | \                  E 
   E  +  F                 -> E + F     
 / | \   |                 -> E + F + F
E  +  F  G                 -> F + F + F
|     |  |                 -> G + F + F
F     G  ID                -> ID + F + F
|     |                    -> ID + G + F
G     ID                   -> ID + ID + F
|                          -> ID + ID + G
ID                         -> ID + ID + ID

4. 派生与规约

最左派生 (Left-most Derivation): 在派生的每一步，总是选择最左边的非终结符进行展开
最右派生 (Right-most Derivation): 在派生的每一步，总是选择最右边的非终结符进行展开
唯一性: 同一棵解析树能够唯一确定一种最左派生，同一棵解析树能够唯一确定一种最右派生
- 如果一串标记串没有歧义，那么只有唯一的最左派生可以生成这一标记串，也只有唯一的最右派生可以生成这一标记串
规约 (Reduction): 是派生的逆过程，它将一个终结符序列中与某个产生式右部匹配的子串替换成该产生式的左部非终结符
- 最左规约的逆过程恰好是最右派生，最右规约的逆过程恰好是最左派生

例子：最左规约与最右派生

   ID + ID + ID                            E -> E + F
-> G + ID + ID                               -> E + G
-> F + ID + ID                               -> E + ID
-> E + ID + ID                               -> E + F + ID
-> E + G + ID                                -> E + G + ID
-> E + F + ID                                -> E + ID + ID
-> E + ID                                    -> F + ID + ID
-> E + G                                     -> G + ID + ID
-> E + F                                     -> ID + ID + ID
-> E

5. 移入规约分析

思想: 这是最常见的自底向上分析方法
- 它从左到右扫描输入的标记串，从左向右进行规约
- 目标是计算出最左规约（或者说最右派生）

核心操作: 移入 (Shift)、规约 (Reduce)

扫描线的右侧全部都是终结符
规约操作都发生在扫描线的左侧紧贴扫描线的区域内

   | ID + ID + ID
-> ID | + ID + ID
-> G | + ID + ID
-> F | + ID + ID
-> E | + ID + ID
-> E + | ID + ID
-> E + ID | + ID
-> E + G | + ID
-> E + F | + ID
-> E | + ID
-> E + | ID
-> E + ID |
-> E + G |
-> E + F |
-> E |

移入与规约的选择问题:
- 既能移入，又能规约的情形，应当选择移入还是规约？
- 有多种规约方案的情形，应当如何选择？

6. 已移入部分的结构

这部分在探讨扫描线左侧的可行结构，这有助于我们解决“移入与规约的选择问题”。

已移入部分的结构特征:
- 已移入规约的部分可以分为 $n$ 段，每段对应一条产生式
- 第 $i$ 段拼接上第 $i + 1$ 条产生式的左侧非终结符是第 $i$ 条产生式右侧符号串的一个前缀
例子:
- F * (E) | 中已移入规约的部分可以分为： F * ( E )
- 分别对应产生式：E -> . F F -> F * . G G -> ( E ) .
- F * (E + | ID ) 中已移入规约的部分可以分为： F * ( E +
- 分别对应产生式：E -> . F F -> F * . G G -> ( . E ) E -> E + . F

7. 已移入部分的结构判定

这部分提出了判定可行的扫描线左侧结构的算法，是用于解决“移入与规约的选择问题”的一个判断方法。

核心思想: 以扫描线左侧的最右段为状态，构建 NFA，该 NFA 中的所有状态都是终止状态
- 新增一段带来的变化对应一条 $\epsilon$ 边，其他加入符号带来的变化对应一条普通边
- 要判断一串符号串是否是可行的扫描线左侧结构，只需判断这个符号串能否被这个 NFA 接受
状态转移:
- 普通转移: 当从一个状态 S 读入一个符号 X 时，它会转移到一个新的状态 S'
  - S' 中的项是 S 中形如 A -> α . X β 的项将点右移一位后得到的结果，即 A -> α X . β
- $\epsilon$ -转移: 在一个状态中，如果存在一个项 A -> α . B β（其中 B 是非终结符），那么必须为接下来可能出现的 B 做好准备
  - 因此，所有 B 的产生式对应的初始项，如 B -> . γ，都必须被递归地加入到当前状态中
判定过程:
- 从包含初始产生式 START -> . E 的初始状态开始
- 每次移入一个符号，就根据状态转移规则进入下一个状态
- 如果某一步无法找到合法的转移，说明输入的符号串不可行

例子：判断 E + F + | ... 是否是可行的扫描线左侧结构：

E + F + | ...

[]
START -> . E
    E -> . F
    E -> . E + F
    F -> . G
    F -> . F * G
    G -> . ( E )
    G -> . ID

E + F + | ...

[E]
START -> E .
    E -> E . + F

E + F + | ...

[E +]
E -> E + . F
F -> . G
F -> . F * G
G -> . ID
G -> . ( E )

E + F + | ...

[E + F]
E -> E + F .
F -> F . * G

E + F + | ...

[E + F +]
( No possible state )

8. 基于 follow 集合的判定法

这部分用于解决“移入与规约的选择问题”的另一个判断方法。

定义: 假设 X 是一个终结符，
- X 是 Follow( Y ) 的元素当且仅当 ... Y X ... 是可能被完全规约的
- X 是 First( Y ) 的元素当且仅当 X ... 是可能被规约为 Y 的
First 集合的计算:
- 对任意终结符 X ， X 都是 First( X ) 的元素
- 对任意产生式 Y -> Z ... ，First( Z ) 的元素都是 First( Y ) 的元素
Follow 集合的计算:
- 对任意产生式 U -> ... Y Z ... ，First( Z ) 是 Follow( Y ) 的子集
- 对任意产生式 Z -> ... Y ，Follow( Z ) 是 Follow( Y ) 的子集

9. 移入规约分析完整过程实例

ID * (ID + ID) 的移入规约分析：

初始： | ID * ( ID + ID )
移入： ID | * ( ID + ID )
规约： G | * ( ID + ID ) ，因为 ID * | ... 不可行
规约： F | * ( ID + ID ) ，因为 G * | ... 不可行
移入： F * | ( ID + ID ) ，因为 * 不是 Follow( E ) 中的元素
移入： F * ( | ID + ID )
移入： F * ( ID | + ID )
规约： F * ( G | + ID ) ，因为 F * ( ID + | ... 不可行
规约： F * ( F | + ID ) ，因为 F * ( G + | ... 不可行
规约： F * ( E | + ID ) ，因为 F * ( F + | ... 不可行
移入： F * ( E + | ID )
移入： F * ( E + ID | )
规约： F * ( E + G | ) ，因为 F * ( E + ID ) | ... 不可行
规约： F * ( E + F | ) ，因为 F * ( E + G ) | ... 不可行
规约： F * ( E | ) ，因为另外两种方案扫描线左侧的结构都不可行
移入： F * ( E ) |
规约： F * G |
规约： F |，因为 F * F | ... 不可行
规约： E | ，亦可看做 E | EOF
移入： E EOF |
规约： START |
语法分析结束

10. 冲突

移入/规约冲突（shift/reduce conflict）: 在同一时刻既能进行移入操作，又能进行规约操作
规约/规约冲突（reduce/reduce conflict）: 在同一时刻能进行两种不同的规约操作
歧义与冲突的关系: 给定一套上下文无关语法，如果移入规约分析中，一定不会出现移入/规约冲突，也不会出现规约/规约冲突，那么任何一串标记串都不会有歧义；反之不一定。
- 没有冲突 -> 没有歧义
- 有歧义 -> 有冲突
例子: 考虑 U V W | X Y，存在规约/规约冲突，但该语法没有歧义
1
2
A -> B X Y A -> C X Z B -> U V W C -> U V W

11. Bison 语法分析器

Bison 是一个语法分析器生成器，可以语法分析规则生成 C 语言的语法分析器。

输入（.y 文件）：基于上下文无关语法与优先级、结合性的语法分析规则
输出（.c 文件）：用 C 语言实现的基于移入规约分析算法的语法分析器

lang.y:

文件头: 描述语法分析器所需的头文件、全局变量以及函数
1
2
3
4
5
6
7
8
%{ #include <stdio.h> #include "lang.h" #include "lexer.h" int yyerror(char * str); int yylex(); struct cmd * root; %}
- 其中 yylex() 是 Flex 词法分析器提供的函数
- yyerror(str) 是处理语法错误的必要设定
- root 是语法分析最后生成的语法树根节点
语法分析结果在 C 中的存储: 描述多种语法结构产生对应的语法分析结果
1
2
3
4
5
6
7
%union { unsigned int n; char * i; struct expr * e; struct cmd * c; void * none; }
- n 表示自然数常数的词法语法分析结果
- i 表示变量的词法语法分析结果
- e 表示表达式的语法分析结果
- c 表示程序语句的语法分析结果

终结符与非终结符:

%token <n> TM_NAT
%token <i> TM_IDENT
%token <none> TM_LEFT_BRACE TM_RIGHT_BRACE
%token <none> TM_LEFT_PAREN TM_RIGHT_PAREN
%token <none> TM_MALLOC TM_RI TM_RC TM_WI TM_WC
%token <none> TM_VAR TM_IF TM_THEN TM_ELSE TM_WHILE TM_DO
%token <none> TM_SEMICOL TM_ASGNOP TM_OR TM_AND TM_NOT
%token <none> TM_LT TM_LE TM_GT TM_GE TM_EQ TM_NE
%token <none> TM_PLUS TM_MINUS TM_MUL TM_DIV TM_MOD
%type <c> NT_WHOLE NT_CMD
%type <e> NT_EXPR

%token 表示终结符， %type 表示非终结符
尖括号内表示语义值的存储方式

优先级与结合性:

%nonassoc TM_ASGNOP
%left TM_OR
%left TM_AND
%left TM_LT TM_LE TM_GT TM_GE TM_EQ TM_NE
%left TM_PLUS TM_MINUS
%left TM_MUL TM_DIV TM_MOD
%left TM_NOT
%left TM_LEFT_PAREN TM_RIGHT_PAREN
%right TM_SEMICOL

越先出现优先级越低
同一行声明内的优先级相同

上下文无关语法:

%%
NT_WHOLE:
  NT_CMD {
    $$ = ($1);
    root = $$;
  }
;

所有词法分析规则都放在一组 %% 中
第一条语法分析规则描述初始符号对应的产生式
用 $$ 表示产生式左侧符号的语义值
用 $1、$2 等表示产生式右侧符号的语义值

NT_EXPR:
  TM_NAT {
    $$ = (TConst($1));
  }
  | TM_LEFT_PAREN NT_EXPR TM_RIGHT_PAREN {
    $$ = ($2);
  }
  | TM_MINUS NT_EXPR {
    $$ = (TUnOp(T_UMINUS,$2));
  }
  | NT_EXPR TM_PLUS NT_EXPR {
    $$ = (TBinOp(T_PLUS,$1,$3));
  }
  | NT_EXPR TM_MINUS NT_EXPR {
    $$ = (TBinOp(T_MINUS,$1,$3));
}
...

Lecture 3：简单编译器

这部分介绍编译器后端，即如何将程序的语法树转化为汇编代码。

1. 拆分复合表达式

关键点 1：每个赋值语句至多进行一步计算
关键点 2：转化后的程序仅在必要处保留树结构
- 顺序执行的语句可以用链表存储

关键点 3：要妥善处理 while 循环条件的计算语句

在 AST 中，while 循环条件是一个表达式
但经过拆分后，这个表达式的计算将会变为一段程序语句以及一个表达式
- 拆分前
1
x + y + z < 10
- 拆分后
1
2
#0 = x + y; #1 = #0 + z
1
#1 < 10

If 语句的处理方法：

拆分前

1
2
3

if (old_condition)
then { ... }
else { ... }

拆分后

...
(some computation)
...
if (new_condition)
then { ... }
else { ... }

While 语句的处理方法：

拆分前

while (old_condition) do {
  ...
  (old loop body)
  ...
}

拆分后

LABEL_1:
  ...
  (some computation)
  ...
  if (! new_condition) then jmp LABEL_2
  ...
  (new loop body)
  ...
  jmp LABEL1
LABEL_2:
  ...

关键点 4：要妥善处理短路求值

由于短路求值的存在，and 与 or 必须转化为 if 语句

拆分前

1
2
3

if (p && * p != 0)
then { ... }
else { ... }

拆分后

if (!p)
then { #1 = p }
else { #2 = * p;
       #1 = (#2 != 0) };
if (#1)
then { ... }
else { ... }

2. 生成基本块

整体框架：遍历程序语句链表，遇到分支或循环语句时创建新基本块

3. 寄存器分配

这部分只考虑最简单的寄存器分配，即每个变量对应一个寄存器，多个变量可能对应相同的寄存器。

3.1 活性分析

计算方法：

\begin{gathered} \operatorname{in}(u)=(\operatorname{out}(u) \backslash \operatorname{def}(u)) \cup \operatorname{use}(u) \\ \operatorname{out}(u)=\bigcup_{u \rightarrow v} \operatorname{in}(v) \end{gathered}

生成 Interference Graph：如果存在一个 $u$ 使得 $x, y \in \operatorname{in}(u)$ ，那么就在 $x$ 与 $y$ 之间连一条边，表示它们不能分配同一个寄存器

3.2 简单寄存器分配算法

假设共有 $K$ 个寄存器；

步骤一，Simplify：在 Interference Graph 中删除度数不超过 $K - 1$ 的节点，删除的节点用栈记录
步骤二，Spill：如果无法 Simplify，就任意删除一个节点，再回到前面步骤一
步骤三，Select：按照删除节点的倒序为所有变量分配寄存器；
- Simplify 删除的节点能够保证被分配到与 Interference Graph 上相邻节点不冲突的寄存器
- Spill 变量可能可以分配到寄存器（假 Spill），也可能无法分配到寄存器（真 Spill），此时应当存储在内存中
步骤四，Start over：如果有至少一个节点无法分配到寄存器，则改写相关代码并重做 liveness 分析与上述所有步骤

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

1. 一个极简的指令式程序语言：SimpleWhile

SimpleWhile 语言的程序表达式：

整数类型表达式：只有整数常量、变量、加法、减法与乘法运算

1	`EI :: = N \| V \| EI + EI \| EI - EI \| EI * EI`

Inductive expr_int : Type :=
  | EConst (n: Z): expr_int
  | EVar (x: var_name): expr_int
  | EAdd (e1 e2: expr_int): expr_int
  | ESub (e1 e2: expr_int): expr_int
  | EMul (e1 e2: expr_int): expr_int.

布尔类型表达式：

1	`EB :: = TRUE \| FALSE \| EI < EI \| EB && EB \| ! EB`

Inductive expr_bool: Type :=
  | ETrue: expr_bool
  | EFalse: expr_bool
  | ELt (e1 e2: expr_int): expr_bool
  | EAnd (e1 e2: expr_bool): expr_bool
  | ENot (e: expr_bool): expr_bool.

SimpleWhile 语言的程序语句：

C :: = SKIP |
       V = EI |
       C; C |
       if (EB) then { C } else { C } |
       while (EB) do { C }

Inductive com : Type :=
  | CSkip: com
  | CAsgn (x: var_name) (e: expr_int): com
  | CSeq (c1 c2: com): com
  | CIf (e: expr_bool) (c1 c2: com): com
  | CWhile (e: expr_bool) (c: com): com.

2. 更多的程序语言：While 语言

在许多以 C 语言为代表的常用程序语言中，往往不区分整数类型表达式与布尔类型表达式，同时表达式中也包含更多运算符。

While 语言的程序表达式：

1
2
3

E :: = N | V | -E | E+E | E-E | E*E | E/E | E%E |
       E<E | E<=E | E==E | E!=E | E>=E | E>E |
       E&&E | E||E | !E

Inductive binop : Type :=
  | OOr | OAnd
  | OLt | OLe | OGt | OGe | OEq | ONe
  | OPlus | OMinus | OMul | ODiv | OMod.

Inductive unop : Type :=
  | ONot | ONeg.

Inductive expr : Type :=
  | EConst (n: Z): expr
  | EVar (x: var_name): expr
  | EBinop (op: binop) (e1 e2: expr): expr
  | EUnop (op: unop) (e: expr): expr.

While 语言的程序语句：

C :: = SKIP |
       V = E |
       C; C |
       if (E) then { C } else { C } |
       while (E) do { C }

Inductive com : Type :=
  | CSkip: com
  | CAsgn (x: var_name) (e: expr): com
  | CSeq (c1 c2: com): com
  | CIf (e: expr) (c1 c2: com): com
  | CWhile (e: expr) (c: com): com.

3. 更多的程序语言：WhileDeref

在 While 程序语言中增加取地址上的值 EDeref 操作。

WhileDeref 语言的程序表达式：

Inductive expr : Type :=
  | EConst (n: Z): expr
  | EVar (x: var_name): expr
  | EBinop (op: binop) (e1 e2: expr): expr
  | EUnop (op: unop) (e: expr): expr
  | EDeref (e: expr): expr.

WhileDeref 语言的程序语句：赋值语句分为两种情况

Inductive com : Type :=
  | CSkip: com
  | CAsgnVar (x: var_name) (e: expr): com
  | CAsgnDeref (e1 e2: expr): com
  | CSeq (c1 c2: com): com
  | CIf (e: expr) (c1 c2: com): com
  | CWhile (e: expr) (c: com): com.

4. 更多的程序语言：WhileD

在大多数程序语言中，会同时支持或不支持取地址 EAddrOf 与取地址上的值 EDeref 两类操作，我们在 WhileDeref 语言中再加入取地址操作。

WhileD 语言的程序表达式：

Inductive expr : Type :=
  | EConst (n: Z): expr
  | EVar (x: var_name): expr
  | EBinop (op: binop) (e1 e2: expr): expr
  | EUnop (op: unop) (e: expr): expr
  | EDeref (e: expr): expr
  | EAddrOf (e: expr): expr.

WhileD 语言的程序语句：语法树不变

Inductive com : Type :=
  | CSkip: com
  | CAsgnVar (x: var_name) (e: expr): com
  | CAsgnDeref (e1 e2: expr): com
  | CSeq (c1 c2: com): com
  | CIf (e: expr) (c1 c2: com): com
  | CWhile (e: expr) (c: com): com.

5. 更多的程序语言：WhileDC

在程序语句中增加控制流语句 continue 与 break，并增加多种循环语句。

WhileDC 语言的程序表达式：

Inductive expr : Type :=
  | EConst (n: Z): expr
  | EVar (x: var_name): expr
  | EBinop (op: binop) (e1 e2: expr): expr
  | EUnop (op: unop) (e: expr): expr
  | EDeref (e: expr): expr
  | EAddrOf (e: expr): expr.

WhileDC 语言的程序语句：

Inductive com : Type :=
  | CSkip: com
  | CAsgnVar (x: var_name) (e: expr): com
  | CAsgnDeref (e1 e2: expr): com
  | CSeq (c1 c2: com): com
  | CIf (e: expr) (c1 c2: com): com
  | CWhile (e: expr) (c: com): com
  | CFor (c1: com) (e: expr) (c2: com) (c3: com): com
  | CDoWhile (c: com) (e: expr): com
  | CContinue: com
  | CBreak: com.

6. 更多的程序语言：WhileDL

下面在程序语句中增加局部变量声明。

C :: = skip
       V = E | * E = E |
       C; C |
       if (E) then { C } else { C } |
       while (E) do { C } |
       var V; C

Inductive com : Type :=
  | CSkip: com
  | CAsgnVar (x: var_name) (e: expr): com
  | CAsgnDeref (e1 e2: expr): com
  | CSeq (c1 c2: com): com
  | CIf (e: expr) (c1 c2: com): com
  | CWhile (e: expr) (c: com): com
  | CLocalVar (x: var_name) (c: com): com.

7. 带类型标注的表达式

先定义整数类型，每个整数类型由其所需比特数（ sz ）和其有无符号（ sg ）两部分构成。

1
2
3

Inductive Signedness : Type :=
  | Signed: Signedness
  | Unsigned: Signedness.

1 2	`Inductive IntType : Type := \| Build_IntType (sz: Z) (sg: Signedness): IntType.`

基于此，定义带类型标注的 While 语言表达式。

Inductive expr : Type :=
  | EConst (n: Z) (t: IntType): expr
  | EVar (x: var_name) (t: IntType): expr
  | EBinop (op: binop) (e1 e2: expr) (t: IntType): expr
  | EUnop (op: unop) (e: expr) (t: IntType): expr.

8. 基于语法树递归定义的例子

8.1 表达式中包含的计算次数

下面定义 SimpleWhile 语言中一个整数类型表达式中包含的算数运算数量。

Fixpoint number_of_comp (ei: expr_int): Z :=
  match ei with
  | EAdd e1 e2 =>  number_of_comp e1 + number_of_comp e2 + 1
  | ESub e1 e2 => number_of_comp e1 + number_of_comp e2 + 1
  | EMul e1 e2 => number_of_comp e1 + number_of_comp e2 + 1
  | EVar v => 0
  | EConst n => 0
end.

8.2 带类型表达式的几个基本合法性条件

我们定义表达式中常数的合法性条件，即每个常数都落在其类型规定的范围之内。

首先定义每个整数类型对应的数值范围。

Definition const_in_range (n: Z) (t: IntType): Prop :=
  match t with
  | Build_IntType sz Signed =>
      - Z.pow 2 (sz - 1) <= n < Z.pow 2 (sz - 1)
  | Build_IntType sz Unsigned =>
      0 <= n < Z.pow 2 sz
  end.

接着定义“表达式中所有常数全都满足类型范围要求”的合法性条件。

Fixpoint consts_in_range (e: expr): Prop :=
  match e with
  | EConst n t => const_in_range n t
  | EVar v t => True
  | EBinop op e1 e2 t => consts_in_range e1 /\ consts_in_range e2
  | EUnop op e1 t => consts_in_range e1
  end.

Lecture 5：表达式指称语义

1. SimpleWhile 整数类型表达式的指称语义

程序状态集合： $\mathrm{state} \triangleq \mathrm{var\_name} \rightarrow \mathbb{Z}$

1	`Definition state: Type := var_name -> Z.`

整数类型表达式 $e$ 的行为：定义为 $e$ $e$ 在每个程序状态上的值
- $\llbracket e \rrbracket: \mathrm{state} \to \mathbb{Z}$
- $\llbracket e \rrbracket(s)$ 表示表达式 $e$ 在程序状态 $s$ 上的求值结果

从而有如下的具体定义：

$\llbracket n \rrbracket(s)=n$
$\llbracket x \rrbracket(s)=s(x)$
$\llbracket e_1 + e_2 \rrbracket(s)=\llbracket e_1\rrbracket(s) + \llbracket e_2 \rrbracket(s)$
$\llbracket e_1 - e_2 \rrbracket(s)=\llbracket e_1\rrbracket(s) - \llbracket e_2 \rrbracket(s)$
$\llbracket e_1 * e_2 \rrbracket(s)=\llbracket e_1\rrbracket(s) * \llbracket e_2 \rrbracket(s)$

Fixpoint eval_expr_int (e: expr_int) (s: state) : Z :=
  match e with
  | EConst n => n
  | EVar X => s X
  | EAdd e1 e2 => eval_expr_int e1 s + eval_expr_int e2 s
  | ESub e1 e2 => eval_expr_int e1 s - eval_expr_int e2 s
  | EMul e1 e2 => eval_expr_int e1 s * eval_expr_int e2 s
  end.

2. 定义有符号 64 位运算的表达式语义

在表达式的指称语义中表示表达式求值错误（有符号 64 位整数的运算越界的情况）这一概念，可以将求值结果由“整数”改为“整数或求值失败”。

新指称语义： $\forall e . \quad \llbracket e \rrbracket: \mathrm{state} \rightarrow \mathbb{Z}$
程序状态： $\mathrm{state} \triangleq \mathrm{var\_name} \rightarrow \mathbb{Z}$ ， $s \in \mathrm{state}$ 合法当且仅当 $\forall x .-2^{63} \leqslant s(x) \leqslant 2^{63}-1$

从而之前的具体定义可以改为：

$\llbracket n \rrbracket(s)=n$ ，若 $-2^{63} \leqslant n \leqslant 2^{63}-1$
$\llbracket n \rrbracket(s)=\epsilon$ ，若 $-2^{63} \leqslant n \leqslant 2^{63}-1$ 不成立
$\llbracket x \rrbracket(s)=s(x)$
若 $\llbracket e_1 \rrbracket(s) \neq \epsilon, \llbracket e_2 \rrbracket(s) \neq \epsilon$ 并且 $-2^{63} \leqslant \llbracket e_1 \rrbracket(s)+\llbracket e_2 \rrbracket(s) \leqslant 2^{63}-1$ ，

$\llbracket e_1+e_2 \rrbracket(s)=\llbracket e_1 \rrbracket(s)+\llbracket e_2 \rrbracket(s)$
若否，

$\llbracket e_1+e_2 \rrbracket(s)=\epsilon$

3. 变量初始化与表达式语义

考虑到变量需要初始化的情况，给变量加上一个“未初始化”的状态。

$s \in \mathrm{state}$ $s \in state$ 当且仅当 $s$ $s$ 是这样的一个二元组 $s = (s_\mathrm{status}, s_\mathrm{value})$ $s = (s_{status}, s_{value})$ ，其中
- $s_\mathrm{status}: \mathrm{var\_name} \to \{I, U\}$
- $s_\mathrm{value}: \mathrm{var\_name} \to Z \cup \{\epsilon\}$
$s \in \mathrm{state}$ $s \in state$ 是一个合法状态当且仅当
- $\forall x . \, s_{\text {status}}(x)=\mathrm{I} \Rightarrow-2^{63} \leqslant s_{\text {value }}(x) \leqslant 2^{63}-1$
- $\forall x . \, s_{\text {status}}(x)=\mathrm{U} \Rightarrow s_{\text {value}}(x)=\epsilon$
$\llbracket e \rrbracket: \mathrm{state} \rightarrow \mathbb{Z} \cup\{\epsilon\}$

4. 行为等价

基于整数类型表达式的语义定义 eval_expr_int，我们可以定义整数类型表达式之间的行为等价（亦称语义等价）。

行为等价的定义：两个表达式 $e_1$ 与 $e_2$ 是等价的当且仅当它们在任何程序状态上的求值结果都相同，即

e_1 \equiv e_2 \quad \text { iff. } \quad \forall s . \, \llbracket e_1 \rrbracket(s)=\llbracket e_2 \rrbracket(s)

1 2	`Definition iequiv (e1 e2: expr_int): Prop := forall s, ⟦ e1 ⟧ s = ⟦ e2 ⟧ s.`

5. 行为等价的性质

行为等价是一个等价关系：

自反性： $e \equiv e$
对称性： $e_1 \equiv e_2 \Rightarrow e_2 \equiv e_1$
传递性： $e_1 \equiv e_2 \land e_2 \equiv e_3 \Rightarrow e_1 \equiv e_3$

#[export] Instance iequiv_refl: Reflexive iequiv.
#[export] Instance iequiv_symm: Symmetric iequiv.
#[export] Instance iequiv_trans: Transitive iequiv.
#[export] Instance iequiv_equiv: Equivalence iequiv.

行为等价是一个同余关系：表达式中的加号/减号/乘号能保持行为等价

即对于二元算子 $\oplus \in \{+, -, *\}$ ，若 $e_1 \equiv e_1'$ 且 $e_2 \equiv e_2'$ ，则 $e₁ \oplus e₂ \equiv e₁' ⊕ e₂'$

#[export] Instance EAdd_iequiv_morphism:
  Proper (iequiv ==> iequiv ==> iequiv) EAdd.
#[export] Instance ESub_iequiv_morphism:
  Proper (iequiv ==> iequiv ==> iequiv) ESub.
#[export] Instance EMul_iequiv_morphism:
  Proper (iequiv ==> iequiv ==> iequiv) EMul.

6. 利用高阶函数定义指称语义

本节引入一种更为抽象且结构化的方法来定义指称语义，其核心在于将语义算子定义为高阶函数。

以 $\llbracket e_1 + e_2 \rrbracket (s) = \llbracket e_1 \rrbracket (s) + \llbracket e_2 \rrbracket (s)$ 为例，可以看作是用函数 $\llbracket e_1 \rrbracket$ 和 $\llbracket e_2 \rrbracket$ 定义了函数 $\llbracket e_1 + e_2 \rrbracket$ 。因此，可以将加法运算定义为一个高阶函数。

先定义三个算术运算符对应的语义算子：

Definition add_sem (D1 D2: state -> Z) (s: state): Z :=
  D1 s + D2 s.

Definition sub_sem (D1 D2: state -> Z) (s: state): Z :=
  D1 s - D2 s.

Definition mul_sem (D1 D2: state -> Z) (s: state): Z :=
  D1 s * D2 s.

这意味着整数类型表达式的语义满足下面性质：

$\llbracket e_1 + e_2 \rrbracket = \mathrm{add\_sem}(\llbracket e_1 \rrbracket, \llbracket e_2 \rrbracket)$
$\llbracket e_1 - e_2 \rrbracket = \mathrm{sub\_sem}(\llbracket e_1 \rrbracket, \llbracket e_2 \rrbracket)$
$\llbracket e_1 * e_2 \rrbracket = \mathrm{mul\_sem}(\llbracket e_1 \rrbracket, \llbracket e_2 \rrbracket)$

接着，我们定义常量和变量的语义算子。

Definition const_sem (n: Z): state -> Z :=
  fun s => n.

Definition var_sem (X: var_name): state -> Z :=
  fun s => s X.

利用高阶函数定义的语义算子，我们可以重新定义整数类型表达式的指称语义。

Fixpoint eval_expr_int (e: expr_int): state -> Z :=
  match e with
  | EConst n =>
    const_sem n
  | EVar X =>
    var_sem X
  | EAdd e1 e2 =>
    add_sem (eval_expr_int e1) (eval_expr_int e2)
  | ESub e1 e2 =>
    sub_sem (eval_expr_int e1) (eval_expr_int e2)
  | EMul e1 e2 =>
    mul_sem (eval_expr_int e1) (eval_expr_int e2)
  end.

可以证明，前面定义的三个语义算子都能保持函数等价。

以 add_sem_congr 为例，其含义是：add_sem 的第一个参数做 func_equiv 变换，第二个参数做 func_equiv 变化，其结果也做 func_equiv 变换，即保持函数等价。用数学语言表述，如果以 $f == g$ 表示函数的等价（逐点相等），即 $\forall x, f(x) = g(x)$ ，add_sem_congr 的含义是：若 $⟦ e_1 ⟧ == ⟦ e_1' ⟧$ ， $⟦ e_2 ⟧ == ⟦ e_2' ⟧$ ，那么 $\mathrm{add\_sem}(⟦ e_1 ⟧, ⟦ e_2 ⟧) == \mathrm{add\_sem}(⟦ e_1' ⟧, ⟦ e_2' ⟧)$ ，也就是 $⟦ e_1 + e_2 ⟧ == ⟦ e_1' + e_2' ⟧$ ，这也就是后面的 EAdd_congr。

#[export] Instance add_sem_congr:
  Proper (func_equiv _ _ ==>
          func_equiv _ _ ==>
          func_equiv _ _) add_sem.

#[export] Instance sub_sem_congr:
  Proper (func_equiv _ _ ==>
          func_equiv _ _ ==>
          func_equiv _ _) sub_sem.

#[export] Instance mul_sem_congr:
  Proper (func_equiv _ _ ==>
          func_equiv _ _ ==>
          func_equiv _ _) mul_sem.

最后，证明行为等价是等价关系，以及语法算子能够保持行为等价（即同余性质）。

1
2
3

(* 使用函数相等定义的行为等价 *)
Definition iequiv (e1 e2: expr_int): Prop :=
  (⟦ e1 ⟧ == ⟦ e2 ⟧)%func.

1 2	`(* 行为等价是等价关系 *) #[export] Instance iequiv_equiv: Equivalence iequiv.`

(* 语法算子能够保持行为等价 *)
#[export] Instance EAdd_congr:
  Proper (iequiv ==> iequiv ==> iequiv) EAdd.

#[export] Instance ESub_congr:
  Proper (iequiv ==> iequiv ==> iequiv) ESub.

#[export] Instance EMul_congr:
  Proper (iequiv ==> iequiv ==> iequiv) EMul.

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

1. 布尔表达式的指称语义

对于任意布尔表达式 $e$ ，我们规定它的语义 $\llbracket e \rrbracket$ 是程序状态集合的子集，是所有使得 $e$ 求值为真的程序状态构成的集合。

$\llbracket \mathrm{TRUE} \rrbracket = \mathrm{state}$
$\llbracket \mathrm{FALSE} \rrbracket = \varnothing$
$s \in \llbracket e_1 < e_2 \rrbracket$ 当且仅当 $\llbracket e_1 \rrbracket (s) < \llbracket e_2 \rrbracket (s)$
$\llbracket e_1 \&\& e_2 \rrbracket = \llbracket e_1 \rrbracket \cap \llbracket e_2 \rrbracket$
$\llbracket ! e_1 \rrbracket = \mathrm{state} \setminus \llbracket e_1 \rrbracket$

Definition true_sem: state -> Prop := Sets.full.

Definition false_sem: state -> Prop := ∅.

Definition lt_sem (D1 D2: state -> Z):
  state -> Prop :=
  fun s => D1 s < D2 s.

Definition and_sem (D1 D2: state -> Prop):
  state -> Prop :=
  D1 ∩ D2.

Definition not_sem (D: state -> Prop):
  state -> Prop :=
  Sets.complement D.

从而可以定义布尔表达式的指称语义。

Fixpoint eval_expr_bool (e: expr_bool): state -> Prop :=
  match e with
  | ETrue =>
    true_sem
  | EFalse =>
    false_sem
  | ELt e1 e2 =>
    lt_sem (eval_expr_int e1) (eval_expr_int e2)
  | EAnd e1 e2 =>
    and_sem (eval_expr_bool e1) (eval_expr_bool e2)
  | ENot e1 =>
    not_sem (eval_expr_bool e1)
  end.

与整数类型表达式的行为等价定义一样，我们也可以用函数相等定义布尔表达式行为等价。

1 2	`Definition bequiv (e1 e2: expr_bool): Prop := ⟦ e1 ⟧ == ⟦ e2 ⟧.`

先证明三个语义算子 lt_sem 、 and_sem 与 not_sem 能保持函数等价，再利用函数等价的性质证明布尔表达式行为等价的性质。证明与整数类型表达式类似。

#[export] Instance lt_sem_congr:
  Proper (func_equiv _ _ ==>
          func_equiv _ _ ==>
          Sets.equiv) lt_sem.
        
#[export] Instance and_sem_congr:
  Proper (Sets.equiv ==>
          Sets.equiv ==>
          Sets.equiv) and_sem.

#[export] Instance not_sem_congr:
  Proper (Sets.equiv ==> Sets.equiv) not_sem.

#[export] Instance bequiv_equiv: Equivalence bequiv.

#[export] Instance ELt_congr:
  Proper (iequiv ==> iequiv ==> bequiv) ELt.

#[export] Instance EAnd_congr:
  Proper (bequiv ==> bequiv ==> bequiv) EAnd.

#[export] Instance ENot_congr:
  Proper (bequiv ==> bequiv) ENot.

2. 程序语句的指称语义定义

$(s_1, s_2) \in ⟦ c ⟧$ 当且仅当从 $s_1$ 状态开始执行程序 $c$ 会以程序状态 $s_2$ 终止。

赋值语句

\llbracket x=e \rrbracket=\left\{\left(s_1, s_2\right) \mid s_2(x)=\llbracket e \rrbracket\left(s_1\right) \text {, for any } y \in \text { var\_name, if } x \neq y, s_1(y)=s_2(y)\right\}

Definition asgn_sem
          (X: var_name)
          (D: state -> Z)
          (s1 s2: state): Prop :=
  s2 X = D s1 /\ forall Y, X <> Y -> s2 Y = s1 Y.

空语句

\llbracket \operatorname{skip} \rrbracket=\{(s, s) \mid s \in \text { state }\}

1 2	`Definition skip_sem: state -> state -> Prop := Rels.id.`

顺序执行语句

\llbracket c_1 ; c_2 \rrbracket=\llbracket c_1 \rrbracket \circ \llbracket c_2 \rrbracket=\left\{\left(s_1, s_3\right) \mid\left(s_1, s_2\right) \in \llbracket c_1 \rrbracket,\left(s_2, s_3\right) \in \llbracket c_2 \rrbracket\right\}

1
2
3

Definition seq_sem (D1 D2: state -> state -> Prop):
  state -> state -> Prop :=
  D1 ∘ D2.

条件分支语句

定义 1

\begin{aligned} \llbracket \text { if }(e) \text { then }\left\{c_1\right\} \text { else }\left\{c_2\right\} \rrbracket= & \left(\left\{\left(s_1, s_2\right) \mid s_1 \in \llbracket e \rrbracket\right\} \cap \llbracket c_1 \rrbracket\right) \cup \\ & \left(\left\{\left(s_1, s_2\right) \mid s_1 \notin \llbracket e \rrbracket\right\} \cap \llbracket c_2 \rrbracket\right) \end{aligned}

定义 2

\text { if }(e) \text { then }\left\{c_1\right\} \text { else }\left\{c_2\right\} \rrbracket=\text { test\_true }(\llbracket e \rrbracket) \circ \llbracket c_1 \rrbracket \cup \text { test\_false }(\llbracket e \rrbracket) \circ \llbracket c_2 \rrbracket

其中，

\begin{aligned} & \text { test\_true }(\llbracket e \rrbracket)=\left\{\left(s_1, s_2\right) \mid s_1 \in \llbracket e \rrbracket, s_1=s_2\right\} \\ & \text { test\_false }(\llbracket e \rrbracket)=\left\{\left(s_1, s_2\right) \mid s_1 \notin \llbracket e \rrbracket, s_1=s_2\right\} \end{aligned}

Definition test_true
            (D: state -> Prop):
  state -> state -> Prop :=
  Rels.test D.

Definition test_false
            (D: state -> Prop):
  state -> state -> Prop :=
  Rels.test (Sets.complement D).

Definition if_sem
            (D0: state -> Prop)
            (D1 D2: state -> state -> Prop):
  state -> state -> Prop :=
  (test_true D0 ∘ D1) ∪ (test_false D0 ∘ D2).

循环语句

定义 1： $\operatorname{iterLB}_n(\llbracket e \rrbracket, \llbracket c \rrbracket)$ 表示执行循环体 $n$ 次

\begin{aligned} & \text { iterLB }{ }_0(\llbracket e \rrbracket, \llbracket c \rrbracket)=\text { test\_false }(\llbracket e \rrbracket) \text {; } \\ & \text { iterLB }{ }_{n+1}(\llbracket e \rrbracket, \llbracket c \rrbracket)=\text { test\_true }(\llbracket e \rrbracket) \circ \llbracket c \rrbracket \circ \operatorname{iterLB}_n(\llbracket e \rrbracket, \llbracket c \rrbracket) \text {; } \\ & \llbracket \text { while }(e) \text { do }\{c\} \rrbracket=\bigcup_{n \in \mathbb{N}} \operatorname{iterLB}_n(\llbracket e \rrbracket, \llbracket c \rrbracket) \text {. } \end{aligned}

Fixpoint iterLB
          (D0: state -> Prop)
          (D1: state -> state -> Prop)
          (n: nat):
  state -> state -> Prop :=
  match n with
  | O => test_false D0
  | S n0 => test_true D0 ∘ D1 ∘ iterLB D0 D1 n0
  end.

Definition while_sem
            (D0: state -> Prop)
            (D1: state -> state -> Prop):
  state -> state -> Prop :=
  ⋃ (iterLB D0 D1).

定义 2： $\text { boundedLB }_n(\llbracket e \rrbracket, \llbracket c \rrbracket)$ 表示执行循环体小于 $n$ 次

\begin{aligned} & \text { boundedLB }_0(\llbracket e \rrbracket, \llbracket c \rrbracket)=\varnothing \\ & \text { boundedLB }{ }_{n+1}(\llbracket e \rrbracket, \llbracket c \rrbracket)=\text { test\_true }(\llbracket e \rrbracket) \circ \llbracket c \rrbracket \circ \text { boundedLB }_n(\llbracket e \rrbracket, \llbracket c \rrbracket) \cup \text { test\_false }(\llbracket e \rrbracket) \\ & \llbracket \text { while }(e) \text { do }\{c\} \rrbracket=\bigcup_{n \in \mathbb{N}} \text { boundedLB }_n(\llbracket e \rrbracket, \llbracket c \rrbracket) \end{aligned}

Fixpoint boundedLB
          (D0: state -> Prop)
          (D1: state -> state -> Prop)
          (n: nat):
  state -> state -> Prop :=
  match n with
  | O => H
  | S n0 =>
    (test_true D0 ∘ D1 ∘ boundedLB D0 D1 n0) ∪
    (test_false D0)
  end.

Definition while_sem
            (D0: state -> Prop)
            (D1: state -> state -> Prop):
  state -> state -> Prop :=
  ⋃ (boundedLB D0 D1).

下面是程序语句指称语义的递归定义。

Fixpoint eval_com (c: com): state -> state -> Prop :=
  match c with
  | CSkip =>
    skip_sem
  | CAsgn X e =>
    asgn_sem X (eval_expr_int e)
  | CSeq c1 c2 =>
    seq_sem (eval_com c1) (eval_com c2)
  | CIf e c1 c2 =>
    if_sem (eval_expr_bool e) (eval_com c1) (eval_com c2)
  | CWhile e c1 =>
    while_sem (eval_expr_bool e) (eval_com c1)
  end.

3. 程序语句的行为等价

下面定义程序语句的行为等价。

1 2	`Definition cequiv (c1 c2: com): Prop := ⟦ c1 ⟧ == ⟦ c2 ⟧.`

可以证明，赋值语句、顺序执行、if 语句和 while 语句对应的语义算子 asgn_sem 、seq_sem 、 if_sem 与 while_sem 能由等价的函数及相同的集合计算得到相同的集合。其中，证明 if 语句和 while 语句性质时，需要先证明 test_true 和 test_false 能够由等价的函数计算得到相同的集合。

#[export] Instance asgn_sem_congr:
  Proper (eq ==> func_equiv _ _ ==> Sets.equiv) asgn_sem.

#[export] Instance seq_sem_congr:
  Proper (Sets.equiv ==> Sets.equiv ==> Sets.equiv) seq_sem.

#[export] Instance test_true_congr:
  Proper (Sets.equiv ==> Sets.equiv) test_true.

#[export] Instance test_false_congr:
  Proper (Sets.equiv ==> Sets.equiv) test_false.

#[export] Instance if_sem_congr:
  Proper (Sets.equiv ==>
          Sets.equiv ==>
          Sets.equiv ==>
          Sets.equiv) if_sem.

下面证明 Simplewhile 程序语句行为等价的代数性质。

1 2	`(* 程序语句的行为等价是等价关系 *) #[export] Instance cequiv_equiv: Equivalence cequiv.`

(* 语法算子能保持行为等价 *)
#[export] Instance CAsgn_congr:
  Proper (eq ==> iequiv ==> cequiv) CAsgn.

#[export] Instance CSeq_congr:
  Proper (cequiv ==> cequiv ==> cequiv) CSeq.

#[export] Instance CIf_congr:
  Proper (bequiv ==> cequiv ==> cequiv ==> cequiv) CIf.

更多关于程序行为的有用性质可以使用集合与关系的运算性质完成证明，seq_skip 与 skip_seq 表明了删除顺序执行中多余的空语句不改变程序行为。

Lemma seq_skip:
  forall c, [[ c; skip ]] ~=~ c.

Lemma skip_seq:
  forall c, [[ skip; c ]] ~=~ c.

类似地，seq_assoc 表明顺序执行的结合顺序是不影响程序行为的，因此，所有实际的编程中都不需要在程序开发的过程中额外标明顺序执行的结合方式。

1 2	`Lemma seq_assoc: forall c1 c2 c3, [[ (c1; c2); c3 ]] ~=~ [[ c1; (c2; c3) ]].`

4. 复杂程序语句语义性质的证明

下面证明几条程序语句语义的一般性性质。我们首先可以证明，两种 while 语句语义的定义方式是等价的。

Lemma while_sem1_while_sem2_equiv:
  forall D0 D1,
    WhileSem1.while_sem D0 D1 ==
    WhileSem2.while_sem D0 D1.

还可以证明，boundedLB 是递增的。

1 2	`Theorem boundedLB_inc: forall D0 D1 n m, boundedLB D0 D1 m ⊆ boundedLB D0 D1 (n + m).`

以及 while_sem 能保持集合相等、CWhile 能保持行为等价。

#[export] Instance while_sem_congr:
  Proper (Sets.equiv ==>
          Sets.equiv ==>
          Sets.equiv) while_sem.

#[export] Instance CWhile_congr:
  Proper (bequiv ==> cequiv ==> cequiv) CWhile.

前面提到，while 循环语句的行为也可以描述为：只要循环条件成立，就先执行循环体再重新执行循环。我们可以证明，我们目前定义的程序语义符合这一性质。

1
2
3

Lemma while_unroll1: forall e c,
  [[ while (e) do {c} ]] ~=~
  [[ if (e) then { c; while (e) do {c} } else {skip} ]].

定理： $\llbracket \text{ while } (e) \text{ do } \{c\} \rrbracket= \text{ test\_true } (\llbracket e \rrbracket) \circ \llbracket c \rrbracket \circ \llbracket \text{ while } (e) \text{ do } \{c\} \rrbracket \cup \text{ test\_false } (\llbracket e \rrbracket)$
证明：

\begin{aligned} & \llbracket \text { while }(e) \text { do }\{c\} \rrbracket \\ = & \bigcup_{n \in \mathbb{N}} \text { boundedLB }{ }_n(\llbracket e \rrbracket, \llbracket c \rrbracket) \\ = & \bigcup_{n \in \mathbb{N}} \text { boundedLB }{ }_{n+1}(\llbracket e \rrbracket, \llbracket c \rrbracket) \\ = & \bigcup_{n \in \mathbb{N}}(\text { test\_true }(\llbracket e \rrbracket) \circ \llbracket c \rrbracket \circ \text { boundedLB }(\llbracket e \rrbracket, \llbracket c \rrbracket) \cup \text { test\_false }(\llbracket e \rrbracket)) \\ = & \text { test\_true }(\llbracket e \rrbracket) \circ \llbracket c \rrbracket \circ \bigcup_{n \in \mathbb{N}} \text { boundedLB }_n(\llbracket e \rrbracket, \llbracket c \rrbracket) \cup \text { test\_false }(\llbracket e \rrbracket) \\ = & \text { test\_true }(\llbracket e \rrbracket) \circ \llbracket c \rrbracket \circ \llbracket \text { while }(e) \text { do }\{c\} \rrbracket \cup \text { test\_false }(\llbracket e \rrbracket) \end{aligned}

Lecture 7：霍尔逻辑

1. 霍尔三元组

对于任意程序状态 $s_1$ 与 $s_2$ ，如果 $s_1$ 满足性质 $P$ 并且 $(s_1, s_2) \in ⟦ c ⟧$ ，那么 $s_2$ 满足性质 $Q$ 。这一性质写作 $\{P\} c \{Q\}$ ，称为霍尔三元组， $P$ 称为前条件， $Q$ 称为后条件。

可以理解为，如果程序的起始状态 $s_1$ 满足前条件 $P$ ，那么在程序运行终止的情况下，终止状态 $s_2$ 满足后条件 $Q$ 。

2. 顺序执行规则、空语句规则与条件分支语句规则

顺序执行规则：如果 $\{P\} c_1 \{Q\}$ 并且 $\{Q\} c_2 \{R\}$ ，那么 $\{P\} c_1;c_2 \{R\}$ 。
空语句规则： $\{P\} \text{ skip } \{P\}$
条件分支语句规则：如果 $\{P \&\& e\} c_1 \{Q\}$ 并且 $\{P \&\& !e\} c_2 \{Q\}$ ，那么 $\{P\} \text{ if } (e) \text{ then } \{c_1\} \text{ else } \{c_2\} \{Q\}$ 。

3. While 语句规则与循环不变量

While 语句规则：如果 $\{ P \&\& e \} c \{P\}$ ${P && e} c {P}$ ，那么 $\{P\} \text{ while } (e) \text{ do } \{c\} \{P \&\& !e\}$ ${P} while (e) do {c} {P &&! e}$
- 其中 $P$ 称为循环不变量
循环不变量 $P$ 满足的性质：
- 前条件能推出循环不变量；
- 循环体能保持循环不变量，即 $\{ P \&\& e \} c \{P\}$ ；
- 循环不变量并且循环条件不成立（ $P \&\& !e$ ）能推出后条件

例 1：

{ x == 0 }
while (x < 10) do
{
  x = x + 1
}
{ x == 10 }

循环不变量：x <= 10

例 2：假如

m

与

n

是给定正整数

{ x == m && y == 0 }
while (! (x < n)) do {
  x = x - n;
  y = y + 1
}
{ n * y + x == m && 0 <= x < n }

循环不变量：n * y + x == m && 0 <= x

例 3：假如

m

与

n

是给定正整数

{ x == m }
while (! (x < n)) do {
  x = x - n
}
{ exists y'. n * y' + x = m && 0 <= x < n }

循环不变量：exists y'. n * y' + x = m && x >= 0

例 4：假如

m

与

n

是给定正整数

{ x == m && y == n }
while (! (! (x < 0) && ! (0 < x))) do {
  y = y - 1;
  x = x - 1
}
{ y == n - m }

循环不变量：y - x == n - m

例 5：假如

m

是给定正整数

{ x == m && i == res == 0 }
while (i < x) do {
  res = res + x;
  i = i + 1
}
{ res == m * m }

循环不变量：res == i * m && x == m && i <= m

4. 变量赋值语句规则（正向）与最强后条件

最佳后条件的定义：亦称为最强后条件 (strongest postcondition)
- $\{P\} c \{Q\}$ 成立；
- 如果 $\{P\} c \{Q'\}$ 成立，那么 $Q$ 能推出 $Q'$ 。
变量赋值规则（正向）： $\{P\} x=e\left\{\exists x^{\prime} . e\left[x \mapsto x^{\prime}\right]=x \, \& \& \, P\left[x \mapsto x^{\prime}\right]\right\}$

例子：

1
2
3

{ x == m && y == n }
x = x + y
{ exists x'. x' + y == x && x' == m && y == n }

1
2
3

{ x == m && y == n }
temp = x
{ exists temp'. x == temp && x == m && y == n }

5. 符号执行（正向）与验证条件生成

符号执行的例子：

//@ require true
//@ ensure x == 10
x = 0;
//@ [generated] 0 == x && true
//@ inv x <= 10
while (x < 10) do
{
  //@ [generated] x <= 10 && x < 10
  x = x + 1
  //@ [generated] x' + 1 == x && x' <= 10 && x' < 10
  //@ [target] x <= 10
}
//@ [generated] x <= 10 && !(x < 10)

生成的验证条件：

前条件能推出循环不变量
1
0 == x && true |-- x <= 10

循环体能保持循环不变量

1	`x' + 1 == x && x' <= 10 && x' < 10 \|-- x <= 10`

循环不变量并且循环条件不成立能推出后条件
1
x <= 10 && !(x < 10) |-- x == 10

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)$

1.1 状态单子

状态单子用于表示带存储状态的计算。

定义： $M(A) \triangleq \Sigma \rightarrow \Sigma \times A$
含义：如果 $f \in M(A)$ ， $f(s_1) = (s_2, a)$ 表示从 $s_1$ 状态开始执行计算 $f$ ，那么计算结果是 $a$ ，并且存储状态会被修改为 $s_2$

考虑 $\Sigma = \mathbb{Z}$ 的情况，

$\text{Read}: M(\mathbb{Z})$ 表示从存储空间中读出一个整数 $\operatorname{Read}(s)=(s, s)$
$\text{WriteAndPlus1} : \mathbb{Z} \to M(\mathbb{Z})$ 表示向存储空间中写入一个整数并且将这个整数加一后返回 $\operatorname{WriteAndPlus1}(n)(s)=(n, n+1)$
$\text{ReadAndPlus} : \mathbb{Z} \to M(\mathbb{Z})$ 表示将存储空间中的值加上某个整数后的结果返回 $\operatorname{ReadAndPlus}(n)(s)=(s, n+s)$
$\text{return}$ 算子：如果 $a \in A$ ，那么 $\operatorname{return}(a)(s) = (s, a)$
$\text{bind}$ 算子：如果 $f \in M(A)$ 并且 $g : A \to M(B)$ ，那么 $\text{bind}(f, g) \in M(B)$ ，而且 $\operatorname{bind}(f, g)\left(s_1\right)=\left(s_3, b\right)$ 其中 $f(s_1) = (s_2, a)$ ， $g(a)(s_2) = (s_3, b)$ 。

1.2 集合单子

集合单子用于表示非确定性的计算。

定义： $M(A) \triangleq \mathcal{P}(A)$
含义：如果 $f \in M(A)$ ， $a \in f$ 表示 $f$ 的一个可能计算结果是 $a$
$\text{Any} : \mathcal{P}(A) \to M(A)$ 表示从集合 $A$ 的某个子集中任意选一个元素返回 $a \in \operatorname{Any}(\mathrm{X}) i f f . a \in X$
$\text{return}$ 算子： $\operatorname{return}(a) = \{a\}$
$\text{bind}$ 算子：如果 $f \in M(A)$ 并且 $g : A \to M(B)$ ，那么 $\text{bind}(f, g) \in M(B)$ ，而且 $\operatorname{bind}(f, g)=\{b \mid \exists a . a \in f \text { and } b \in g(a)\}$

1.3 记录时间花费的单子

除了计算结果外，额外记录计算花费的运算次数。

定义： $M(A) \triangleq \mathbb{N} \times A$
含义：如果 $f \in M(A)$ ， $f = (t, a)$ 表示 $f$ 这一计算需要的时间是 $t$ 并且计算结果是 $a$
$\text{return}$ 算子： $\operatorname{return}(a) = (0, a)$
$\text{bind}$ 算子：如果 $f \in M(A)$ 并且 $g : A \to M(B)$ ，那么 $\text{bind}(f, g) \in M(B)$ ，而且 $\operatorname{bind}(f, g)=\left(t_1+t_2, b\right)$ 其中 $f = (t_1, a)$ ， $g(a) = (t_2, b)$ 。

1.4 描述计算异常退出的单子

除了成功执行完成计算外，也可能计算出错异常终止。

定义： $M(A) \triangleq A \cup \{\epsilon\}$
含义：如果 $f \in M(A)$ ，那么 $f \in A$ 表示能够成功完成计算， $f = \epsilon$ 表示计算出错异常终止
$\text{return}$ 算子： $\operatorname{return}(a) = a$
$\text{bind}$ $bind$ 算子：如果 $f \in M(A)$ $f \in M (A)$ 并且 $g : A \to M(B)$ $g : A \to M (B)$ ，那么 $\text{bind}(f, g) \in M(B)$ $bind (f, g) \in M (B)$
- 当 $f = a \in A$ 并且 $g(a) = b \in B$ 时， $\text{bind}(f, g) = b$
- 当 $f = a \in A$ 并且 $g(a) = \epsilon$ 时， $\text{bind}(f, g) = \epsilon$
- 当 $f = \epsilon$ 时， $\text{bind}(f, g) = \epsilon$

2. 在 Coq 中定义单子结构

首先，定义 Monad 的统一定义接口。

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;
}.

接着定义集合单子。

Module SetMonad.

Definition M (A: Type): Type := A -> Prop.

Definition bind: forall (A B: Type) (f: M A) (g: A -> M B), M B :=
  fun (A B: Type) (f: M A) (g: A -> M B) =>
    fun b: B => exists a: A, a ∈ f /\ b ∈ g a.

Definition ret: forall (A: Type) (a: A), M A :=
  fun (A: Type) (a: A) => Sets.singleton a.

End SetMonad.

#[export] Instance set_monad: Monad SetMonad.M := {|
  bind := SetMonad.bind;
  ret := SetMonad.ret;
|}.

还可以定义状态单子。

Module StateMonad.

Definition M (Σ A: Type): Type := Σ -> Σ * A.

Definition bind (Σ: Type):
  forall (A B: Type) (f: M Σ A) (g: A -> M Σ B), M Σ B :=
  fun A B f g s1 =>
    match f s1 with
    | (s2, a) => g a s2
  end.

Definition ret (Σ: Type):
  forall (A: Type) (a: A), M Σ A :=
  fun A a s => (s, a).

End StateMonad.

#[export] Instance state_monad (Σ: Type): Monad (StateMonad.M Σ) := {|
  bind := StateMonad.bind Σ;
  ret := StateMonad.ret Σ;
|}.

3. bind 算子的记号

以下是一些集合单子的例子。

任取一个整数：

1	`Definition any_Z: SetMonad.M Z := Sets.full.`

整数乘二：

1 2	`Definition multi_two: Z -> SetMonad.M Z := fun x => ret (x * 2).`

整数加一：

1 2	`Definition plus_one: Z -> SetMonad.M Z := fun x => ret (x + 1).`

任取整数再乘二：

1 2	`Definition bind_ex0: SetMonad.M Z := bind any_Z multi_two.`

任取整数乘二再加一：

Definition bind_ex1: SetMonad.M Z :=
  bind (bind any_Z multi_two) plus_one.

Definition bind_ex2: SetMonad.M Z :=
  bind any_Z (fun x => bind (multi_two x) plus_one).

下面是用单子描述计算时常用的记号：

1 2	`Notation "x <- c1 ;; c2" := (bind c1 (fun x => c2)) (at level 61, c1 at next level , right associativity) : monad_scope.`

用这些 Notation 可以重写前面的一些例子。

任取整数再乘二：

1 2	`Definition bind_ex0': SetMonad.M Z := x <- any_Z;; ret (x * 2).`

任取整数乘二再加一：

1 2	`Definition bind_ex1 ': SetMonad.M Z := x <- any_Z;; y <- multi_two x;; ret (y + 1).`

等价于

1 2	`bind any_Z (fun x => bind (multi_two x) (fun y => ret (y + 1))).`

例题：写出下面标记背后表达的单子定义

Definition bind_ex2 ': SetMonad.M Z :=
  x <- any_Z;;
  y <- any_Z;;
  z1 <- multi_two y;;
  z2 <- plus_one y;;
  ret (x + y + z1 + z2).

bind any_Z (fun x =>
  bind any_Z (fun y =>
    bind (multi_two y) (fun z1 =>
      bind (plus_one y) (fun z2 =>
        ret (x + y + z1 + z2)))))

4. 集合单子

4.1 集合单子的简单例子

1
2
3

Definition choice {A: Type} (f g: SetMonad.M A):
  SetMonad.M A :=
  f ∪ g.

1
2
3

Definition assume (P: Prop): SetMonad.M unit :=
  fun _ => P.
(* P 为真则返回 unit，P 为假则返回空集 *)

choice 算子和 assume 算子结合使用，可以用来表示条件分支。

Definition compute_abs (z: Z): SetMonad.M Z :=
  choice
    (assume (z >= 0);; ret z)
    (assume (z <= 0);; ret (-z)).

4.2 用集合单子定义表达式指称语义

在整数类型表达式中添加 ANY ：

ANY + 1 表示任取一个整数再加一
ANY * 2 表示任取一个整数再乘二

Inductive expr_int : Type :=
  | EConst (n: Z): expr_int
  | EVar (x: var_name): expr_int
  | EAdd (e1 e2: expr_int): expr_int
  | ESub (e1 e2: expr_int): expr_int
  | EMul (e1 e2: expr_int): expr_int
  | EAny: expr_int.

描述非确定性的表达式指称语义：
- $\llbracket e \rrbracket: \text{state} \rightarrow M(\mathbb{Z})$ ，其中 $M$ 表示集合单子
- $n \in \llbracket e \rrbracket(s)$ 表示 $e$ 在 $s$ 上的求值结果可能是 $n$

下面定义语义算子：

Definition any_sem: state -> SetMonad.M Z :=
  fun s => any_Z.

Definition const_sem (n: Z): state -> SetMonad.M Z :=
  fun s => ret n.

Definition var_sem (X: var_name): state -> SetMonad.M Z :=
  fun s => ret (s X).

Definition add_sem (D1 D2: state -> SetMonad.M Z):
  state -> SetMonad.M Z :=
  fun s =>
    x <- D1 s;; y <- D2 s;; ret (x + y).

Definition sub_sem (D1 D2: state -> SetMonad.M Z):
  state -> SetMonad.M Z :=
  fun s =>
    x <- D1 s;; y <- D2 s;; ret (x - y).

Definition mul_sem (D1 D2: state -> SetMonad.M Z):
  state -> SetMonad.M Z :=
  fun s =>
    x <- D1 s;; y <- D2 s;; ret (x * y).

Fixpoint eval_expr_int (e: expr_int): state -> SetMonad.M Z :=
  match e with
  | EConst n =>
    const_sem n
  | EVar X =>
    var_sem X
  | EAdd e1 e2 =>
    add_sem (eval_expr_int e1) (eval_expr_int e2)
  | ESub e1 e2 =>
    sub_sem (eval_expr_int e1) (eval_expr_int e2)
  | EMul e1 e2 =>
    mul_sem (eval_expr_int e1) (eval_expr_int e2)
  | EAny =>
    any_sem
end.

5. 非确定性 + 计算异常退出

我们同时考虑计算带有非确定性以及异常退出。

5.1 单子定义

Module SetMonadE.

Record M (A: Type): Type := {
  nrm: A -> Prop;
  err: Prop;
}.

Definition ret (A: Type) (a: A): M A := {|
  nrm := Sets.singleton a;
  err := False;
|}.

Definition bind (A B: Type) (f: M A) (g: A -> M B):
  M B :=
  {|
    nrm := fun b => exists a, a ∈ f.(nrm) /\ b ∈ (g a).(nrm);
    err := f.(err) \/ exists a, a ∈ f.(nrm) /\ (g a).(err);
  |}.

End SetMonadE.

#[export] Instance err_monad: Monad SetMonadE.M := {|
  bind := SetMonadE.bind;
  ret := SetMonadE.ret;
|}.

5.2 基本算子与简单示例

Definition abort {A: Type}: SetMonadE.M A :=
  {|
    SetMonadE.nrm := ∅;
    SetMonadE.err := True;
  |}.

Definition assume (P: Prop):
  SetMonadE.M unit :=
  {|
    SetMonadE.nrm := fun _ => P;
    SetMonadE.err := False;
  |}.

Definition assert (P: Prop):
  SetMonadE.M unit :=
  {|
    SetMonadE.nrm := fun _ => P;
    SetMonadE.err := ~ P;
  |}.

Definition choice {A: Type} (f g: SetMonadE.M A):
  SetMonadE.M A :=
  {|
    SetMonadE.nrm := f.(nrm) ∪ g.(nrm);
    SetMonadE.err := f.(err) \/ g.(err);
  |}.

下面是一些简单示例。

Definition compute_abs (z: Z): SetMonadE.M Z :=
  choice
    (assume (z >= 0);; ret z)
    (assume (z <= 0);; ret (-z)).

1
2
3

Definition compute_div (a b: Z): SetMonadE.M Z :=
  assert (b <> 0);;
  ret (a / b).

1
2
3

Definition compute_mod (a b: Z): SetMonadE.M Z :=
  assert (b <> 0);;
  ret (a mod b).

5.3 SimpleWhile 的整数类型表达式指称语义（有符号 64 位计算）

下面定义语义算子。

Definition const_sem (n: Z):
  state -> SetMonadE.M Z :=
  fun s =>
    assert (Int64.min_signed <= n <= Int64.max_signed);;
    ret n.

Definition var_sem (X: var_name):
  state -> SetMonadE.M Z :=
  fun s =>
    ret (s X).

Definition add_sem (D1 D2: state -> SetMonadE.M Z):
  state -> SetMonadE.M Z :=
  fun s =>
    x <- D1 s;; y <- D2 s;;
    assert (Int64.min_signed <= x + y <= Int64.max_signed);;
    ret (x + y).

Definition sub_sem (D1 D2: state -> SetMonadE.M Z):
  state -> SetMonadE.M Z :=
  fun s =>
    x <- D1 s;; y <- D2 s;;
    assert (Int64.min_signed <= x - y <= Int64.max_signed);;
    ret (x - y).

Definition mul_sem (D1 D2: state -> SetMonadE.M Z):
  state -> SetMonadE.M Z :=
  fun s =>
    x <- D1 s;; y <- D2 s;;
    assert (Int64.min_signed <= x * y <= Int64.max_signed);;
    ret (x * y).

Fixpoint eval_expr_int (e: expr_int):
  state -> SetMonadE.M Z :=
  match e with
  | EConst n =>
    const_sem n
  | EVar X =>
    var_sem X
  | EAdd e1 e2 =>
    add_sem (eval_expr_int e1) (eval_expr_int e2)
  | ESub e1 e2 =>
    sub_sem (eval_expr_int e1) (eval_expr_int e2)
  | EMul e1 e2 =>
    mul_sem (eval_expr_int e1) (eval_expr_int e2)
  end.

5.4 SimpleWhile 的整数类型表达式指称语义（考虑变量初始化）

1
2
3

Inductive val: Type :=
  | Var_U: val
  | Var_I (i: Z): val.

这里，如果一个变量的值用 Var_U 表示，那么一个变量没有初始化；如果一个变量的值用 Var_I 表示，那么这个变量已经初始化了。

这样，程序状态就可以如下定义。

1	`Definition state: Type := var_name -> val.`

下面定义语义算子。

Definition var_sem (X: var_name):
  state -> SetMonadE.M Z :=
  fun s =>
    match s X with
    | Var_U => abort
    | Var_I n => ret n
    end.

其他语义算子的定义代码都不需要修改。

Fixpoint eval_expr_int (e: expr_int):
  state -> SetMonadE.M Z :=
  match e with
  | EConst n =>
    const_sem n
  | EVar X =>
    var_sem X
  | EAdd e1 e2 =>
    add_sem (eval_expr_int e1) (eval_expr_int e2)
  | ESub e1 e2 =>
    sub_sem (eval_expr_int e1) (eval_expr_int e2)
  | EMul e1 e2 =>
    mul_sem (eval_expr_int e1) (eval_expr_int e2)
  end.

6. While 语言表达式的指称语义

常量、变量、加、减、乘对应的语义算子都可以沿用先前的定义。下面先定义除法和取余对应的语义算子，具体规定细节参考了 C 标准。

Definition div_sem (D1 D2: state -> SetMonadE.M Z):
  state -> SetMonadE.M Z :=
  fun s =>
    x <- D1 s;; y <- D2 s;;
    assert (y <> 0);;
    assert (y <> -1 \/ x <> Int64.min_signed);;
    ret (Z.quot x y).

Definition mod_sem (D1 D2: state -> SetMonadE.M Z):
  state -> SetMonadE.M Z :=
  fun s =>
    x <- D1 s;; y <- D2 s;;
    assert (y <> 0);;
    assert (y <> -1 \/ x <> Int64.min_signed);;
    ret (Z.rem x y).

C 标准规定：

在任何情况下，整数运算中的 C 表达式 a / b 与 a % b 永远满足 a = b * (a / b) + a % b。
- 同时，如果前者的计算是未定义行为，那么后者的也是。
如果除法运算不整除，那么 a % b 与 a 同号。

下面再定义整数大小比较的语义算子。

Definition eq_sem (D1 D2: state -> SetMonadE.M Z):
  state -> SetMonadE.M Z :=
  fun s =>
    x <- D1 s;; y <- D2 s;;
    choice
      (assume (x = y);; ret 1)
      (assume (x <> y);; ret 0).

Definition neq_sem (D1 D2: state -> SetMonadE.M Z):
  state -> SetMonadE.M Z :=
  fun s =>
    x <- D1 s;; y <- D2 s;;
    choice
      (assume (x <> y);; ret 1)
      (assume (x = y);; ret 0).

Definition lt_sem (D1 D2: state -> SetMonadE.M Z):
  state -> SetMonadE.M Z :=
  fun s =>
    x <- D1 s;; y <- D2 s;;
    choice
      (assume (x < y);; ret 1)
      (assume (x >= y);; ret 0).

Definition le_sem (D1 D2: state -> SetMonadE.M Z):
  state -> SetMonadE.M Z :=
  fun s =>
    x <- D1 s;; y <- D2 s;;
    choice
      (assume (x <= y);; ret 1)
      (assume (x > y);; ret 0).

Definition gt_sem (D1 D2: state -> SetMonadE.M Z):
  state -> SetMonadE.M Z :=
  fun s =>
    x <- D1 s;; y <- D2 s;;
    choice
      (assume (x > y);; ret 1)
      (assume (x <= y);; ret 0).

Definition ge_sem (D1 D2: state -> SetMonadE.M Z):
  state -> SetMonadE.M Z :=
  fun s =>
    x <- D1 s;; y <- D2 s;;
    choice
      (assume (x >= y);; ret 1)
      (assume (x < y);; ret 0).

最后两个语义算子是关于逻辑运算的语义算子。

Definition and_sem (D1 D2: state -> SetMonadE.M Z):
  state -> SetMonadE.M Z :=
  fun s =>
    x <- D1 s;;
    choice
      (assume (x <> 0);;
      y <- D2 s;;
      choice
        (assume (y <> 0);; ret 1)
        (assume (y = 0);; ret 0))
      (assume (x = 0);; ret 0).
(* 这里实现了短路求值 *)

Definition or_sem (D1 D2: state -> SetMonadE.M Z):
  state -> SetMonadE.M Z :=
  fun s =>
    x <- D1 s;;
    choice
      (assume (x <> 0);; ret 1)
      (assume (x = 0);;
      y <- D2 s;;
      choice
        (assume (y <> 0);; ret 1)
        (assume (y = 0);; ret 0)).

除了定义二元运算符的语义算子之外，还有两个一元运算符需要定义其语义算子。

Definition not_sem (D: state -> SetMonadE.M Z):
  state -> SetMonadE.M Z :=
  fun s =>
    x <- D s;;
    choice
      (assume (x <> 0);; ret 0)
      (assume (x = 0);; ret 1).

Definition neg_sem (D: state -> SetMonadE.M Z):
  state -> SetMonadE.M Z :=
  fun s =>
    x <- D s;;
    assert (x <> Int64.min_signed);;
    ret (- x).

将上面这些语义算子集成起来。

Definition binop_sem (op: binop) (D1 D2: state -> SetMonadE.M Z):
  state -> SetMonadE.M Z :=
  match op with
  | OPlus => add_sem D1 D2
  | OMinus => sub_sem D1 D2
  | OMul => mul_sem D1 D2
  | ODiv => div_sem D1 D2
  | OMod => mod_sem D1 D2
  | OLt => lt_sem D1 D2
  | OLe => le_sem D1 D2
  | OGt => gt_sem D1 D2
  | OGe => ge_sem D1 D2
  | OEq => eq_sem D1 D2
  | ONe => neq_sem D1 D2
  | OAnd => and_sem D1 D2
  | OOr => or_sem D1 D2
  end.

Definition unop_sem (op: unop) (D: state -> SetMonadE.M Z):
  state -> SetMonadE.M Z :=
  match op with
  | ONeg => neg_sem D
  | ONot => not_sem D
  end.

最终的递归定义如下。

Fixpoint eval_expr (e: expr): state -> SetMonadE.M Z :=
  match e with
  | EConst n =>
    const_sem n
  | EVar X =>
    var_sem X
  | EBinop op e1 e2 =>
    binop_sem op (eval_expr e1) (eval_expr e2)
  | EUnop op e1 =>
    unop_sem op (eval_expr e1)
  end.

7. WhileDeref 语言表达式的指称语义

我们在 While 语言的基础上引入内存。

首先，每个程序状态 s 中除了包含每个变量的值 s.(var) 还包含内存地址上存储的值 s.(mem) ，这些内存地址是指存储变量数值之外的额外内存存储空间。而对于每个内存地址而言，又要首先定义是否有该地址的读写权限。据此，可以重新定义 var_sem。

Record state: Type := {
  var: var_name -> val; (** 变量的值 *)
  mem: Z -> mem_val;    (** 额 外 内 存 空 间 上 存 储 的 值 *)
}.

Inductive mem_val: Type :=
| Mem_HasPerm (v: val): mem_val (** 有 内 存 读 写 权 限 *)
| Mem_NoPerm: mem_val.          (** 无 内 存 读 写 权 限 *)

Definition var_sem (X: var_name):
  state -> SetMonadE.M Z :=
  fun s =>
    match s.(var) X with
    | Var_U => abort
    | Var_I n => ret n
    end.

接下来定义解引用的语义算子。

Definition deref_sem (D: state -> SetMonadE.M Z):
  state -> SetMonadE.M Z :=
  fun s =>
    x <- D s;;
    match s.(mem) x with
    | Mem_NoPerm => abort
    | Mem_HasPerm Var_U => abort
    | Mem_HasPerm (Var_I n) => ret n
    end.

其他语义算子保持不变。最终的递归定义如下。

Fixpoint eval_expr (e: expr): state -> SetMonadE.M Z :=
  match e with
  | EConst n =>
    const_sem n
  | EVar X =>
    var_sem X
  | EBinop op e1 e2 =>
    binop_sem op (eval_expr e1) (eval_expr e2)
  | EUnop op e1 =>
    unop_sem op (eval_expr e1)
  | EDeref e1 =>
    deref_sem (eval_expr e1)
  end.

Lecture 9：不动点定理

1. 不动点分析

$\llbracket$ while $(e)$ do $\{c\} \rrbracket$ 是下面方程的一个解：

X=\text { test\_true }(\llbracket e \rrbracket) \circ \llbracket c \rrbracket \circ X \cup \text { test\_false }(\llbracket e \rrbracket)

也就是下面函数的一个不动点：

F(X) \triangleq \text { test\_true }(\llbracket e \rrbracket) \circ \llbracket c \rrbracket \circ X \cup \text { test\_false }(\llbracket e \rrbracket)

如果从 $s_1$ 出发执行循环语句 $\text{while }(e) \text{ do } \{c\}$ 会以 $s_2$ 为终止状态结束运行，那么对于任意一个 $F$ 的不动点 $X$ ，都有
- $(s_1, s_2) \in X$
- 不存在其他的 $s$ 使得 $(s_1, s) \in X$
如果从 $s_1$ 出发执行循环语句 $\text{while }(e) \text{ do } \{c\}$ 会在某一次执行循环体的过程中在循环体内部陷入死循环，那么对于任意一个 $F$ 的不动点 $X$ ，都有
- 不存在 $s$ 使得 $(s_1, s) \in X$
如果从 $s_1$ 出发执行循环语句 $\text{while }(e) \text{ do } \{c\}$ 时每一次执行循环体后依次经过程序状态 $s_2, s_3, \dots$ 循行不终止，那么对于任意一个 $F$ 的不动点 $X$ ，以及任意程序状态 $s$ ，都有
- 要么 $(s_1, s),(s_2, s),(s_3, s), \dots$ 全部都是 $X$ 的元素
- 要么 $(s_1, s),(s_2, s),(s_3, s), \dots$ 全部都不是 $X$ 的元素

因此， $F(X)$ 的不动点存在，但不一定唯一。

$\llbracket$ while $(e)$ do $\{c\} \rrbracket$ 可以被定义为 $F(X)$ 的最小不动点。

2. Kleene 不动点定理

下面介绍 Kleene 不动点定理。这将统一的回答为什么有不动点，如何构造最小不动点。

Kleene 不动点定理：任意完备偏序集 $(A, \leqslant_A)$ 上的单调连续函数 $F$ 有不动点，且它的最小不动点是：
$\operatorname{lub}(\perp, F(\perp), F(F(\perp)), \ldots)$
偏序集：
- 定义：满足下面三个条件的 $(A, \leqslant_A)$ $(A, ⩽_{A})$ 成为一个偏序集（partial ordering）：
  - 自反性：对于任意 $a \in A$ ， $a \leqslant_A a$
  - 传递性：对于任意 $a, b, c \in A$ ，如果 $a \leqslant_A b$ 、 $b \leqslant_A c$ ，那么 $a \leqslant_A c$
  - 反对称性：对于任意 $a, b \in A$ ，如果 $a \leqslant_A b$ 、 $b \leqslant_A a$ ，那么 $a = b$
- 例子：
  - $(\mathbb{R}, \leqslant)$ 是一个偏序集。
  - 如果 $D$ 表示自然数之间的整除关系，即 $(a, b) \in D$ 当且仅当 $a | b$ ，那么 $(\mathbb{N}, D)$ 是一个偏序集。值得一提的是，在这个偏序关系下，两个自然数之间不一定可以相互比较；例如 $2 ∤ 3$ 并且 $3 ∤ 2$ 。
  - 如果 $X$ 是一个集合， $\mathcal{P}(X)$ 表示 $X$ 的幂集，那么 $(\mathcal{P}(X), \subseteq)$ 构成一个偏序集。
完备偏序集：
- 定义：如果偏序集 $(A, \leqslant_A)$ $(A, ⩽_{A})$ 还满足下面性质，那么它是一个完备偏序集（complete partial ordering，CPO）：
  - 完备性：对于任意 $S \subseteq A$ ，如果 $S$ 中任意两个元素之间都可以大小比较，那么 $S$ 有上确界（least upper bound, lub），记做 $\operatorname{lub}(S)$ ，即：(1) 对于任意 $a \in S$ ， $a \leqslant_A \operatorname{lub}(S)$ ；(2) 如果某个 $b \in A$ 使得每一个 $a \in S$ 都有 $a \leqslant_A b$ ，那么 $\operatorname{lub}(S) \leqslant_A b$ 。
  - 注：符合上述性质的 $S$ 称为偏序集 $A$ 上的一条链。
- 例子：
  - $(\mathbb{R}, \leqslant)$ 是偏序集但是不是完备偏序集，因为 $\mathbb{Z} \subseteq \mathbb{R}$ 是一条链，但是它没有上确界。
  - 如果 $X$ 是一个集合， $\mathcal{P}(X)$ 表示 $X$ 的幂集，那么 $(\mathcal{P}(X), \subseteq)$ 是一个完备偏序集。其中，对于任意 $U \subseteq \mathcal{P}(X)$ ，都有 $\operatorname{lub}(U)=\bigcup_{V \in U} V$ 是 $U$ 的上确界。
  - 如果 $D$ 表示自然数之间的整除关系，即 $(a, b) \in D$ 当且仅当 $a | b$ ，那么 $(\mathbb{N}, D)$ 是一个完备偏序集。特别的，如果 $U \subseteq \mathbb{N}$ 是一条链还是一个有穷集，那么 $\operatorname{lub}(U)$ 就是 $U$ 的最小公倍数；如果 $U \subseteq \mathbb{N}$ 是一条链还是一个无穷集，那么 $\operatorname{lub}(U)$ 就是 $0$ 。
  - 如果 $D^+$ 表示正整数之间的整除关系，那么 $\left(\mathbb{Z}^{+}, D^{+}\right)$ 是一个偏序集，但不是一个完备偏序集。例如， $\left\{1,2,4,8, \ldots, 2^n, \ldots\right\}$ 是整除关系上的一条链，但是它没有整除关系意义下的上确界。
单调函数：如果 $(A, \leqslant_A)$ 是一个偏序集，那么 $F : A \to A$ 是一个单调函数当且仅当：对于任意 $a, b \in A$ ，如果 $a \leqslant_A b$ ，那么 $F(a) \leqslant_A F(b)$ 。
引理：如果 $S$ 是偏序集 $(A, \leqslant_A)$ 上的一条链， $F : A \to A$ 是一个单调函数，那么 $F(S) \triangleq \{F(a) | a \in S\}$ 也是一条链。
- 证明：任给 $a, b \in S$ ，要么 $a \leqslant_A b$ ，要么 $b \leqslant_A a$ 。若前者成立，那么 $F(a) \leqslant_A F(b)$ ；若后者成立，那么 $F(b) \leqslant_A F(a)$ ，因此 $F(S)$ 中的元素间两两可以比较大小。
单调连续函数：如果 $(A, \leqslant_A)$ 是一个完备偏序集，那么单调函数 $F : A \to A$ 是连续的当且仅当：对于任意一条非空链 $S$ ， $F(\operatorname{lub}(S))=\operatorname{lub}(F(S))$ 。
引理：如果 $(A, \leqslant_A)$ 是一个完备偏序集，那么这个集合上有最小元，记做 $\bot$ 。
- 证明：空集 $\varnothing$ 是 $(A, \leqslant_A)$ 上的一条链。而任何一个 $A$ 中元素，都是空集的上界。因此，对于任意 $a \in A$ 都有， $\operatorname{lub}(\varnothing) \leqslant_A a$ 。
引理：如果 $F$ 是完备偏序集 $(A, \leqslant_A)$ 上的单调连续函数，那么 $\{\perp, F(\perp), F(F(\perp)), \ldots\}$ 是 $(A, \leqslant_A)$ 上的一条链。
- 证明：由于 $\bot$ 是最小元，所以 $\bot \leqslant_A F(\bot)$ 。由于 $F$ 是单调函数，所以 $F(\bot) \leqslant_A F(F(\bot))$ 。依次类推， $\perp \leqslant_A F(\perp) \leqslant_A F(F(\perp)) \leqslant_A \ldots$
定理：如果 $F$ 是完备偏序集 $(A, \leqslant_A)$ 上的单调连续函数， $\operatorname{lub}(\perp, F(\perp), F(F(\perp)), \ldots)$ 是 $F$ 的一个不动点。
- 证明：
$\begin{aligned} & F(\operatorname{lub}(\perp, F(\perp), F(F(\perp)), \ldots)) \\ =\quad & \operatorname{lub}(F(\perp), F(F(\perp)), F(F(F(\perp))), \ldots) \\ =\quad & \operatorname{lub}(\perp, F(\perp), F(F(\perp)), F(F(F(\perp))), \ldots) \end{aligned}$
定理：如果 $F$ 是完备偏序集 $(A, \leqslant_A)$ 上的单调连续函数且 $F(a) = a$ ，那么 $\operatorname{lub}(\perp, F(\perp), F(F(\perp)), \ldots) \leqslant_A a$ 。
- 证明：
$\begin{aligned} & \perp \leqslant_A a \\ & F(\perp) \leqslant_A F(a)=a \\ & F(F(\perp)) \leqslant_A F(a)=a \\ & ... \end{aligned}$
用 Kleene 不动点定义 while 语句语义：
- $(\mathcal{P}(\text{state} \times \text{state}), \subseteq)$ 是一个完备偏序集；
- $F(X) \triangleq \text { test\_true }(\llbracket e \rrbracket) \circ \llbracket c \rrbracket \circ X \cup \text { test\_false }(\llbracket e \rrbracket)$ $F (X) ≜ test_true ([[e]]) \circ [[c]] \circ X \cup test_false ([[e]])$ 是一个单调连续函数；
  - $G(X)=Y \circ X$ 是单调连续函数；
  - $H(X)=X \cup Y$ 是单调连续函数；
  - 如果 $G(X)$ 与 $H(X)$ 都是单调连续函数，那么 $G(H(X))$ 也是单调连续函数；
- $F$ 的最小不动点是： $\bigcup_{n \in \mathbb{N}}\left(F^{(n)}(\varnothing)\right)$
- 两种定义的对应关系： $F^{(n)}(\varnothing)=\operatorname{boundedLB}(\llbracket e \rrbracket, \llbracket c \rrbracket)$ 。

3. While 语言的指称语义

下面定义程序语句的语义。程序语句的语义包含两种情况：正常运行终止和运行出错。

Record CDenote: Type := {
  nrm: state -> state -> Prop;
  err: state -> Prop
}.

空语句的语义：

Definition skip_sem: CDenote :=
  {|
    nrm := Rels.id;
    err := ∅;
  |}.

赋值语句的语义：

Definition asgn_sem
            (X: var_name)
            (D: state -> SetMonadE.M Z): CDenote :=
  {|
    nrm := fun s1 s2 =>
      exists i,
        i ∈ (D s1).(nrm) /\ s2 X = Var_I i /\
        (forall Y, X <> Y -> s2 Y = s1 Y);
    err := fun s1 => (D s1).(err);
  |}.

顺序执行语句的语义：

Definition seq_sem (D1 D2: CDenote): CDenote :=
  {|
    nrm := D1.(nrm) ∘ D2.(nrm);
    err := D1.(err) ∪ (D1.(nrm) ∘ D2.(err));
  |}.

条件分支语句的语义：

Definition test_true (D: state -> SetMonadE.M Z):
  state -> state -> Prop :=
  Rels.test
    (fun s =>
      exists i, i ∈ (D s).(nrm) /\ i <> 0).

Definition test_false (D: state -> SetMonadE.M Z):
  state -> state -> Prop :=
  Rels.test (fun s => 0 ∈ (D s).(nrm)).

Definition err_set (D: state -> SetMonadE.M Z):
  state -> Prop :=
  fun s => (D s).(err).

Definition if_sem
            (D0: state -> SetMonadE.M Z)
            (D1 D2: CDenote): CDenote :=
  {|
    nrm := (test_true D0 ∘ D1.(nrm)) ∪
           (test_false D0 ∘ D2.(nrm));
    err := err_set D0 ∪
           (test_true D0 ∘ D1.(err)) ∪
           (test_false D0 ∘ D2.(err))
  |}.

循环语句的语义：

Definition while_sem
            (D0: state -> SetMonadE.M Z)
            (D1: CDenote): CDenote :=
  {|
    nrm := Kleene_LFix
            (fun X =>
              test_true D0 ∘ D1.(nrm) ∘ X ∪
              test_false D0);
    err := Kleene_LFix
            (fun X =>
              test_true D0 ∘ D1.(nrm) ∘ X ∪
              test_true D0 ∘ D1.(err) ∪
              err_set D0);
  |}.

程序语句的语义可以最后表示成下面递归函数。

Fixpoint eval_com (c: com): CDenote :=
  match c with
  | CSkip =>
    skip_sem
  | CAsgn X e =>
    asgn_sem X (eval_expr e)
  | CSeq c1 c2 =>
    seq_sem (eval_com c1) (eval_com c2)
  | CIf e c1 c2 =>
    if_sem (eval_expr e) (eval_com c1) (eval_com c2)
  | CWhile e c1 =>
    while_sem (eval_expr e) (eval_com c1)
  end.

4. 加入 break、continue 语句的指称语义

在 While 程序语言中加入 break 和 continue 语句。

Inductive com : Type :=
  | CSkip: com
  | CAsgn (X: var_name) (e: expr): com
  | CSeq (c1 c2: com): com
  | CIf (e: expr) (c1 c2: com): com
  | CWhile (e: expr) (c: com): com
  | CContinue: com
  | CBreak: com.

Record CDenote: Type := {
  nrm: state -> state -> Prop;
  brk: state -> state -> Prop;
  cnt: state -> state -> Prop;
  err: state -> Prop
}.

空语句的语义：

Definition skip_sem: CDenote :=
  {|
    nrm := Rels.id;
    brk := ∅;
    cnt := ∅;
    err := ∅;
  |}.

Break 语句的语义：

Definition brk_sem: CDenote :=
  {|
    nrm := ∅;
    brk := Rels.id;
    cnt := ∅;
    err := ∅;
  |}.

Continue 语句的语义：

Definition cnt_sem: CDenote :=
  {|
    nrm := ∅;
    brk := ∅;
    cnt := Rels.id;
    err := ∅;
  |}.

顺序执行语句的语义：

Definition seq_sem (D1 D2: CDenote): CDenote :=
  {|
    nrm := D1.(nrm) ∘ D2.(nrm);
    brk := D1.(brk) ∪ (D1.(nrm) ∘ D2.(brk));
    cnt := D1.(cnt) ∪ (D1.(nrm) ∘ D2.(cnt));
    err := D1.(err) ∪ (D1.(nrm) ∘ D2.(err));
  |}.

赋值语句的语义：

Definition asgn_sem
            (X: var_name)
            (D: state -> SetMonadE.M Z): CDenote :=
  {|
  nrm := fun s1 s2 =>
    exists i,
      i ∈ (D s1).(nrm) /\ s2 X = Var_I i /\
      (forall Y, X <> Y -> s2 Y = s1 Y);
  brk := ∅;
  cnt := ∅;
  err := fun s1 => (D s1).(err);
  |}.

条件分支语句的语义：

Definition if_sem
            (D0: state -> SetMonadE.M Z)
            (D1 D2: CDenote): CDenote :=
  {|
    nrm := (test_true D0 ∘ D1.(nrm)) ∪
           (test_false D0 ∘ D2.(nrm));
    brk := (test_true D0 ∘ D1.(brk)) ∪
           (test_false D0 ∘ D2.(brk));
    cnt := (test_true D0 ∘ D1.(cnt)) ∪
           (test_false D0 ∘ D2.(cnt));
    err := err_set D0 ∪
           (test_true D0 ∘ D1.(err)) ∪
           (test_false D0 ∘ D2.(err));
  |}.

循环语句的语义：

Definition while_sem
            (D0: state -> SetMonadE.M Z)
            (D1: CDenote): CDenote :=
  {|
    nrm := Kleene_LFix
            (fun X =>
              test_true D0 ∘ D1.(nrm) ∘ X ∪
              test_true D0 ∘ D1.(cnt) ∘ X ∪
              test_true D0 ∘ D1.(brk) ∪
              test_false D0);
    brk := ∅;  (* 普通终止而不是 break 终止 *)
    cnt := ∅;  (* 普通终止而不是 continue 终止 *)
    err := Kleene_LFix
            (fun X =>
              test_true D0 ∘ D1.(nrm) ∘ X ∪
              test_true D0 ∘ D1.(cnt) ∘ X ∪
              test_true D0 ∘ D1.(err) ∪
              err_set D0);
  |}.

程序语句的语义可以最后表示成下面递归函数。

Fixpoint eval_com (c: com): CDenote :=
  match c with
  | CSkip =>
    skip_sem
  | CAsgn X e =>
    asgn_sem X (eval_expr e)
  | CSeq c1 c2 =>
    seq_sem (eval_com c1) (eval_com c2)
  | CIf e c1 c2 =>
    if_sem (eval_expr e) (eval_com c1) (eval_com c2)
  | CWhile e c1 =>
    while_sem (eval_expr e) (eval_com c1)
  | CBreak =>
    brk_sem
  | CContinue =>
    cnt_sem
  end.

5. SetMonad 中加入循环

首先定义循环体的计算结果，其结果要么是 continue 终止，要么是 break 终止。

1
2
3

Inductive ContinueOrBreak (A B: Type): Type :=
  | by_continue (a: A)
  | by_break (b: B).

下面用不动点定义 repeat 循环。

Definition repeat_break_f
            {A B: Type}
            (body: A -> SetMonad.M (ContinueOrBreak A B))
            (W: A -> SetMonad.M B)
            (a: A): SetMonad.M B :=
  x <- body a;;
  match x with
  | by_continue a' => W a'
  | by_break b => ret b
  end.

Definition repeat_break
            {A B: Type}
            (body: A -> SetMonad.M (ContinueOrBreak A B)):
  A -> SetMonad.M B :=
  Kleene_LFix (repeat_break_f body).

下面还可以定义循环体中的 continue 语句和 break 语句。

Definition continue {A B: Type} (a: A):
  SetMonad.M (ContinueOrBreak A B) :=
  ret (by_continue a).

Definition break {A B: Type} (b: B):
  SetMonad.M (ContinueOrBreak A B) :=
  ret (by_break b).

下面是一些加入循环的 SetMonad 的例子。

例 1：3x + 1

Definition body_3x1 (x: Z): SetMonad.M (ContinueOrBreak Z Z) :=
  choice
    (assume (x <= 1);; break x)
    (choice
      (assume (exists k, x = 2 * k);;
        continue (x / 2))
      (assume (exists k, k <> 0 /\ x = 2 * k + 1);;
        continue (3 * x + 1))).

Definition run_3x1: Z -> SetMonad.M Z :=
  repeat_break body_3x1.

例 2：二分查找

Definition body_binary_search (P: Z -> Prop):
  Z * Z -> SetMonad.M (ContinueOrBreak (Z * Z) Z) :=
  fun '(lo, hi) =>
  choice
    (assume (lo + 1 = hi);; break lo)
    (assume (lo + 1 < hi);;
      let mid := (lo + hi) / 2 in
      choice
        (assume (P mid);; continue (mid, hi))
        (assume (~ P mid);; continue (lo, mid))).

Definition binary_search (P: Z -> Prop) (lo hi: Z):
  SetMonad.M Z :=
  repeat_break (body_binary_search P) (lo, hi).

例 3：归并

Definition body_merge:
  list Z * list Z * list Z ->
  SetMonad.M (ContinueOrBreak (list Z * list Z * list Z) (list Z)) :=
  fun '(l1, l2, l3) =>
  match l1, l2 with
  | nil, _ => break (l3 ++ l2)
  | _, nil => break (l3 ++ l1)
  | x :: l1', y :: l2' =>
    choice
      (assume (x <= y);; continue (l1', l2, l3 ++ x :: nil))
      (assume (y <= x);; continue (l1, l2', l3 ++ y :: nil))
  end.

Definition merge l l0 :=
  repeat_break body_merge (l, l0, nil).

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

1. 单子程序上的霍尔逻辑

集合单子上，霍尔三元组会退化为霍尔二元组。

1 2	`Definition Hoare {A: Type} (c: SetMonad.M A) (P: A -> Prop): Prop := forall a, a ∈ c -> P a.`

各个单子算子满足下面性质。

Theorem Hoare_bind {A B: Type}:
  forall (f: SetMonad.M A)
         (g: A -> SetMonad.M B)
         (P: A -> Prop)
         (Q: B -> Prop),
    Hoare f P ->
    (forall a, P a -> Hoare (g a) Q) ->
    Hoare (bind f g) Q.

1
2
3

Theorem Hoare_ret {A: Type}:
  forall (a: A) (P: A -> Prop),
    P a -> Hoare (ret a) P.

Theorem Hoare_conseq {A: Type}:
  forall (f: SetMonad.M A) (P Q: A -> Prop),
    (forall a, P a -> Q a) ->
    Hoare f P ->
    Hoare f Q.

Theorem Hoare_conjunct {A: Type}:
  forall (f: SetMonad.M A) (P Q: A -> Prop),
    Hoare f P ->
    Hoare f Q ->
    Hoare f (fun a => P a /\ Q a).

Theorem Hoare_choice {A: Type}:
  forall (f g: SetMonad.M A)
         (P: A -> Prop),
    Hoare f P ->
    Hoare g P ->
    Hoare (choice f g) P.

Theorem Hoare_assume_bind {A: Type}:
  forall (P: Prop)
         (f: SetMonad.M A)
         (Q: A -> Prop),
    (P -> Hoare f Q) ->
    (Hoare (assume P;; f) Q).

Theorem Hoare_repeat_break {A B: Type}:
  forall (body: A -> SetMonad.M (ContinueOrBreak A B))
         (P: A -> Prop)
         (Q: B -> Prop),
    (forall a, P a ->
              Hoare (body a) (fun x => match x with
                                      | by_continue a => P a
                                      | by_break b => Q b
                                      end)) ->
    (forall a, P a -> Hoare (repeat_break body a) Q).

2. 霍尔逻辑证明

2.1 3x + 1

Theorem functional_correctness_3x1:
  forall n: Z,
    n >= 1 ->
    Hoare (run_3x1 n) (fun m => m = 1).

2.2 二分查找

Theorem functional_correctness_binary_search:
  forall (P: Z -> Prop) lo hi,
    (forall n m, n <= m -> P m -> P n) ->
    P lo ->
    ~ P hi ->
    Hoare (binary_search P lo hi)
          (fun x => P x /\ ~ P (x + 1)).

2.3 归并

Theorem functional_correctness_merge:
  forall l1 l2,
    incr l1 ->
    incr l2 ->
    Hoare (merge l1 l2)
          (fun l3 => Permutation (l1 ++ l2) l3 /\ incr l3).

2.4 拓展欧几里得

Definition any (A: Type): SetMonad.M A := Sets.full.

Theorem Hoare_any_bind {A B: Type}:
  forall (f: A -> SetMonad.M B) (Q: B -> Prop),
    (forall a, Hoare (f a) Q) ->
    Hoare (bind (any A) f) Q.

Lemma Hoare_Kleene_LFix2 {A1 A2 B: Type}:
  forall (a1: A1) (a2: A2)
         (Q: B -> Prop)
         (f: (A1 -> A2 -> SetMonad.M B) ->
             (A1 -> A2 -> SetMonad.M B)),
    (forall n, Hoare (Nat.iter n f H a1 a2) Q) ->
    Hoare (Kleene_LFix f a1 a2) Q.

Definition body_ext_euclid
            (W: Z -> Z -> SetMonad.M (Z * Z))
            (a b: Z): SetMonad.M (Z * Z) :=
  choice
    (assume (b = 0);;
      choice
        (assume (a >= 0);; ret (1, 0))
        (assume (a <= 0);; ret (-1, 0)))
    (assume (b <> 0);;
      q <- any Z;;
      r <- any Z;;
      assume (a = r + q * b);;
      '(x, y) <- W b r;;
      ret (y, x - q * y)).

Definition ext_euclid (a b: Z): SetMonad.M (Z * Z) :=
  Kleene_LFix body_ext_euclid a b.

Lemma functional_correctness_ext_euclid_aux:
  forall W,
    (forall a b, Hoare
                  (W a b)
                  (fun '(x, y) => a * x + b * y = Z.gcd a b)) ->
    (forall a b, Hoare
                  (body_ext_euclid W a b)
                  (fun '(x, y) => a * x + b * y = Z.gcd a b)).

Theorem functional_correctness_ext_euclid:
  forall a b,
    Hoare (ext_euclid a b)
          (fun '(x, y) => a * x + b * y = Z.gcd a b).

2.5 归并排序

Definition gmergesort_f (W: list Z -> SetMonad.M (list Z)):
  list Z -> SetMonad.M (list Z) :=
  fun x =>
    choice
    (ext_sort x)
    (assume(length x >= 2)%nat;;
      '(p1, q1) <- ext_split x ;;
      p2 <- W (p1) ;;
      q2 <- W (q1) ;;
      merge p2 q2).

Definition gmergesort := Kleene_LFix gmergesort_f.

1
2
3

Theorem functional_correctness_mergesort:
  forall l,
    Hoare (gmergesort l) (fun l0 => Permutation l l0 /\ incr l0).

2.6 依次处理列表

Fixpoint list_iter
          {A B: Type}
          (f: A -> B -> SetMonad.M B)
          (l: list A)
          (b: B):
  SetMonad.M B :=
  match l with
  | nil => ret b
  | a :: l0 => b0 <- f a b;; list_iter f l0 b0
  end.

Theorem Hoare_list_iter {A B: Type}:
  forall (f: A -> B -> SetMonad.M B)
         (P: list A -> B -> Prop),
    (forall b l a,
        P l b ->
        Hoare (f a b) (fun b0 => P (l ++ a :: nil) b0)) ->
    (forall b l, P nil b -> Hoare (list_iter f l b) (fun b0 => P l b0)).

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$ $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)`

例子 - 双向链表的验证

双向链表和队列的定义：

struct list {
  int data;
  struct list *next;
  struct list *prev;
};

struct queue {
  struct list * head;
  struct list * tail;
};

入队和出队操作：

void enqueue(struct queue * q, int x)
  /*@ With l
    Require store_queue(q, l)
    Ensure store_queue(q, app(l, cons(x, nil)))
  */
{
  struct list * p = malloc_list_cell();
  p -> data = x;
  if (q -> head == ( void * ) 0) {
    q -> head = p;
    q -> tail = p;
    p -> next = ( void * ) 0;
    p -> prev = ( void * ) 0;
  }
  else {
    q -> tail -> next = p;
    p -> prev = q -> tail;
    q -> tail = p;
    p -> next = ( void * ) 0;
  }
}

int dequeue(struct queue * q)
  /*@ With x l
    Require store_queue(q, cons(x, l))
    Ensure __return == x && store_queue(q, l)
  */
{
  struct list * p = q -> head;
  int x0 = p -> data;
  q -> head = p -> next;
  free_list_cell(p);
  if (q -> head == ( void * ) 0) {
    q -> tail = ( void * ) 0;
  }
  else {
    q -> head -> prev = ( void * ) 0;
  }
  return x0;
}

例子 - 函数式先进先出队列的验证

队列的定义：

struct list {
  int data;
  struct list *next;
};

struct queue {
  struct list * l1;
  struct list * l2;
};

入队和出队操作：

void push(struct list * * p, int x)
  /*@ With l
    Require sll( * p, l)
    Ensure sll( * p, cons(x, l))
  */
{
  struct list * px = malloc_list_cell();
  px -> data = x;
  px -> next = * p;
  * p = px;
}

int pop(struct list * * p)
  /*@ With x l
    Require sll( * p, cons(x, l))
    Ensure __return == x && sll( * p, l)
  */
{
  struct list * px = * p;
  int x0 = px -> data;
  * p = px -> next;
  free_list_cell(px);
  return x0;
}

void enqueue(struct queue * q, int x)
  /*@ With l
    Require store_queue(q, l)
    Ensure store_queue(q, app(l, cons(x, nil)))
  */
{
  push(&(q -> l2), x);
}

int dequeue(struct queue * q)
  /*@ With x l
    Require store_queue(q, cons(x, l))
    Ensure __return == x && store_queue(q, l)
  */
{
  if (q -> l1 == ( void * ) 0) {
    q -> l1 = reverse(q -> l2);
    q -> l2 = ( void * ) 0;
  }
  return pop(&(q -> l1));
}

Lecture 12: 状态关系单子与霍尔逻辑

1. 状态关系单子程序

下面用 StateRelMonad 表示带有程序状态的非确定性计算。

Module StateRelMonad.

Definition M (Σ A: Type): Type :=
  Σ -> A -> Σ -> Prop.

Definition bind (Σ A B: Type) (f: M Σ A) (g: A -> M Σ B): M Σ B :=
  fun (s1: Σ) (b: B) (s3: Σ) =>
    exists (a: A) (s2: Σ),
      (s1, a, s2) ∈ f /\ (s2, b, s3) ∈ g a.
      
Definition ret (Σ A: Type) (a0: A): M Σ A :=
  fun (s1: Σ) (a: A) (s2: Σ) => a = a0 /\ s1 = s2.

End StateRelMonad.

#[export] Instance state_rel_monad (Σ: Type): Monad (StateRelMonad.M Σ) :=
{|
  bind := StateRelMonad.bind Σ;
  ret := StateRelMonad.ret Σ;
|}.

再定义一些额外的算子。

Definition assume {Σ: Type} (P: Σ -> Prop): StateRelMonad.M Σ unit :=
  fun s1 _ s2 => P s1 /\ s1 = s2.

Definition choice {Σ A: Type} (f g: StateRelMonad.M Σ A): StateRelMonad.M Σ A :=
  f ∪ g.

Definition any {Σ: Type} (A: Type): StateRelMonad.M Σ A :=
  fun s1 _ s2 => s1 = s2.

Definition repeat_break_f
            {Σ A B: Type}
            (body: A -> StateRelMonad.M Σ (ContinueOrBreak A B))
            (W: A -> StateRelMonad.M Σ B)
            (a: A): StateRelMonad.M Σ B :=
  x <- body a;;
  match x with
  | by_continue a' => W a'
  | by_break b => ret b
  end.

Definition repeat_break
            {Σ A B: Type}
            (body: A -> StateRelMonad.M Σ (ContinueOrBreak A B)):
  A -> StateRelMonad.M Σ B :=
  Kleene_LFix (repeat_break_f body).

Definition continue {Σ A B: Type} (a: A):
  StateRelMonad.M Σ (ContinueOrBreak A B) :=
  ret (by_continue a).

Definition break {Σ A B: Type} (b: B):
  StateRelMonad.M Σ (ContinueOrBreak A B) :=
  ret (by_break b).

2. 霍尔逻辑

在 StateRelMonad 上的霍尔逻辑是一个关于霍尔三元组的逻辑。

Definition Hoare {Σ A: Type}
                 (P: Σ -> Prop)
                 (c: StateRelMonad.M Σ A)
                 (Q: A -> Σ -> Prop): Prop :=
  forall s1 a s2, P s1 -> (s1, a, s2) P c -> Q a s2.

Theorem Hoare_bind {Σ A B: Type}:
  forall (P: Σ -> Prop)
         (f: StateRelMonad.M Σ A)
         (Q: A -> Σ -> Prop)
         (g: A -> StateRelMonad.M Σ B)
         (R: B -> Σ -> Prop),
  Hoare P f Q ->
  (forall a, Hoare (Q a) (g a) R) ->
  Hoare P (bind f g) R.

Theorem Hoare_ret {Σ A: Type}:
  forall (P: A -> Σ -> Prop) (a0: A),
    Hoare (P a0) (ret a0) P.

Theorem Hoare_choice {Σ A: Type}:
  forall P (f g: StateRelMonad.M Σ A) Q,
    Hoare P f Q ->
    Hoare P g Q ->
    Hoare P (choice f g) Q.

Theorem Hoare_assume_bind {Σ A: Type}:
  forall P (Q: Σ -> Prop) (f: StateRelMonad.M Σ A) R,
    Hoare (fun s => Q s /\ P s) f R ->
    Hoare P (assume Q;; f) R.

Theorem Hoare_any_bind {Σ A B: Type}:
  forall P Q (f: A -> StateRelMonad.M Σ B),
    (forall a, Hoare P (f a) Q) ->
    (Hoare P (bind (any A) f) Q).

Theorem Hoare_conseq {Σ A: Type}:
  forall (P1 P2: Σ -> Prop) f (Q1 Q2: A -> Σ -> Prop),
    (forall s, P1 s -> P2 s) ->
    (forall b s, Q2 b s -> Q1 b s) ->
    Hoare P2 f Q2 ->
    Hoare P1 f Q1.

Theorem Hoare_conseq_pre {Σ A: Type}:
  forall (P1 P2: Σ -> Prop) f (Q: A -> Σ -> Prop),
    (forall s, P1 s -> P2 s) ->
    Hoare P2 f Q ->
    Hoare P1 f Q.

Theorem Hoare_conseq_post {Σ A: Type}:
  forall (P: Σ -> Prop) f (Q1 Q2: A -> Σ -> Prop),
    (forall b s, Q2 b s -> Q1 b s) ->
    Hoare P f Q2 ->
    Hoare P f Q1.

Theorem Hoare_conj {Σ A: Type}:
  forall (P: Σ -> Prop) f (Q1 Q2: A -> Σ -> Prop),
    Hoare P f Q1 ->
    Hoare P f Q2 ->
    Hoare P f (fun a s => Q1 a s /\ Q2 a s).

Theorem Hoare_forall {Σ A: Type}:
  forall (X: Type) (P: Σ -> Prop) f (Q: X -> A -> Σ -> Prop),
    (forall x, Hoare P f (Q x)) ->
    Hoare P f (fun a s => forall x, Q x a s).

Theorem Hoare_pre_ex {Σ A: Type}:
  forall (X: Type) (P: X -> Σ -> Prop) f (Q: A -> Σ -> Prop),
    (forall x, Hoare (P x) f Q) ->
    Hoare (fun s => exists x, P x s) f Q.

Theorem Hoare_ret ' {Σ A: Type}:
    forall (P: Σ -> Prop) (Q: A -> Σ -> Prop) (a0: A),
    (forall s, P s -> Q a0 s) ->
    Hoare P (ret a0) Q.

Theorem Hoare_repeat_break {Σ A B: Type}:
  forall (body: A -> StateRelMonad.M Σ (ContinueOrBreak A B))
         (P: A -> Σ -> Prop)
         (Q: B -> Σ -> Prop),
  (forall a, Hoare (P a) (body a) (fun x s => match x with
                                             | by_continue a => P a s
                                             | by_break b => Q b s
                                             end)) ->
  (forall a, Hoare (P a) (repeat_break body a) Q).

3. 定义有向图和图上的程序

如下定义有向图。

Record PreGraph (Vertex Edge: Type) := {
  vvalid : Vertex -> Prop;
  evalid : Edge -> Prop;
  src : Edge -> Vertex;
  dst : Edge -> Vertex
}.

基于此就能定义“从 x 点经过一条边可以到达 y 点”。

Record step_aux {V E: Type} (pg: PreGraph V E) (e: E) (x y: V): Prop :=
{
  step_evalid: pg.(evalid) e;
  step_src_valid: pg.(vvalid) x;
  step_dst_valid: pg.(vvalid) y;
  step_src: pg.(src) e = x;
  step_dst: pg.(dst) e = y;
}.

Definition step {V E: Type} (pg: PreGraph V E) (x y: V): Prop :=
  exists e, step_aux pg e x y.

进一步，单步可达关系的自反传递闭包就是多步可达关系。

1 2	`Definition reachable {V E: Type} (pg: PreGraph V E) := clos_refl_trans (step pg).`

参考资料

本文参考上海交通大学程序语言与编译原理课程 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