Question

在语言学中，语义学（semantics）研究的是单词和它们含义之间的关系：单词“dog”是纸上一些符号的组合，或是由某个人声带引起的一系列空气振动，这与真正的狗或者通常意义上狗的概念极为不同。语义不止关注抽象含义本身的基本性质，还关注具体的记号如何与它们的抽象含义关联起来。

计算机科学里，形式语义学注重找到确定程序难以捉摸的含义的方法，并利用这些方法发现或者证明编程语言中有趣的东西。形式语义学得到了广泛应用，从定义新的语言和进行编译优化这种具体的应用，到构造程序正确性的数学证明这样更抽象的领域不一而足。

为了完整地定义编程语言，我们需要：语法，描述程序看起来是什么样的；语义（semantics）1，描述程序的含义。

1在讨论编程语言理论的环境下，单词 semantics 通常被当作单数对待：我们通过为语言赋予语义来描述这种语言的含义。

许多语言都没有官方的书面规范，而只有一个可用的解释器或者编译器。Ruby 本身算是“靠实现规范”这一类：尽管有很多关于 Ruby 应该如何工作的书和教程，但这些资料的最终源头都是松本行弘先生（Matz）的 Ruby 解释器（MRI，Matz's Ruby Interpreter），这是Ruby 的参考实现。如果任何一份 Ruby 文档与 MRI 的实际行为不一致，那必然是文档错了；JRuby、Rubinius 以及 MacRuby 这些第三方实现都只能努力地精准模拟 MRI 的行为，只有如此，它们才可以声称自己与 Ruby 语言有效地兼容。其他像 PHP 和 Perl 5 这样的语言，也使用了这种以实现为主导的语言定义方法。

另一种描述编程语言的方法，就是写一份平实的官方规范（一般是英语的）。C++、Java 以及 ECMAScript（JavaScript 的标准版本）都使用了这种方法：这些语言的标准化通过由专家委员会写成的、与实现无关的文档来完成，而且会存在很多与这些标准兼容的实现。比起只是依赖于一个参考实现，用官方文档规范定义一种语言更为严谨：这样所做的设计决策更有可能是经过深思熟虑、进行理性选择之后的，而不是某一个特定实现的意外结果。

但是，规范通常非常难懂，而且很难讲规范中是不是含有矛盾、疏漏和有歧义的地方。特别是一份英语规范没有形式化的方法可以进行推导，我们只能完整彻底地阅读规范，大量地思考，然后寄希望于这样就可以掌握所有的前因后果。

Ruby 1.8.7 的规范确实存在，甚至已经被接受为 ISO 标 准了（ISO/IEC 30170）2。尽管 mruby 工程（https://github.com/mruby/mruby）尝试构建一份轻量级、嵌入式的 Ruby 实现，并且明确声明将与 ISO 标准而不是 MRI 兼容，但 MRI 仍然被认为是 Ruby 语言由实现定义的权威规范。

2尽管访问 ISO/IEC 30170 需要支付费用，但这一规范的一份早期草案可以免费下载：http://ipa.go.jp/osc/english/ruby/。

第三种方法是使用形式语义学中的数学方法准确描述编程语言的含义。它的目标是不仅能用适合系统分析甚至自动化分析的格式写出规范，还能保证其完全没有歧义，这样就可以对规范是否一致、是否含有冲突，以及是否有疏漏进行全面检查。在介绍如何处理语法之后，我们将会看到语义规范的这些形式化方法。