读软件工程论文时，最让人泄气的时刻，往往不是看不懂算法，而是读到一半突然被一行符号挡住：每个字母似乎都见过，连在一起却不知道该从哪里读起。
这种停顿通常与数学能力无关。论文只是把研究对象、程序状态和分析步骤压缩进了几行定义，却省略了初学者最需要的阅读顺序。本文要做的，就是把这些定义重新展开，翻译成自然语言和熟悉的程序操作。
先看两种常见写法：
\[\sigma\in\Sigma=X\rightarrow V\]或者
\[[\![x=e]\!](\sigma) = \sigma[x\mapsto[\![e]\!](\sigma)],\]它们看起来像数学题，其实没有未知数需要求解：第一行定义程序状态，第二行描述赋值语句如何改变状态。拆开以后，不过是字典操作和几行伪代码。
本文不补一整套数学课程，只讨论怎样阅读软件工程论文中的形式化表达。以后在 ICSE、FSE、ASE、ISSTA 等会议论文里再遇到集合、映射和语义规则时，你会知道先看什么。
多数软件工程论文里的形式化是一种精确的技术语言，主要回答三个问题：
- 研究对象是什么？
- 这些对象如何组织在一起？
- 方法按照什么规则处理它们？
我们会借助一个只有两条赋值语句的小程序，认识最常见的符号。读完后，你应该能够：
- 区分集合、元素、元组和序列；
- 读懂 $f:A\rightarrow B$ 一类映射声明；
- 把程序状态理解为“变量到值”的映射；
- 将一条语义规则翻译成自然语言或伪代码；
- 面对陌生公式时，知道先看哪里、后看哪里。
阅读路线如下：
\[\text{基本对象} \longrightarrow \text{程序状态} \longrightarrow \text{语义规则} \longrightarrow \text{阅读方法}.\]1. 形式化到底解决什么问题？
先看一句常见的方法描述：
分析器在程序执行过程中记录每个变量的值。
这句话不难懂，却不够精确。比如：
- “变量”具体包括哪些对象？
- “值”来自哪个范围？
- 每个变量是否都对应一个值？
- 一个变量的值未知时怎样表示？
- “记录”在数学上究竟是什么关系？
作者不妨先定义：
\[X = \text{the set of program variables},\] \[V = \text{the set of values},\]再写：
\[\sigma:X\rightarrow V.\]这行公式说明：$\sigma$ 是一个从变量集合 $X$ 到值集合 $V$ 的映射。给定任意变量 $x\in X$，$\sigma(x)$ 就是它当前对应的值。
自然语言负责解释直觉，形式化负责消除歧义。两者并不冲突；一篇写得好的论文通常会同时使用它们。
1.1 先“翻译”公式，不要急着“解”公式
初学者看到下面的表达式时，常会下意识地寻找推导过程：
\[\sigma\in\Sigma=X\rightarrow V.\]但这不是一道方程题，而是一组压缩在一起的定义。把它从右向左拆开：
- $X\rightarrow V$：从 $X$ 到 $V$ 的函数；
- $\Sigma=X\rightarrow V$：$\Sigma$ 是所有这类函数组成的集合；
- $\sigma\in\Sigma$：$\sigma$ 是其中一个具体函数。
合起来就是一句话：
一个程序状态 $\sigma$ 把每个变量映射到一个值。
以后再遇到公式，先问“这句话用自然语言怎么说”，再研究作者为什么这样定义。
2. 先认识公式里的基本对象
复杂定义通常由少数几种基本结构组成。集合说明“有哪些对象”，元组负责“把对象组合起来”，序列则表示“按顺序排列的一组对象”。
2.1 集合与元素
假设：
\[X=\text{the set of program variables}.\]$X$ 表示程序变量的集合。它可能包含：
\[X=\{x,y,result,count,\ldots\}.\]论文一般不会枚举程序中的全部变量，而是用 $X$ 代表这个整体。
成员关系：$x\in X$
表达式
\[x\in X\]表示“$x$ 是集合 $X$ 中的一个元素”。如果 $X$ 已被定义为变量集合，就直接读成“$x$ 是一个变量”。
类似地，若
\[L=\text{the set of program locations},\]则
\[\ell\in L\]表示 $\ell$ 是一个程序位置。
大写与小写是一种惯例
程序分析和编程语言论文经常写：
\[x\in X,\qquad v\in V,\qquad \ell\in L.\]通常，大写字母表示集合或域，小写字母表示其中一个具体元素。例如，$V=\mathbb{Z}$ 表示值域为整数，而 $v\in V$ 表示某个具体整数。
这只是常见的命名习惯，不是数学规则。作者给出的正式定义始终比字母外形更可靠。
2.2 元组与笛卡尔积
在
\[A\times B\]中，$\times$ 通常不是数值乘法，而是笛卡尔积。它把 $A$ 中的元素与 $B$ 中的元素两两组合。
若
\[A=\{a_1,a_2\},\qquad B=\{b_1,b_2\},\]那么
\[A\times B= \{(a_1,b_1),(a_1,b_2),(a_2,b_1),(a_2,b_2)\}.\]在程序分析中，笛卡尔积常用于组合不同类型的信息。例如：
\[L\times X\]表示所有“程序位置与变量”的组合，其中 $(\ell,x)$ 指“位于 $\ell$ 的变量 $x$”。再加上值域后，
\[(\ell,x,v)\in L\times X\times V\]表示“在程序位置 $\ell$，变量 $x$ 对应值 $v$”。
看到 $\times$ 时，先把它读成“把几类对象放进同一个元组”。
2.3 序列与 Kleene 星号
表达式
\[A^*\]表示由零个或多个 $A$ 中元素组成的有限序列。这里的星号称为 Kleene 星号。
若 $I$ 是指令集合，那么 $I^*$ 就是一段指令序列，可以是：
\[[],\qquad [i_1],\qquad [i_1,i_2,i_3].\]这个记号常用于表示：
- 语句或指令序列；
- 函数参数列表；
- API 调用序列；
- 程序执行轨迹。
集合强调“成员属于哪里”，元组强调“哪些对象组成一项记录”，序列则额外保留元素的先后顺序。
3. 用映射描述程序状态
认识基本对象后，下一步是把它们组织起来。程序分析中最常见的组织方式是映射。
3.1 函数声明：$f:A\rightarrow B$
表达式
\[f:A\rightarrow B\]表示 $f$ 是一个从 $A$ 到 $B$ 的函数。给定 $a\in A$，函数返回的 $f(a)$ 属于 $B$。
例如，设
\[Name=\{Alice,Bob,Carol\},\qquad Age=\mathbb{N},\]就可以定义：
\[age:Name\rightarrow Age.\]$age(Alice)=20$ 表示 Alice 被映射到年龄 20。
读函数声明时，先别管内部算法。只看箭头两侧，确认“输入是什么，输出是什么”，定义的轮廓就清楚了。
3.2 程序状态是变量到值的映射
程序状态的典型定义是：
\[\sigma\in\Sigma=X\rightarrow V.\]其中：
- $X$：变量集合；
- $V$：值集合；
- $\Sigma$：所有程序状态的集合；
- $\sigma$：一个具体的程序状态。
例如：
\[\sigma=\{x\mapsto1,\ y\mapsto3,\ z\mapsto10\}.\]于是：
\[\sigma(x)=1,\qquad \sigma(y)=3,\qquad \sigma(z)=10.\]如果换成代码，它很像一个字典：
1
2
3
4
5
state = {
"x": 1,
"y": 3,
"z": 10,
}
因此，$\sigma:X\rightarrow V$ 可以暂时记作：
1
Map<Variable, Value>
论文里的状态定义并不是脱离实现的装饰。很多分析器在代码中确实会维护与之相似的数据结构。
3.3 区分 $\rightarrow$ 与 $\mapsto$
这两个箭头用途不同：
$\rightarrow$ 描述映射的类型
\[\sigma:X\rightarrow V\]说明 $\sigma$ 的输入来自 $X$，输出落在 $V$。
$\mapsto$ 描述一项具体对应关系
\[x\mapsto42\]说明 $x$ 被映射到 42。因此：
\[\sigma=\{x\mapsto1,\ y\mapsto2\}\]给出了一个具体状态的内容。
两者可以简记为：
$\rightarrow$ 说明函数“从哪里到哪里”；$\mapsto$ 说明某个元素“具体对应什么”。
3.4 状态更新：$\sigma[x\mapsto v]$
程序执行会改变状态。表达式
\[\sigma[x\mapsto v]\]表示在 $\sigma$ 的基础上把 $x$ 更新为 $v$，其他变量保持不变。
若
\[\sigma=\{x\mapsto1,\ y\mapsto2\},\]那么
\[\sigma[x\mapsto10]=\{x\mapsto10,\ y\mapsto2\}.\]对应的伪代码是：
1
2
new_state = state.copy()
new_state[x] = 10
考虑赋值语句：
1
x = y + 1;
如果当前状态为 $\sigma$，执行过程可以写成：
- 用 $\sigma(y)$ 读取
y； - 计算 $\sigma(y)+1$；
- 得到新状态 $\sigma[x\mapsto\sigma(y)+1]$。
这行数学表达与“计算右侧表达式，然后写回变量 x”完全对应。
3.5 撇号通常表示更新后的对象
$\sigma’$ 读作 sigma prime。在程序语义中，它常表示下一状态或更新后的状态。例如：
\[\sigma\rightarrow\sigma'\]可以表示程序从状态 $\sigma$ 转移到状态 $\sigma’$。
Prime 并没有跨论文统一的含义。它也可能表示“与原对象相关的另一个对象”，因此仍需查看作者的定义。
4. 从程序执行读到语义规则
集合和映射帮助我们描述状态，语义规则则进一步说明：一段程序如何读取或改变状态。
4.1 语义括号：解释一段程序
程序语言文献中常用
\[[\![e]\!]\]表示程序结构 $e$ 的语义，也就是“$e$ 表示什么”。例如：
\[[\![1+2]\!]=3.\]表达式的结果通常依赖当前状态。对 x + 1，可以定义：
它的意思是：在状态 $\sigma$ 下解释 x + 1，先读取 x 的值，再加 1。
第一次见到双括号时，可以把
\[[\![e]\!](\sigma)\]暂时看作：
1
eval(e, state)
也就是“给定表达式和程序状态，计算表达式的含义”。
4.2 拆解一条赋值语义
现在把前面的符号组合起来：
\[[\![x=e]\!](\sigma) = \sigma[x\mapsto[\![e]\!](\sigma)].\]这条规则描述赋值语句 x = e。不要试图一眼读完整行，可以分两步看。
第一步：计算右侧表达式
\[v=[\![e]\!](\sigma).\]在当前状态 $\sigma$ 下计算 $e$，结果记为 $v$。
第二步：用结果更新状态
\[\sigma[x\mapsto v].\]把变量 $x$ 更新为 $v$，其他变量不变。
整条规则对应下面几行伪代码：
1
2
3
4
value = eval(e, state)
new_state = state.copy()
new_state[x] = value
return new_state
许多复杂的语义规则，其实是用数学形式写出的解释器或分析算法。把公式改写成伪代码，比反复盯着符号更容易看出执行顺序。
4.3 完整示例：执行两条赋值语句
考虑程序：
1
2
x = 1;
y = x + 2;
变量集合和值域分别是：
\[X=\{x,y\},\qquad V=\mathbb{Z}.\]所有程序状态构成：
\[\Sigma=X\rightarrow V.\]设初始状态为 $\sigma_0$。执行 x = 1 后：
所以 $\sigma_1(x)=1$。
接着执行 y = x + 2。先计算右侧表达式：
再更新 y：
最终状态满足：
\[\sigma_2(x)=1, \qquad \sigma_2(y)=3.\]这段推演展示了一条完整链路：先定义对象和状态，再用语义规则描述程序如何改变状态。
4.4 延伸：帽子符号表示抽象对象
理解具体执行后，再看静态分析中的抽象值会更自然。相关论文经常同时使用 $v$ 与 $\hat{v}$，帽子通常表示对象的抽象版本。
例如，程序运行时的具体值是：
\[v=42.\]如果分析器只关心正数、负数和零，就可能把它抽象为：
\[\hat{v}=Positive.\]类似地，$V$ 可能表示具体值域，$\hat{V}$ 表示抽象值域。这类抽象不是随意丢失信息，而是只保留当前分析真正需要的性质：
\[\text{具体对象}\longrightarrow\text{保留所需性质的抽象对象}.\]Hat 是抽象解释中的常见约定，但不是固定语法。看到 $\hat{x}$ 时，先检查作者是否在区分具体对象与抽象对象。
5. 怎样阅读一段陌生的形式化？
读论文时，最长的规则总是最显眼，但它通常不适合作为起点。下面这套顺序更稳妥。
5.1 第一步：找出基本域
先在正文或符号表中找到：
\[X=?,\qquad V=?,\qquad L=?\]确认作者定义了哪些基本对象，例如变量、值、程序位置、表达式和指令。
5.2 第二步：找出结构化对象
再看基本对象如何组合。例如：
\[\sigma:X\rightarrow V\]把变量与值组织成状态；
\[(\ell,\sigma)\in L\times\Sigma\]把程序位置与当前状态组成一个配置。
5.3 第三步：只看函数的输入与输出
假设论文定义：
\[Analysis:P\rightarrow R.\]第一遍先不研究函数内部，只确认 $P$ 是什么程序表示、$R$ 是什么分析结果。函数类型已经透露了方法的大致目标。
5.4 第四步：最后阅读规则
读具体规则时，按求值顺序拆分公式：先读取什么，再计算什么，最后更新或返回什么。必要时将每一步写成伪代码。
5.5 建立自己的符号表
遇到符号较多的论文，可以在草稿上记录：
1
2
3
4
5
6
7
8
9
10
11
L = 程序位置集合
ℓ = 一个程序位置
X = 变量集合
x = 一个变量
V = 值集合
v = 一个值
Σ = 程序状态集合
σ = 一个程序状态，即变量到值的映射
这样再看到 $(\ell,\sigma)$ 时，就能直接读成“当前程序位置与当前程序状态”，不必每次回头寻找定义。
5.6 不要根据希腊字母猜含义
论文经常使用：
\[\sigma,\pi,\xi,\Gamma,\Sigma,\Phi,\Delta,\ldots\]有些约定确实很常见，例如 $\sigma$ 表示状态、$\pi$ 表示路径、$\Gamma$ 表示环境或上下文。但这些符号没有全领域统一的解释。
如果论文写 $\sigma\in\Sigma$，关键是作者如何定义 $\Sigma$，而不是你过去在哪里见过 $\sigma$。
5.7 避开三个常见误区
误区一：从最长的公式开始
看到 $F(\sigma,\ell,x,\ldots)=\ldots$ 就直接研究右侧细节，很容易被未定义的符号卡住。先找基本域、函数类型和辅助定义。
误区二：第一遍就理解所有分支
第一遍只需抓住：
\[\text{输入}\rightarrow\text{状态}\rightarrow\text{规则}\rightarrow\text{输出}.\]确认主干后，再回头检查边界情况和特殊分支。
误区三：把所有形式化都当成证明
许多程序分析论文中的公式是在给方法写规范，而不是要求读者推导定理。先问“这一定义描述了什么”，再问“作者能从中证明什么”。
6. 常见符号速查表
| 符号 | 阅读方式 |
|---|---|
| $x\in X$ | $x$ 是集合 $X$ 中的元素 |
| $A\subseteq B$ | $A$ 是 $B$ 的子集 |
| $A\times B$ | 从 $A$、$B$ 中各取一个元素组成二元组 |
| $f:A\rightarrow B$ | $f$ 是从 $A$ 到 $B$ 的映射 |
| $x\mapsto v$ | $x$ 具体映射到 $v$ |
| $A^*$ | 由 $A$ 中元素组成的有限序列 |
| $\sigma:X\rightarrow V$ | 程序状态把变量映射到值 |
| $\sigma(x)$ | 查询状态中变量 $x$ 的值 |
| $\sigma[x\mapsto v]$ | 把状态中的 $x$ 更新为 $v$ |
| $\sigma’$ | 通常表示更新后的状态或下一个状态 |
| $\hat{x}$ | 通常表示 $x$ 的抽象版本 |
| \([\![e]\!]\) | 程序结构 $e$ 的语义解释 |
这张表用来查阅，不必一次背完。更有用的练习，是把符号放回论文的上下文中翻译。
6.1 本篇暂不展开的符号
后续阅读中还会遇到：
\[\bot,\qquad \top,\qquad \sqsubseteq,\qquad \sqcup,\qquad lfp,\]以及：
\[\langle e,\sigma\rangle \rightarrow \langle e',\sigma'\rangle.\]它们涉及抽象域、格、合并操作、不动点和操作语义。本文先不展开这些理论；在进入它们之前，先建立“程序—状态—规则”这条主线更重要。
7. 练习：把公式翻译成自然语言
建议先用一句自然语言回答，再尝试写出对应的伪代码或具体结果。
7.1 集合与元素
给定：
\[L=\{\ell_1,\ell_2,\ldots\}, \qquad \ell\in L.\]$L$ 和 $\ell$ 分别表示什么？
7.2 映射
解释：
\[Env:X\rightarrow V.\]它接收什么，返回什么？
7.3 状态更新
若
\[\sigma=\{x\mapsto1,\ y\mapsto2\},\]那么
\[\sigma[x\mapsto5]\]得到什么状态？
7.4 表达式语义
解释：
\[[\![x+1]\!](\sigma).\]若 $\sigma(x)=10$，结果是多少？
7.5 赋值语义
尝试将下面的定义完整翻译成自然语言：
\[[\![x=e]\!](\sigma) = \sigma[x\mapsto[\![e]\!](\sigma)].\]如果能指出公式中哪一部分负责求值、哪一部分负责更新，本文的主要内容就掌握了。
8. 进一步阅读
本文只负责帮你跨过符号阅读这道门槛。如果想继续深入，可以根据自己的研究问题选一条路线，不必一次把所有材料都学完。
程序语言基础：本博客的 Easy Foundations for Programming Languages 系列从类型化 Lambda 演算讲起，适合刚接触程序语言理论的学生。
形式化推理与程序验证：Software Foundations 是一套经典的交互式教材，内容涵盖逻辑、操作语义、Hoare 逻辑和类型系统。书中定义和练习都使用 Coq 检查，适合希望系统练习形式化推理的读者。
Operational Semantics 与 Denotational Semantics：Cornell CS 4110 的课程材料 给出了一个很好记的区分：Operational Semantics 关注程序如何计算，Denotational Semantics 关注程序计算什么。如果论文开始讨论求值关系或语义函数，可以从这里继续。
静态分析：若研究方向涉及静态分析，可以阅读 MIT Press 的 Introduction to Static Analysis: An Abstract Interpretation Perspective。它从程序语义、状态抽象和抽象语义讲到不动点计算与工作列表算法，理论与实现衔接得比较完整。
抽象解释的理论基础：Patrick Cousot 的 MIT Abstract Interpretation 课程适合继续研究格、不动点和可靠近似。不过，对刚进入软件工程研究的学生来说，这不应是 formalization 的起点。先学会读程序、状态和迁移规则，再进入格与不动点，会更容易建立直觉。
这些材料不是一张必须依次完成的课程表。做程序验证，可以优先看 Software Foundations；研究静态分析，就从 MIT Press 的教材向抽象解释深入；只想读懂论文中的语义定义，博客系列和 Cornell 的课程材料已经足够作为下一步。
9. 本篇小结
Formalization 入门最重要的不是掌握多少数学，而是形成一种阅读顺序：
\[\boxed{ \text{对象} \longrightarrow \text{关系} \longrightarrow \text{规则} }\]先找“定义了什么对象”，再看“对象之间有什么关系”，最后才看“规则如何计算”。对应到论文中，就是三个具体问题：
- 作者定义了哪些对象？
- 这些对象通过集合、元组或映射形成了什么结构？
- 算法如何查询、转换或更新这些结构？
对刚开始阅读程序分析论文的学生，可以先建立下面这条直觉：
\[\text{Formalization} \approx \text{用集合、映射和规则精确描述算法}.\]当你看到
\[\sigma:X\rightarrow V\]时，不必把它看成一串陌生符号，直接读成：
程序状态把每个变量映射到一个值。
当你看到
\[[\![x=e]\!](\sigma) = \sigma[x\mapsto[\![e]\!](\sigma)]\]时，也不用把它当作复杂数学。它说的是：
计算右侧表达式，然后用结果更新变量 $x$。
能在公式、自然语言和伪代码之间完成这样的转换，就迈过了阅读软件工程形式化定义的第一道门槛。