形式语义学

形式语义学（formal semantics），是程序设计理论的组成部分，以数学为工具，利用符号和公式，精确地定义和解释计算机程序设计语言的语义，使语义形式化的学科。

在计算理论中，形式语义学是关注计算的模式和程序设计语言的含义的严格的数学研究的领域。

语言的形式语义是用数学模型去表达该语言描述的可能的计算来给出的。

提供程序设计语言的形式语义的方法很多，其中主要类别有：

• 指称语义学，着重于语言的执行结果而非过程，包括域理论；

• 操作语义学，例如抽象机（象SECD抽象机），着重于描述语言的过程；

• 公理语义学，如 谓词变换语义学和代数语义学。