软件工程形式化入门（一）：别怕公式——从集合、映射读懂程序状态
论文里的集合、箭头和希腊字母总让你卡住？从程序状态出发，学会把形式化定义重新读成熟悉的程序概念。
一位刚进入课题组的硕士生第一次参加论文讨论时，在方法章节旁边写满了问号。他认得“变量”“状态”和“赋值”这些词，却说不清作者为什么要换一套符号重新描述它们。更让人沮丧的是，每个符号单独看都不陌生，连在一起却像一句无法断句的话。
讨论开始后，导师没有让他先去补高等数学，而是指着定义问了三个朴素的问题：这里定义了什么对象？对象之间是什么关系？这条规则让程序状态发生了什么变化？当公式被按这个顺序拆开，它忽然不再像一道需要求解的数学题，而更像一段写得格外紧凑的伪代码。
“软件工程形式化入门”系列正是从这三个问题出发，主要写给刚接触软件分析的硕士研究生，也欢迎对静态分析（static analysis）、程序验证（program verification）和程序语言（programming languages）感兴趣的读者。它不会要求你先补完一整套数学，而是帮助你获得阅读论文形式化描述（formalization）所需的基本能力：辨认对象、翻译规则，并看清技术结论依赖的前提。
六篇主线文章会跟随一个程序分析器逐步展开：先看清程序状态怎样被表示，再进入控制流与程序语义，接着理解抽象解释（abstract interpretation）为何能够处理庞大的状态空间，最后讨论不动点计算、可靠性与工程取舍。第一篇只做旅程中最基础、也最关键的一件事——学会给公式断句。
形式化不是横在文字与结论之间的墙，而是一座把程序对象、关系和规则连接起来的桥。
作为整个系列的起点，本文暂时不追求更复杂的理论，而是先学会辨认公式中的基本对象，理解它们如何组成程序状态，再把一条语义规则还原成自然语言和伪代码。从下面两种常见写法开始：
\[\sigma\in\Sigma=X\rightarrow V\]或者
\[[\![x=e]\!](\sigma) = \sigma[x\mapsto[\![e]\!](\sigma)],\]它们看起来像数学题，其实没有未知数需要求解：第一行定义程序状态，第二行描述赋值语句如何改变状态。拆开以后，不过是字典操作和几行伪代码。当你以后在 ICSE、FSE、ASE、ISSTA 等会议论文里再遇到集合、映射和语义规则时，这些符号就不再是需要跳过的黑箱。
多数软件工程论文里的形式化是一种精确的技术语言，主要回答三个问题：
- 研究对象是什么？
- 这些对象如何组织在一起？
- 方法按照什么规则处理它们？
我们会借助一个只有两条赋值语句的小程序，先区分集合、元素、元组和序列，再读懂映射与程序状态，最后把语义规则还原为自然语言和伪代码。这条路线的目标不是记住一张符号表，而是建立一套面对陌生公式时仍然可以工作的阅读顺序。
一、形式化到底解决什么问题？
先看一句常见的方法描述：
分析器在程序执行过程中记录每个变量的值。
这句话不难懂，却不够精确。比如：
- “变量”具体包括哪些对象？
- “值”来自哪个范围？
- 每个变量是否都对应一个值？
- 一个变量的值未知时怎样表示？
- “记录”在数学上究竟是什么关系？
作者不妨先定义：
\[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)$ 就是它当前对应的值。
自然语言负责解释直觉，形式化负责消除歧义。两者并不冲突；一篇写得好的论文通常会同时使用它们。
初学者看到下面的表达式时，常会下意识地寻找推导过程：
\[\sigma\in\Sigma=X\rightarrow V.\]但这不是一道方程题，而是一组压缩在一起的定义。把它从右向左拆开：
- $X\rightarrow V$：从 $X$ 到 $V$ 的函数；
- $\Sigma=X\rightarrow V$：$\Sigma$ 是所有这类函数组成的集合；
- $\sigma\in\Sigma$：$\sigma$ 是其中一个具体函数。
合起来就是一句话：
一个程序状态 $\sigma$ 把每个变量映射到一个值。
以后再遇到公式，先问“这句话用自然语言怎么说”，再研究作者为什么这样定义。
二、先认识公式里的基本对象
复杂定义通常由少数几种基本结构组成。集合说明“有哪些对象”，元组负责“把对象组合起来”，序列则表示“按顺序排列的一组对象”。
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$ 时，先把它读成“把几类对象放进同一个元组”。
元组适合表示长度固定、不同位置各有含义的结构；当元素数量不固定而且顺序重要时，论文通常改用序列。
表达式
\[A^*\]表示由零个或多个 $A$ 中元素组成的有限序列。这里的星号称为克莱尼星号（Kleene star）。
若 $I$ 是指令集合，那么 $I^*$ 就是一段指令序列，可以是：
\[[],\qquad [i_1],\qquad [i_1,i_2,i_3].\]这个记号常用于表示：
- 语句或指令序列；
- 函数参数列表；
- 应用程序接口（Application Programming Interface，API）调用序列；
- 程序执行轨迹。
集合强调“成员属于哪里”，元组强调“哪些对象组成一项记录”，序列则额外保留元素的先后顺序。
三、用映射描述程序状态
认识基本对象后，下一步是把它们组织起来。程序分析中最常见的组织方式是映射。
3.1 从函数声明到程序状态
表达式
\[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。
读函数声明时，先别管内部算法。只看箭头两侧，确认“输入是什么，输出是什么”，定义的轮廓就清楚了。
在程序分析中，映射最重要的用途之一，就是描述变量与当前值之间的关系。
程序状态的典型定义是：
\[\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.2 箭头、对应关系与状态更新
这两个箭头用途不同：
$\rightarrow$ 描述映射的类型。
\[\sigma:X\rightarrow V\]说明 $\sigma$ 的输入来自 $X$，输出落在 $V$。
$\mapsto$ 描述一项具体对应关系。
\[x\mapsto42\]说明 $x$ 被映射到 42。因此：
\[\sigma=\{x\mapsto1,\ y\mapsto2\}\]给出了一个具体状态的内容。
两者可以简记为：
$\rightarrow$ 说明函数“从哪里到哪里”；$\mapsto$ 说明某个元素“具体对应什么”。
区分映射的类型和其中一项具体对应关系之后，就可以进一步描述程序执行时最常见的操作：更新状态。
程序执行会改变状态。表达式
\[\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.3 更新后的对象怎样命名？
$\sigma’$ 读作“西格玛撇”（sigma prime）。在程序语义中，它常表示下一状态或更新后的状态。例如：
\[\sigma\rightarrow\sigma'\]可以表示程序从状态 $\sigma$ 转移到状态 $\sigma’$。
撇号（prime）并没有跨论文统一的含义。它也可能表示“与原对象相关的另一个对象”，因此仍需查看作者的定义。
四、从程序执行读到语义规则
集合和映射帮助我们描述状态，语义规则则进一步说明：一段程序如何读取或改变状态。
4.1 从语义括号到赋值规则
程序语言文献中常用
\[[\![e]\!]\]表示程序结构 $e$ 的语义，也就是“$e$ 表示什么”。例如：
\[[\![1+2]\!]=3.\]表达式的结果通常依赖当前状态。对 x + 1，可以定义：
它的意思是：在状态 $\sigma$ 下解释 x + 1，先读取 x 的值，再加 1。
第一次见到双括号时，可以把
\[[\![e]\!](\sigma)\]暂时看作：
1
eval(e, state)
也就是“给定表达式和程序状态，计算表达式的含义”。
有了语义括号的直觉后，可以把一条赋值语义完整拆开来看。
现在把前面的符号组合起来：
\[[\![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.2 完整示例：执行两条赋值语句
考虑程序：
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.\]这段推演展示了一条完整链路：先定义对象和状态，再用语义规则描述程序如何改变状态。
完整例子还引出论文中的另一种常见命名约定：在符号上加帽子，表示对象的抽象版本。
理解具体执行后，再看静态分析中的抽象值会更自然。相关论文经常同时使用 $v$ 与 $\hat{v}$，帽子通常表示对象的抽象版本。
例如，程序运行时的具体值是：
\[v=42.\]如果分析器只关心正数、负数和零，就可能把它抽象为：
\[\hat{v}=Positive.\]类似地，$V$ 可能表示具体值域，$\hat{V}$ 表示抽象值域。这类抽象不是随意丢失信息，而是只保留当前分析真正需要的性质：
\[\text{具体对象}\longrightarrow\text{保留所需性质的抽象对象}.\]帽子符号（hat）是抽象解释中的常见约定，但不是固定语法。看到 $\hat{x}$ 时，先检查作者是否在区分具体对象与抽象对象。
五、怎样阅读一段陌生的形式化？
读论文时，最长的规则总是最显眼，但它通常不适合作为起点。下面这套顺序更稳妥。
阅读陌生形式化的顺序：先辨认对象，再追踪它们之间的关系，最后进入真正的计算规则。
5.1 一套稳定的阅读顺序
第一步：找出基本域。
先在正文或符号表中找到：
\[X=?,\qquad V=?,\qquad L=?\]确认作者定义了哪些基本对象，例如变量、值、程序位置、表达式和指令。
第二步：找出结构化对象。
再看基本对象如何组合。例如：
\[\sigma:X\rightarrow V\]把变量与值组织成状态；
\[(\ell,\sigma)\in L\times\Sigma\]把程序位置与当前状态组成一个配置。
第三步：只看函数的输入与输出。
假设论文定义：
\[Analysis:P\rightarrow R.\]第一遍先不研究函数内部，只确认 $P$ 是什么程序表示、$R$ 是什么分析结果。函数类型已经透露了方法的大致目标。
第四步：最后阅读规则。
读具体规则时，按求值顺序拆分公式：先读取什么，再计算什么，最后更新或返回什么。必要时将每一步写成伪代码。
5.2 建立符号表，也警惕符号惯例
遇到符号较多的论文，可以在草稿上记录：
1
2
3
4
5
6
7
8
9
10
11
L = 程序位置集合
ℓ = 一个程序位置
X = 变量集合
x = 一个变量
V = 值集合
v = 一个值
Σ = 程序状态集合
σ = 一个程序状态，即变量到值的映射
这样再看到 $(\ell,\sigma)$ 时，就能直接读成“当前程序位置与当前程序状态”，不必每次回头寻找定义。
建立符号表的同时，还要避免根据字母外形猜含义。
论文经常使用：
\[\sigma,\pi,\xi,\Gamma,\Sigma,\Phi,\Delta,\ldots\]有些约定确实很常见，例如 $\sigma$ 表示状态、$\pi$ 表示路径、$\Gamma$ 表示环境或上下文。但这些符号没有全领域统一的解释。
如果论文写 $\sigma\in\Sigma$，关键是作者如何定义 $\Sigma$，而不是你过去在哪里见过 $\sigma$。
5.3 三个常见误区
误区一：从最长的公式开始。
看到 $F(\sigma,\ell,x,\ldots)=\ldots$ 就直接研究右侧细节，很容易被未定义的符号卡住。先找基本域、函数类型和辅助定义。
误区二：第一遍就理解所有分支。
第一遍只需抓住：
\[\text{输入}\rightarrow\text{状态}\rightarrow\text{规则}\rightarrow\text{输出}.\]确认主干后，再回头检查边界情况和特殊分支。
误区三：把所有形式化都当成证明。
许多程序分析论文中的公式是在给方法写规范，而不是要求读者推导定理。先问“这一定义描述了什么”，再问“作者能从中证明什么”。
六、符号速查
| 符号 | 阅读方式 |
|---|---|
| $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$ 的语义解释 |
这张表用来查阅，不必一次背完。更有用的练习，是把符号放回论文的上下文中翻译。
七、进一步阅读
本文只负责帮你跨过符号阅读这道门槛。如果想继续深入，可以根据自己的研究问题选一条路线，不必一次把所有材料都学完。
程序语言基础：本博客的 Easy Foundations for Programming Languages 系列从类型化 $\lambda$ 演算（typed lambda calculus）讲起，适合刚接触程序语言理论的学生。
形式化推理与程序验证：Software Foundations 是一套经典的交互式教材，内容涵盖逻辑、操作语义、霍尔逻辑（Hoare logic）和类型系统。书中的定义和练习都使用证明助手（Coq）检查，适合希望系统练习形式化推理的读者。
操作语义（Operational Semantics）与指称语义（Denotational Semantics）：康奈尔大学（Cornell University）CS 4110 的课程材料 给出了一个很好记的区分：操作语义关注程序如何计算，指称语义关注程序计算什么。如果论文开始讨论求值关系或语义函数，可以从这里继续。
静态分析入门网课：南京大学李樾老师的《软件分析》课程 从基本概念逐步进入静态分析的理论与实践，适合还没有系统学过程序分析的读者。课程的讲解对新手很友好，硕士生可以用它建立研究所需的基本框架，对这个方向感兴趣的本科生也完全可以跟学。
静态分析教材：建立基本直觉后，可以继续阅读麻省理工学院出版社（MIT Press）的 Introduction to Static Analysis: An Abstract Interpretation Perspective。它从程序语义、状态抽象和抽象语义讲到不动点计算与工作列表算法，理论与实现衔接得比较完整。
抽象解释的理论基础：帕特里克·库索（Patrick Cousot）的 麻省理工学院（MIT）抽象解释（Abstract Interpretation）课程适合继续研究格、不动点和可靠近似。不过，对刚进入软件工程研究的学生来说，这不应是形式化（formalization）的起点。先学会读程序、状态和迁移规则，再进入格与不动点，会更容易建立直觉。
这些材料不是一张必须依次完成的课程表。做程序验证，可以优先看 Software Foundations；研究静态分析，可以先跟着南京大学《软件分析》建立直觉，再借 MIT Press 的教材向抽象解释深入；只想读懂论文中的语义定义，博客系列和 Cornell 的课程材料已经足够作为下一步。
八、本篇小结
形式化（formalization）入门最重要的不是掌握多少数学，而是形成一种阅读顺序：
\[\boxed{ \text{对象} \longrightarrow \text{关系} \longrightarrow \text{规则} }\]先找“定义了什么对象”，再看“对象之间有什么关系”，最后才看“规则如何计算”。对应到论文中，就是三个具体问题：
- 作者定义了哪些对象？
- 这些对象通过集合、元组或映射形成了什么结构？
- 算法如何查询、转换或更新这些结构？
对刚开始阅读程序分析论文的学生，可以先建立下面这条直觉：
\[\text{Formalization} \approx \text{用集合、映射和规则精确描述算法}.\]当你看到
\[\sigma:X\rightarrow V\]时，不必把它看成一串陌生符号，直接读成：
程序状态把每个变量映射到一个值。
当你看到
\[[\![x=e]\!](\sigma) = \sigma[x\mapsto[\![e]\!](\sigma)]\]时，也不用把它当作复杂数学。它说的是：
计算右侧表达式，然后用结果更新变量 $x$。
能在公式、自然语言和伪代码之间完成这样的转换，就迈过了阅读软件工程形式化定义的第一道门槛。