Question

对于为计算机程序赋予含义的问题，本章已经展示了几种不同的方法。在每种情况下，我们都已经避免了数学化的方法并使用 Ruby 了解了它们的策略，但是形式化的语义通常都是由数学化的工具完成的。

2.5.1　形式化

我们对形式语义的研究并不是特别正式。一直没有认真关注过数学符号，而使用 Ruby 作为元语言意味着比起理解程序的各种方式，我们更关注执行程序的不同方式。合适的指称语义关注的是通过把程序转换成定义良好的数学对象以获得程序的核心含义，关心的是把一个 Simple 的«while»语句无歧义的完整表示成一个 Ruby 的while 循环。

为了提供对指称语义有用的定义和对象，专门发展了称为域理论的数学分支，它采用基于单调函数上不动点的一种计算模型，并且这个单调函数定义在偏序集合上。我们可以通过把程序“编译”成数学函数来理解这个程序，并且域理论的技巧还能用来证明这些函数一些有趣的特性。

另一方面，尽管我们只是用 Ruby 含糊地概括了一下指称语义，但关于操作语义，我们已经在精神上接近它的形式化表示了：我们对方法 #reduce 和 #evaluate 的定义实际上只是用 Ruby 翻译的数学化推理规则。

2.5.2　找到含义

形式化语义的一个重要应用是为一种编程语言的含义给出一个无歧义的定义，而不是让其依赖于像自然语言规范文档和“由实现规范”这样更加随意的方法。形式化的定义还有其他用途，例如证明某种语言通常情况下的特性，以及特定程序在特定情况下的特性，证明语言中程序之间的等价性，研究如何在不改变程序行为的情况下安全地变换程序而使其效率更高。

例如，既然操作语义与解释器的实现极为接近，那么计算机科学家就可以把一个适当的解释器看成一种语言的操作语义，然后证明它在那种语言的指称语义方面的正确性——这意味着证明了由解释器给出的含义和由指称语义给出的含义之间存在着明显的联系。

指称语义的一个优点是比操作语义抽象层次更高，它忽略了程序如何执行的细节，而只关心如何把它转换成一个不同的表示。例如，如果存在一种指称语义可以把两种语言翻译成某种共通的表示，就使对不同语言写成的两个程序进行比较成为可能。

抽象程度会使指称语义看起来有点兜圈子。如果问题是如何解释一种程序设计语言的含义，那么把一种语言翻译成另一种语言是如何让我们更接近问题答案的呢？一个指称只不过与它的含义一样好；尤其是，如果指称的语言有某种操作性的含义，那么一个指称语义只是让我们更接近于能实际执行一个程序，这个语言的语义本身展示了它是如何执行的，而不是如何翻译成另一种语言的。

形式化的指称语义使用抽象的数学对象（通常是函数）来表示表达式和语句这样的编程语言结构，并且因为数学上的约定会规定如何对函数求值这样的事情，这就有了一种直接在操作意义上思考指称的方式。我们已经使用了不太正式的方式，把指称语义看成是一种语言到另一种语言的编译器，而事实上这是多数编程语言最终得以执行的方式：一个 Java 程序将会由 javac 编译成字节码，字节码将会被 java 的虚拟机即时编译成 x86 的指令，然后一个 CPU 会把每一条 x86 指令解码成类 RISC（精简指令集）的微指令放到一个核上去执行……它会在什么地方结束呢？是编译器，还是虚拟机，还是一直重复下去？

当然程序最终会执行，因为语义这个高楼会到达底部暴露出实际的机器：半导体中的电子，它们遵守的是物理法则。18 一台计算机是维护这个不确定结构的装置，大量复杂的解释层在彼此之上保持稳定平衡，这就允许多点触控手势这样人体尺度的想法和 while 循环这样的想法，都能被逐渐地向下翻译给硅和电的物理世界。

18或者，在 Charles Babbage 设计的分析机这种机械计算机的场景下，是齿轮和纸遵守物理规律。

2.5.3　备选方案

本章你已经看到了许多不同名称的语义类型。小步语义还叫结构化操作语义（structuraloperational semantic）和转换语义（transition semantic）；大步语义更普遍的叫法是自然语义（natural semantic）或者关联语义（relational semantic）；而指称语义还可以称为不动点语义（fixed-point semantic）或者数学语义（mathematical semantic）。

还有其他类型的形式语义可用。其中一个就是公理化语义（axiomatic semantic），它通过在语句执行前后分别给出抽象机器状态的断言来描述一个语句的含义：如果一个断言（前置条件）在语句执行前初始是 true，那么随后的其他断言（后置条件）将是 true。公理化语义在验证程序的正确性方面很有用：随着语句合到一起组成更大的程序，它们对应的断言也能合到一起组成更大的断言，其目标就是表明对一个程序总体的断言与它的预期定义匹配。

虽然细节有所不同，但是公理化语义是描述 RubySpec project 最好的语义类型，RubySpec project（http://www.rubyspec.org）是“Ruby 程序设计语言的可执行规范”，它使用 RSpec类型的断言既描述 Ruby 的核心以及标准库，又描述 Ruby 内置语言结构的行为。例如，下面是 RubySpec 描述 Array#<< 方法的片段：

describe "Array#<<" do
  it "correctly resizes the Array" do
    a = []
    a.size.should == 0
    a << :foo
    a.size.should == 1
    a << :bar << :baz
    a.size.should == 3

    a = [1, 2, 3]
    a.shift
    a.shift
    a.shift
    a << :foo
    a.should == [:foo]
  end
end