什么是形式语义学?

[拼音]：xingshi yuyixue

[外文]：formal semantics

程序设计理论的组成部分。它以数学为工具，运用符号和公式，严格地定义程序设计语言的语义，使语义形式化，故称形式语义学。程序设计语言是用来和计算机系统进行通信，并控制其工作的人工语言。作为语言，人工语言和自然语言（如汉语、英语等）一样，有其语法、语义和语用范畴。程序设计语言的语法是指程序的组成规则，语义是指程序的含义；对于语用则说法不一，大致指程序的使用效果。

为了正确、有效地使用程序设计语言，必须了解语言中各个成分的含义，并且要求计算机系统执行这些成分所产生的效果与其含义完全一致。程序设计语言的语义通常是由设计者用一种自然语言非形式地解释的，实施者和使用者依据各自的理解实现和使用这种语言。但是，使用自然语言和非形式的方法解释语义，容易产生歧义现象，造成语言设计者、用户和实施者对语义的不同理解，影响语言的正确实施和有效使用。程序设计语言中的过程调用语句就是这方面的一个典型例子。人们发现对过程调用语句的非形式的解释可能导致各种不同的理解，产生多种不同的效果。

人们对语义精确解释的要求产生了形式语义学，形式语义学的研究始于60年代初期，在程序设计语言ALGOL60的设计中，第一次明确区分了语言的语法和语义，并使用巴科斯－瑙尔范式成功地实现了语法的形式描述。语法的形式化大大推动了语义形式化的研究，围绕ALGOL60的语义出现了形式语义学早期的研究热潮。

美国斯坦福大学J.麦克阿瑟于1962年系统地论述了程序设计语言语义形式化的重要性，以及它同程序的正确性、语言的正确实施等的关系，并提出在形式语义学研究中使用抽象语法和状态向量等方法。

通常的程序设计语言的语法是规定程序组成方法的一些规则，称为具体语法，但在定义程序的语义时，必须首先识别给定的程序，分析程序的语法结构。因此，在形式语义学中使用一种讨论程序分解的语法规则，这种语法称作抽象语法。不同的程序设计语言往往使用不同的记号和表示方式。形式语义学提供的方法适用于一切程序设计语言，故抽象语法采用的记号和表示方式也是具体语法的一种抽象。

在定义程序设计语言的语义时，需要一种定义语义的语言，这种语言称为元语言。元语言可以采用已有的数学语言，也可以是以数学理论为基础的专门设计的语言，因此元语言的语义是严格的。

用程序设计语言编写的程序，规定对计算机系统中数据的一个加工过程，形式语义学的基本方法是将程序加工数据的过程及其结果形式化，从而定义程序的语义。

由于形式化中侧重面和使用的数学工具不同，形式语义学可分为四大类。

（1） *** 作语义学：着重模拟数据加工过程中计算机系统的 *** 作；

（2）指称语义学：主要刻划数据加工的结果，而不是加工过程的细节；

（3）公理语义学：用公理化的方法描述程序对数据的加工；

（4）代数语义学：把程序设计语言看作是刻划数据和加工数据的一种抽象数据类型，使用研究抽象数据类型的代数方法，来描述程序设计语言的形式语义。

形式语义学与软件工程密切关联，是其基础理论之一。从形式语义学的观点看，软件工程中的软件要求和软件说明是在不同详尽程度上对程序语义的刻划，程序正确性是讨论程序的语义和预期目标的一致；自动程序设计则是研究如何将一种元语言刻划的程序的语义自动转换为用另一种语言刻划。泛函式程序设计语言和逻辑程序设计语言的研究以及根据语言的语义定义自动生成语言编译系统的研究受到人们重视。在新一代程序设计语言的设计中，语言的形式定义将先于并指导语言的具体设计和实施，形式语义学将发挥更大的作用。

参考书目

J.McCarthy， Towards ɑ Mathematical Science of Computation， Information Processing， North-Holland Pub.，Amsterdam，1963.