形式语义学（formal semantics），是程序设计理论的组成部分，以数学为工具，利用符号和公式，精确地定义和解释计算机程序设计语言的语义，使语义形式化的学科。形式语义学是从20世纪70年代开始发展出来的一个理论阵营。最初的研究开始于蒙太古以数理逻辑方法对英语的研究，后来经过语言学家和哲学家的共同努力，发展成为一个独立的学科，并且摒弃了蒙太古对生成语言学的句法学的忽视，强调语义解释和句法结构的统一，从而最终成为生成语言学的语义学分支。

形式语义学是指用数学方法精确刻画计算机语言的语义；尤其指用形式系统严格定义出的语言的语义。形式语义学是软件工程学的基础理论之一；语言的形式语法和形式语义已成为程序设计语言的必要组成部分。在形式语义学基础上；形式规范、程序变换、编译自动化等研究都取得了丰硕的成果。程序设计语言的语义通常是由设计者用一种自然语言非形式地解释的；实现者和使用者依据各自的理解去实现和使用这种语言。人们发现对过程调用语句的非形式解释可能导致各种不同的理解；产生多种不同的效果。为了正确、有效地使用程序设计语言；必须了解语言中各个成分的含义；并要求计算机系统执行这些成分所产生的效果与其含义完全一致；人们这种对语义精确解释的要求便产生了形式语义学。形式语义学是对形式语言及其句子采用形式系统方法进行语义定义的学问。需要形式语义研究的原因有以下几点：1、帮助理解语言；2、支持语言标准化；3、指导语言设计；4、帮助编写编译器和语言系统 ；5、支持程序验证和软件可靠性；6、有助于软件规范化。

为了正确、有效地使用程序设计语言，必须弄清语言中各成分的含义，并且要求计算机系统执行这些成分所产生的效果和它的语义完全一致。由于自然语言存在歧义性，故用自然语言解释程序设计语言的含义容易造成误解，影响语言的正确实现和有效使用。实践证明，必须用形式化的语言和方法精确解释程序设计语言。这种需求产生了形式语义学。20世纪60年代初，在程序设计语言ALGOL60的设计中，第一次明确区分了语言的语法和语义，围绕ALGOL60的语义问题出现了形式语义学早期的研究高潮。

70年代，形式语义学取得重大进展，指称语义、代数语义等理论和方法对程序设计理论有深刻的影响。操作语义、公理语义等研究也开创了新的局面。形式语义学是软件工程学的基础理论之一，语言的形式语法和形式语义已成为程序设计语言的必要组成部分。在形式语义学基础上，形式规范、程序变换、编译自动化等研究都取得了丰硕的成果。

用程序设计语言编写的程序，规定了计算机对数据的加工过程。形式语义学的基本方法是用一种元语言将程序加工数据的过程及其结果形式化，从而定义程序的语义。根据所用数学工具和研究重点，形式语义学可分为四大类。

通过语言的实现方式定义语言的语义，也就是将语言成分所对应的计算机的操作作为语言成分的语义。因为语言的语义应该是标准的，不应依赖于特定的计算机系统，或一种具体的实现方式，因此，操作语义学使用抽象机和抽象解释程序来定义语言的语义。

通过执行语言成分所要得到的最终效果来定义该语言成分的语义。指称语义学方法认为语言成分的含义是语言成分本身固有的，不依赖于具体实现该语言成分的计算机。对同一种语言成分，不同的计算机的执行实现过程可以不同，但所产生的最终效果应该是相同的。这种最终效果被看作是语言成分所指称的外在物体，称作语言成分的指称物。指称物多为数学对象，如整数、集合、函数等。指称语义学方法在定义语言的语义时，先确定指称物，然后给出语言成分到指称物的语义映射，这种映射必须满足两个条件：每个语言成分都对应有指称；复合成分的指称只依赖于它的子成分的指称。论域理论是指称语义学方法的数学基础。

用代数公理刻划语言成分的语义，只要研究抽象数据类型的代数规范。抽象数据类型的代数规范通过构造算子和一组有关运算的代数公理刻划类型操作的行为。在论证这种规范满足协调性和完全性的基础上，通过寻找适当的模型代数，可以定义一个抽象类型的不同层次的语义，如初始语义、终止语义等，然后就可以用普通的代数方法论证规范的正确性和实现的正确性，从而形成的一门专业的自然学科。

通过使用数学中的公理化方法，用公理系统定义程序设计语言的语义。另外，公理语义学还研究和寻求适用于描述程序语义、便于语义推导的逻辑语言。例如，用时态逻辑定义的语言的公理语义又称为时态语义。典型的公理语义方法是Hoare公理系统。代表人物有R.W.Floyd和C.A.R Hoare;如果掌握了形式语义学里面的数学理论、方法和概念，就可以用它们去创造规则、刻画规则和证明规则，从而可以描述和推导各类程序设计语言的各种成分和性质。

回顾过去，计算语言学主 要停留在语形处理上，而理论语言学可以为句法结构分析提供成熟的理论支持，因而语言学和计算语言学合作很多。随着语形处理技术日趋成熟，其技术潜力也基本被挖掘殆尽，比如词性标注、汉语词的切分、机器翻译等，近年以来，进展缓慢。互联网上的信息搜索，主要采用的是语词匹配技术语音识别与合成软件，也多是基于对语音的物理属性分析。计算语言学家冯志伟教授曾指出形式语义是理论语言学与计算语言学之间的桥梁。没有形式语义学做中介，理论语言学很难直接与计算语言学中的自然语言语义处理做“无缝对接”，这使得形式语义学在这个信息技术时代显得尤为重要。