编程语言的形式语义

编程语言

语言有两大要素——语法和语义，语法是看得见的表面的形式，语义是真正想表达的背后的含义。各种五发八门的不同的编程语言，其表面形式可以天差地别，但其背后的语义却是相通的。只有使计算机「理解」了人类想表达的东西，才有可能准确给出人类想要的结果。当然也需要计算机拥有对应的计算能力，这正是计算理论所研究的内容，各种计算模型，如有限状态自动机，下推自动机，图灵机，确定性的，不确定性的等等，计算能力的确有差别。不过这一切的前提是你得想办法把自己的想法「告诉」计算机，这就绕不开计算机程序的语义。

形式语义

形式语义试图精确地、无歧义地描述程序的含义，并利用这些含义研究程序的性质。现实中，程序的语义通常有两种方式描述：一种是靠实现规范，如Ruby解释器有一个参考实现；另一种是写一份平实的官方规范，如C++/Java/ECMAScript。

而从更加形式化也更加数学化的角度看，描述程序可以由三种语义：操作语义、指称语义和公理语义。

操作语义

操作语义为程序在某种机器的执行定义一些规则，来捕捉编程语言的含义。这个机器通常是一种抽象的机器：为了解释这种语言所写的程序如何执行，而设计出来的一种想象的、理想化的计算机。操作语义又分为小步操作语义和大步操作语义。

小步操作语义

假想一台机器，用这台机器直接按照这种语言的语法进行操作一小步ー小步地对其进行反复规约，从而对一个程序求值。这种语义相当于为程序实现了一种迭代式的解释器。

大步操作语义

大步语义的思想是，定义如何从一个表达式或者语句直接得到它的结果。这必然需要把程序的执行当成一个递归的而不是迭代的过程。也就是说，为了对一个更大的表达式求值，我们要对所有比它小的子表达式求值，然后把结果结合起来得到最终答案。这种语义相当于为程序实现了一种递归式的解释器。

指称语义

用一种更低级更形式化的语言，或者至少比被描述的语言更好理解的语言，来描述新的语言。它更抽象，与操作语义更像解释器相比，它更像编译器。

公理语义

通过在语句执行前后，分别给出抽象机器状态的断言，来描述一个语句的含义：如果前置条件在语句执行前初始化为true，那么执行后的后置条件也保证为true。公理语义主要用于验证程序的正确性。