形式语义学

形式语义学
形式语义学是程序设计理论的组成部分。以数学为工具,运用符号和公式,严格地定义程序设计语言的语义,使语义形式化。

正文

程序设计理论的组成部分。它以数学为工具,运用符号和公式,严格地定义程序设计语言的语义,使语义形式化,故称形式语义学。程序设计语言是用来和计算机系统进行通信,并控制其工作的人工语言。作为语言,人工语言和自然语言(如汉语、英语等)一样,有其语法、语义和语用范畴。程序设计语言的语法是指程序的组成规则,语义是指程序的含义;对于语用则说法不一,大致指程序的使用效果。
形成和历史  为了正确、有效地使用程序设计语言,必须了解语言中各个成分的含义,并且要求计算机系统执行这些成分所产生的效果与其含义完全一致。程序设计语言的语义通常是由设计者用一种自然语言非形式地解释的,实施者和使用者依据各自的理解实现和使用这种语言。但是,使用自然语言和非形式的方法解释语义,容易产生歧义现象,造成语言设计者、用户和实施者对语义的不同理解,影响语言的正确实施和有效使用。程序设计语言中的过程调用语句就是这方面的一个典型例子。人们发现对过程调用语句的非形式的解释可能导致各种不同的理解,产生多种不同的效果。
人们对语义精确解释的要求产生了形式语义学,形式语义学的研究始于60年代初期,在程序设计语言ALGOL60的设计中,第一次明确区分了语言的语法和语义,并使用巴科斯-瑙尔范式成功地实现了语法的形式描述。语法的形式化大大推动了语义形式化的研究,围绕ALGOL60的语义出现了形式语义学早期的研究热潮。