第4章：语义（程序的含义） Semantics: What Programs Mean

一、导读

如果语法定义了程序的书写形式，那么语义则决定了程序执行时的行为。一段语法完全合法的代码，其含义可能因语言的语义规则不同而大相径庭。例如，1 + "2" 在 JavaScript 中结果是字符串 "12"，而在 Java 中会导致编译错误。这种差异正是语义层面的区别。

形式化语义为编程语言提供了精确的、无歧义的含义定义。它不仅是语言规范的基础，也是编译器实现、程序验证和语言理论研究的理论支撑。

学习目标：

理解三种主要语义描述方法的核心思想

掌握操作语义的基本概念和应用

了解指称语义的数学基础

理解公理语义与程序正确性证明的关系

了解静态语义与类型检查的作用

核心问题： 如何精确地定义一段程序"做了什么"？不同的语义描述方法各有什么优势和适用场景？

二、核心概念详解

2.1 操作语义（Operational Semantics）

操作语义通过定义抽象机器在执行每条语句时的状态变化来描述程序含义。它是三种语义方法中最直观的一种，直接模拟程序的执行过程。

大步操作语义（Big-Step/Natural Semantics）：

直接描述一条语句从初始状态到最终状态的完整执行效果，表示为 <语句, 初始状态> => 最终状态。例如：

<x = 3 + 4, σ> => σ[x ↦ 7]

表示在状态 σ 下执行 x = 3 + 4 后，得到新状态 σ'，其中 x 的值为 7。

小步操作语义（Small-Step/Structural Operational Semantics）：

将执行过程分解为一系列单步转换，每一步只执行一个原子操作，表示为 配置1 → 配置2。例如：

x = 3 + 4 => x = 7 => skip

小步语义能够更精细地描述执行过程中的中间状态，适合分析并发程序和程序的非终止行为。

操作语义的优点是直观易懂，与编译器的实际实现方式接近。大多数编程语言的规范文档采用操作语义来描述语言行为。

2.2 指称语义（Denotational Semantics）

指称语义将程序片段映射到数学对象上，通过组合各个部分的含义来构建整体意义。其核心原则是组合性（Compositionality）：复合程序的含义由其组成部分的含义唯一确定。

在指称语义中，每个语法构造都被赋予一个数学含义（称为"指称"或"denotation"）：

• 基本类型的值映射到数学域（如整数映射到数学整数集 Z）
• 变量映射到存储位置
• 表达式映射到从状态到值的函数
• 语句映射到从状态到状态的函数（或偏函数，以处理非终止情况）

例如，赋值语句 x := e 的指称可以定义为：

C[[x := e]] = λσ. σ[x ↦ E[[e]]σ]

表示一个函数，该函数接受状态 σ，将 e 在 σ 中的值绑定到 x 上，返回新状态。

指称语义的数学严格性使其特别适合形式化验证和语言等价性证明。如果两个程序具有相同的指称，则它们在所有上下文中行为相同。

2.3 公理语义（Axiomatic Semantics）

公理语义不直接定义程序的含义，而是通过逻辑断言来刻画程序的行为。其核心工具是霍尔逻辑（Hoare Logic），使用三元组 {P} S {Q} 来描述语句 S 的行为：

• P（前置条件，Precondition）：执行 S 之前的断言
• S（语句，Statement）：被执行的程序语句
• Q（后置条件，Postcondition）：执行 S 之后的断言

例如：{x = 5} x = x + 1 {x = 6} 表示如果执行前 x 等于 5，执行 x = x + 1 后 x 等于 6。

霍尔逻辑提供了一组推理规则，用于从程序的语法结构推导出正确的霍尔三元组：

• 赋值公理：{Q[x ↦ E]} x = E {Q}
• 顺序规则：从 {P} S1 {R} 和 {R} S2 {Q} 推出 {P} S1; S2 {Q}
• 条件规则：从 {P ∧ B} S1 {Q} 和 {P ∧ ¬B} S2 {Q} 推出 {P} if B then S1 else S2 {Q}
• 循环规则：使用循环不变式（Loop Invariant）来证明循环的正确性

2.4 静态语义（Static Semantics）

静态语义是在编译期检查的程序性质，不涉及程序的运行时行为。最重要的静态语义检查是类型检查（Type Checking）。

类型系统为程序中的每个表达式赋予一个类型，并定义了一组规则来判断程序是否"类型安全"。类型检查的目标是在编译期发现潜在的类型错误，防止运行时出现类型不匹配的问题。

静态语义还包括：

• 变量在使用前是否已声明
• 常量是否被重新赋值
• break/continue 是否出现在合法的上下文中
• 模式匹配是否穷尽了所有情况

2.5 动态语义（Dynamic Semantics）

动态语义描述程序在运行时的行为，包括：

• 表达式的求值顺序
• 副作用的发生时机
• 异常和错误的处理
• 并发执行的交错语义

动态语义与操作语义密切相关，但更关注语言规范层面而非实现层面。

三、深入分析

3.1 求值顺序（Evaluation Order）

求值顺序是语义中一个容易被忽视但极其重要的问题。当表达式包含多个子表达式时，子表达式的求值顺序可能影响程序的行为（特别是当子表达式有副作用时）。

int i = 0;
int a[] = {1, 2, 3};
int result = a[i++] + a[i++] + a[i++];

在 C 语言中，这个表达式的行为是未定义的（Undefined Behavior），因为 C 标准没有规定加法操作数的求值顺序，也没有规定副作用何时生效。不同编译器可能产生不同的结果。

Java 明确规定操作数从左到右求值，因此上述代码在 Java 中结果是确定的（1 + 2 + 3 = 6）。

Haskell 采用惰性求值（Lazy Evaluation），表达式只在需要时才求值，且每个表达式只求值一次。这种求值策略使得程序可以处理无限数据结构，但也带来了空间泄漏的风险。

3.2 副作用与引用透明性

副作用（Side Effect）是指表达式求值过程中对状态产生了可观察的改变，包括：

• 修改变量的值
• 进行 I/O 操作
• 抛出异常
• 修改全局数据结构

引用透明性（Referential Transparency）是指表达式的值只取决于其子表达式的值，不依赖于外部状态。纯函数式语言（如 Haskell）追求完全的引用透明性，这使得程序推理和编译器优化变得更加容易。

命令式语言中，副作用是不可避免的，但良好的编程实践建议限制副作用的范围。例如，将副作用集中在 I/O 边界，保持核心计算逻辑的纯粹性。

3.3 语义等价与程序变换

两个程序是语义等价的，如果它们在所有输入上产生相同的行为。语义等价是编译器优化和程序重构的理论基础。

常见的语义等价变换包括：

• 常量折叠：3 + 4 替换为 7
• 死代码消除：删除永远不会执行的代码
• 公共子表达式消除：a = b + c; d = b + c 替换为 a = b + c; d = a
• 循环不变量外提：将循环中不变的计算移到循环外部

编译器必须保证这些变换不改变程序的语义，这是编译器正确性的核心要求。

四、实践案例

案例1：用霍尔逻辑证明循环正确性

计算从 1 到 n 的整数之和：

// 前置条件：n >= 0
int sum = 0;
int i = 1;
while (i <= n) {
    sum = sum + i;
    i = i + 1;
}
// 后置条件：sum = n*(n+1)/2

选择循环不变式 I: sum = (i-1)*i/2 ∧ i >= 1：

初始化：进入循环前，sum = 0, i = 1，满足 0 = 0*1/2 ∧ 1 >= 1

保持：假设进入循环体时不变式成立且 i <= n，执行后 sum' = sum + i = (i-1)*i/2 + i = i*(i+1)/2，i' = i + 1，代入不变式得 sum' = (i'-1)*i'/2，成立

终止：循环结束时 i > n，结合不变式 sum = (i-1)*i/2，由于 i = n + 1，得 sum = n*(n+1)/2

案例2：惰性求值的优势与陷阱

Haskell 的惰性求值允许定义无限列表：

fibs = 0 : 1 : zipWith (+) fibs (tail fibs)
take 10 fibs  -- [0,1,1,2,3,5,8,13,21,34]

fibs 定义了斐波那契数列的无限序列，但 take 10 只强制求值前 10 个元素。惰性求值使得我们可以用声明式的方式描述无限结构，只在需要时计算具体值。

然而，惰性求值也可能导致空间泄漏。当中间结果被延迟但又被引用时，它们会在内存中累积，直到被强制求值。Haskell 提供了严格求值注解（! 和 seq）来控制这种情况。

五、常见误区

误区1：语法相同意味着语义相同

不同语言中相同的语法可能有完全不同的语义。例如 for 循环在 C 和 Python 中的行为截然不同：C 的 for 是通用的循环结构，而 Python 的 for 是迭代器模式。== 在 Java 中比较引用，在 Python 中比较值。阅读新语言代码时，必须了解其语义规则，不能仅凭语法推测。

误区2：操作语义就是编译器的实现方式

操作语义是对语言行为的抽象描述，而非编译器的具体实现。编译器可以自由选择不符合操作语义描述的执行策略，只要最终的可观察行为与语义规范一致。例如，编译器可以将尾递归优化为循环，虽然操作语义描述的是递归调用，但可观察行为是等价的。

误区3：指称语义太抽象，没有实际用途

指称语义虽然高度数学化，但它为语言设计和编译器验证提供了严格的理论基础。指称语义的组合性使得我们可以独立验证各个语言构造的正确性，然后组合得到整体正确性。许多编译器的形式化验证工作都基于指称语义框架。

误区4：未定义行为只是"编译器的问题"

未定义行为（Undefined Behavior）是语言语义层面的概念，不是编译器实现的缺陷。C 语言中故意留下未定义行为，是为了给编译器优化留出空间。然而，未定义行为是安全漏洞的重要来源。现代语言（如 Rust、Java）通过更严格的语义定义来消除未定义行为，以安全性换取一定的优化空间。

误区5：类型检查属于语法范畴

类型检查是静态语义，而非语法。语法只关心程序的形式结构（如括号是否匹配），类型检查关心的是程序的语义约束（如操作数的类型是否兼容）。一个程序可以语法完全正确但类型检查失败。编译器通常先进行语法分析，再进行类型检查，这是两个独立的阶段。

六、本章小结

本章介绍了三种主要的程序语义描述方法及其在编程语言中的具体应用。操作语义通过状态转换直观地描述程序执行过程，是语言规范文档的常用方法。指称语义借助数学对象提供严格的理论基础，适合形式化验证和语言等价性证明。公理语义通过逻辑断言支持程序正确性证明，是软件验证的重要工具。此外，静态语义（特别是类型系统）在编译期捕获程序错误，动态语义描述运行时的行为特征。求值顺序、副作用和语义等价等概念对于理解编译器优化和程序变换至关重要。掌握这些语义模型有助于我们更深入地理解程序的本质行为，为后续学习类型系统和程序设计语言理论奠定基础。

七、思考题

用大步操作语义描述 if B then S1 else S2 的执行规则。

解释指称语义中的组合性原则，并举例说明为什么它对编译器优化很重要。

使用霍尔逻辑证明以下代码的正确性：给定 n >= 0，计算 n 的阶乘。

比较严格求值和惰性求值的优缺点。各举一个适合使用惰性求值的场景。

什么是未定义行为？为什么 C 语言要保留未定义行为？从安全性和性能两个角度分析。