1 语义的分类

编程语言的语义可以使用两种方式描述：

一种是依赖实现的规范，如解释器有一个参考实现的Ruby。
另一种是其官方规范，如C++/Java/ECMAScript。 

在严格地制定了语言的语法之后，接下来需要一个对如何评估术语的类似精确定义——即，语言。

另一个角度讲，编程语言的设计可以分为两部分：语法和语义。

语法描述了它的外观。

语义描述了它应该做什么。

有很多方法可以使用有效的语法编写程序，但在评估时变得毫无意义。这些无意义的评估称为运行时错误。

语义正式描述了应该如何评估程序。根据其语义格式正确的程序不会卡住。

比如像 .为了充分描述算术语言，我们需要回答三个问题：3+2∗3/2

语法：算术表达式的结构是什么？
静态语义：算术表达式的哪些子集有意义？
动态语义：给定算术表达式的含义是什么？

这些更加形式化也更加数学化的角度看，描述形式化语义有三种主要风格：

 操作语义、指称语义和公理语义，或者 操作式、指称式和公理式。

1.1 操作语义学

它指定编程语言的行为通过为它定义一个简单的抽象机器。 这台机器是“抽象”的，它使用语言的术语作为机器代码的感觉，而不是比一些低级微处理器指令集。

对于简单的语言，机器的状态只是一个术语，机器的行为是定义的通过一个转换函数，对于每个状态，要么给出下一个状态通过对术语执行简化步骤或声明机器已停止。

一个术语 t 的含义可以被认为是最终的机器以 t 作为初始状态启动时达到的状态 .

严格来说，我们这里描述的是所谓的小步操作语义，有时称为结构操作语义（Plotkin，1981）。 还有另一种大步操作样式，有时称为自然语义（Kahn，1987），抽象机的单个转换将术语评估为其最终结果。

有时给出两个或多个不同的操作语义很有用对于单一语言——更抽象一些，机器状态看起来类似于程序员编写的术语，其他术语更接近于由该语言的实际解释器或编译器操作的结构。

证明这些不同机器的行为在某些方面是对应的执行相同程序时的适当意义相当于证明语言实现的正确性。

操作语义学使用的语言是抽象机器的思想，程序的评估是从初始状态到最终状态的一系列状态转换。

转换函数定义状态如何过渡到下一个状态（如果有）。如果没有这样的下一个状态，则计算机要么成功完成其评估，要么面临运行时错误并卡住。在这两种情况下，程序都会停止。

计算机程序中的每个术语都有某种含义，其形式在状态转换完成时最终确定。状态转换可以是单步或多步。

编写操作语义有两种主要方法：小步或大步。

小步语义将行为分解为精细的简化步骤。一个简单的步骤可能无法保证对最终表格进行评估;有时需要多个步骤。

大步语义由多个小步规则组成，这些规则评估为单个规则的最终形式。这样的规则等同于它的多步骤对应物。

由于操作语义是在抽象机器行为之后设置样式的，因此它们可用作实现的参考。

1.2 指称语义学

它对意义采取更抽象的观点：而不是只是一系列机器状态，术语的含义被认为是一些数学对象，例如数字或函数。

为一种语言提供指称语义包括找到一组语义域，然后定义一个解释函数将术语映射到这些域的元素。

寻找合适的语义域用于建模各种语言特征已经产生了丰富而优雅的研究领域称为领域理论。

指称语义的一个主要优点是它从评估的细节，并强调评估的基本概念语言。

此外，所选语义域集合的属性可用于推导程序推理的强大定律行为——例如，证明两个程序具有完全相同的行为，或者一个程序的行为满足某些特定的规则阳离子。

最后，从所选择的语义集合的属性域中，很明显，各种（理想的或不理想的）事物在一种语言中是不可能的。

指称语义使用语言指代数学对象的想法。与操作语义不同，评估和实现细节被抽象出来。

定义解释函数是为了将程序中的术语映射到语义域中的元素（也称为其表示），从而删除原始语法的任何出现。

语义域旨在根据特定的语言特征进行建模，这项研究称为域理论。

通过比较它们的表示法，可以检查两个程序是否相同。

定律可以从语义域派生出来，并用于语言规范以验证实现的正确性。

语义域的属性可用于显示语言中不可能的实例。

1.3 公理语义学

它对这些定律采取了更直接的方法：取而代之的是首先定义程序的行为（通过给出一些可操作的或指称语义），然后从这个定义推导出规律，axiomatic 方法将规律本身作为语言的定义。

一个术语的含义就是可以证明它的东西。

公理化方法的美妙之处在于它们将注意力集中在对程序进行推理的过程上。 正是这种思路给了计算机科学强大的思想，如不变量.

在 20世纪60 年代和 70 年代，操作语义通常被认为是不如其他两种风格——用于快速和复杂的定义语言特征，但不够优雅且在数学上薄弱。

但在 80 年代，越抽象的方法开始遇到越来越棘手的技术问题(指称语义的恶果是非确定论的处理和并发性的处理;对于公理语义，它是过程处理。).比如问题，操作方法的简单性和灵活性来了。

相比之下，越来越有吸引力——尤其是在公开的一些研究人员在该地区的开始新发展，比如

Plotkin的Structural Operational Semantics（1981），
Kahn的Natural Semantics（1987）和Milner关于CCS的工作（1980;1989;1999），

引入了更优雅的形式主义，并展示了在指称语义学背景下发展起来的强大数学技术中有多少可以转移到操作设置。

操作语义已成为本身就是一个充满活力的研究领域，通常是首选方法用于定义编程语言并研究其属性。

公理语义直观地与霍尔逻辑相关。

其规则本身不是从操作或指称行为定义中推导出法律，而是定义语言的语义。

这种逆转简化了对程序的推理，导致了软件验证的发展。

具有相同一组初始和最终断言（定律）的两个不同的程序实现被认为具有相同的语义。

断言之间发生的术语仅用于证明断言本身，对语义没有贡献。

断言定义程序中变量和其他移动部件之间的关系，其中一些断言在整个执行过程中保持不变。这是公理语义学基础的重要不变性概念。

2 小结

语义的分类不仅仅这三个，当然还有其他的语义风格分类，比如代数语义之类的，感兴趣的读者自行查阅，这里不再例举。

自然语义风格（练习 3.5.17）是由卡恩 (1987) 开发。
参见 Astesiano (1991) 和 Hennessy (1990)更详细的发展。
Burstall (1969) 将结构归纳引入计算机科学。

参考

操作语义起源：John McCarthy on Semantics of Lisp （1960）
指称语义起源：Christopher Strachey，Dana Scott关于“迈向计算机语言的数学语义”（1970，1971）
公理语义起源：托尼·霍尔谈霍尔逻辑 （1969）