操作语义（Operational Semantics）

操作语义是一种赋予编程语言精确含义的形式化方法，它用一组推理规则描述程序如何从一个状态转移到下一个状态，从而把程序的意义定义为它的执行过程本身。

概述

操作语义由戈登·普洛特金（Gordon Plotkin）在结构化操作语义的框架下系统化。相比指称语义把程序映射为抽象数学对象，操作语义更贴近直觉，直接描述抽象机器如何一步步求值表达式或执行语句，因而在语言实现和教学中广受欢迎。

核心特点

• 小步语义：也称结构化操作语义，用单步转移关系描述每一次最小的计算动作，可精细刻画中间状态与并发交错。
• 大步语义：也称自然语义，直接给出表达式最终求值到什么结果，忽略中间步骤，适合描述整体输入输出关系。
• 推理规则：用形如前提在上结论在下的规则集合定义合法的转移，通过规则归纳进行证明。
• 配置：通常是程序片段与内存状态的组合，转移在配置之间进行。

应用场景

操作语义广泛用于编程语言标准的形式化规范、编译器与解释器的正确性证明、类型系统的可靠性证明。它是类型健全性证明中进展定理与保型定理的基础，也常用于并发和分布式系统的建模。许多现代语言的官方规范采用操作语义描述求值行为。

常见问题

问：小步语义和大步语义如何选择？答：若关心中间状态、不终止或并发交错，小步语义更合适；若只关心最终结果、程序总能终止，大步语义更简洁。两者可以证明相互一致。

问：操作语义能证明程序正确吗？答：它本身提供的是程序如何执行的严格定义，配合归纳法可证明语言性质如类型安全，但具体某个程序满足需求还需结合规约与验证手段。