编程的修炼(中英双语)

    书籍
    计算机书籍
《编程的修炼(中英双语)》是图灵奖获得者Edsger W. Dijkstra在编程领域里的经典著作中的经典。作者基于其敏锐的洞察力和长期的实际编程经验，对基本顺序程序的描述和开发中的许多关键问题做了独到的总结和开发。书中讨论了顺序程序的本质特征、程序描述和对程序行为(正确性)的推理，并通过一系列从简单到复杂的程序的思考和开发范例，阐释了基于严格的逻辑推理开发正确可靠程序的过程。
《编程的修炼(中英双语)》写于20世纪70年代中后期，但其对编程技术领域的开发、编程语言发展和程序理论研究的深刻影响持续至今。本书值得每个关注计算机科学技术的本质，冀求在程序和软件领域有长远发展的计算机工作者、教师和学生阅读。

艾兹赫尔·戴克斯特拉（Edsger W. Dijkstra，1930年5月11日－2002年8月6日），生于荷兰鹿特丹，自喻为荷兰第一个以程序设计作为职业的人。他早年积极推动结构化程序设计，一生致力于将计算（computing）发展为一门科学，在计算机科学技术的诸多领域有开拓性建树，并由于在程序设计基础研究中的卓越贡献获得1972年图灵奖。
裘宗燕，北京大学数学学院教授。主要研究兴趣是软件形式化方法和程序设计的理论基础，也关注程序设计实践。翻译过若干相关著作，包括《从规范出发的程序设计》、《B方法》、《编程原本》、《计算机程序的构造和解释》、《C++语言的设计和演化》等。

《编程的修炼(中英双语)》
序 IX
前言 XI
第0章 执行抽象 1
第1章 编程语言的作用 13
第2章 状态及其特征 19
第3章 语义的性质 29
第4章 一种编程语言的语义特征 47
第5章 两个定理 73
第6章 论完满终止结构的设计 81
第7章 再论欧几里得算法 89
第8章 几个小例子的形式化处理 101
第9章 论受限的非确定性 143
第10章 有关记法的短论：“变量的作用域” 157
第11章 数组变量 187
第12章 线性检索定理 209
第13章 下一个排列 213
第14章 荷兰国旗问题 221
第15章 更新顺序文件 233
第16章 再论归并 245

　　很长时间以来，我一直想写一本基本上是按照本书线索的著作，原因是：一方面，我知道程序可以有迷人的形态和深刻的逻辑之美；另一方面，我又不得不接受这样的事实，即绝大部分程序只是以一种适合机器执行的方式表达，完全没有什么美感，也不适合人们欣赏。这种不满意还有第二个原因，那就是各种算法通常总是以一种完成了的产品形式发表，而在设计过程中起着最重要作用的，以及成为证明所完成程序的最终形式的正当性的各种思考的主要部分，通常都完全没有提及。我最初的想法是以读者能欣赏到它们的美的方式发表一系列优美的算法。对于如何做这件事，我当时的想法是描述一些实际的和想象中的设计过程，使其中的每个过程最终都得到了一个所需的程序。我在一定程度上实现了最初的想法，作为这本专著的核心部分是一系列的章节，每一章处理并解决一个新问题。而在另一方面，最终写出的这本书与我早前的期望又有很大不同，由于我特别希望用一种自然而且方便的方式来展现这些内容，因这种追求而强加给自己的任务变成了一种重要的责任。我将永远为自己完成了这一工作而感到欣慰。
　　在开始写一本像本书这样的著作时，人们立刻会面临一个问题：“我准备使用哪一种编程语言？”而实际上这并不仅仅是一个有关展示形式的问题！任何工具的一个最重要的（而且也是最难琢磨的）方面，就是它对于被训练而将使用它的人们的工作习惯的影响，这种影响——无论我们是否喜欢——是对我们的思考习惯的影响。在尽可能地分析了这种影响的各方面情况之后，我得出了一个结论：没有一个现存的语言，也没有一个它们的子集适合我的目标。其次，我也知道自
　　己完全没有为设计一种新的编程语言做好准备，因此，我曾发誓在随后的五年里不去做这件事。而且我有一种非常清晰的感觉：这个时期还没有过去！（但还有一个前提，就是除了其他事情外，这本书必须要写。）我试着消解这一矛盾的方式是设计了一个适合我的具体目标的小型语言，只做出一些看起来不可能避免，而且其正当性也得到了充分证实的承诺。
　　这种犹豫和自我强加的约束如果被错误地理解，有可能使本书的许多潜在读者对它感到很失望。那些把编程的困难等同于老练地利用那些精细而花哨的称为“高级编程语言”的工具，或者（更糟糕的！）“编程系统”的困难的人们注定会对这本书不满意。如果因为我忽略了所有那些诱人的花哨玩意儿而使他们感到受了骗，我只能回答说：“你真能确定所有那些诱人的花哨玩意儿，以及那些你所谓‘强大的’编程语言的美妙功能确实属于解集合，而不属于问题的集合吗？”我只是希望，即便我用的是一种小型语言，他们也能看看这本书。在做完这件事之后，他们有可能同意，虽然没有那些诱人的花哨玩意儿，仍然有非常丰富的问题需要讨论。因此，是否在一开始就介绍大部分花哨玩意儿，确实是应该质疑的。还有，对于那些明显是对编程语言的设计有兴趣的读者，我只能表示我的歉意。正如我已经做的那样，我没办法在这个问题上做更明确的事情。但在另一方面，我也希望随着时间的推移，这一专著会对他们有所启示，而且能帮助他们避免一些如果没有读过它有可能犯的错误。
　　在写作的过程中——它持续不断地让我感到惊喜和激动——逐渐呈现的文本与我初始时头脑中的想象大不相同。我一开始设想以一种（易理解的）方式去展示程序的开发过程，带上比我在（引论）课程中更多一点的形式化设施，其中以直观的方式介绍所使用的语义，有关正确性的论证采用通常的严格论述，手工编排，再加上有说服力的文字。在为更形式化的方法建立了必要的基础后，我得到了两个惊喜。第一个惊喜就是所谓的“谓词转换器”，作为我选用的工具，它提供了一种方法，使我们可以直接定义初始状态与最终状态之间的关系，不需要参考在程序实际执行中可能经历的中间状态。我对这种情况感到非常欣慰，因为这清晰地区分了程序员的两个主要关注点：数学的正确性（即程序是否定义了初始状态与最终状态之间所需的正确关系——谓词转换器是我们研究这一问题的一种形式化工具，研究中不需要考虑实际的计算进程），以及工程上对于效率的关注（现在也很清楚，这件事只与实现有关）。这已经成为一种最有帮助的发现，因为同一个程序正文总是有两种相当互补的解释：它可以解释为一个谓词转换器的编码，这样做看起来更适合我们的需要；或者解释为可执行代码，我宁愿把这种解释留给机器去做。第二个惊喜是，我能够想象到的最自然而且最系统化的“谓词转换器的编码”，在被看作“可执行代码”时，将要求一种非确定性的实现。有一段时间，我对把非确定性引进单道编程感到不寒而栗（我对它给多道编程带来的复杂性知道得太多了！），直到我认识到，将程序正文解释为一个谓词转换器的编码有其自身的存在理由。（回顾往事，我们可以看到，过去提出的有关多道编程的许多问题并不是别的什么，只不过是不适当地过分强调了确定性的重要性而带来的后果。）我最终认识到，应该把非确定性看作正常情况，这样，确定性将变成一种——并不很有趣的——特例了。
　　在打好了有关的基础之后，我将所有的时间都投入了想做的事情上，也就是说，去解决一系列的问题。做这件事使我得到了未曾预料的快乐。与我以前的工作方式相比，形式化的设施使我能更牢固地把握所做的工作。我很高兴地发现，明确地关注终止性问题能带来许多富于启发性的看法，以至于使我觉得偏向于考虑部分正确性的观点如此常见是非常令人遗憾的。然而，最大的快乐是，对于大部分我原来做过的问题，这次都得到了更漂亮的解答！这是非常令人鼓舞的事情，我将它看作是一种指示剂，说明我所开发的方法确实提升了我的编程能力。
　　应该怎样学习这本专著呢？我能给出的最佳建议就是，一旦看完了问题的描述，就停止阅读，转去试着自己解决它。尝试自己解决问题，是你能自己认识和评价问题的困难程度的唯一方法，它也使你有机会去比较你的解和我给出的解，还给你得到满足的机会，即看到你给出的解比我给出的更好。还是要先说一下，当你发现这里的内容远不是非常容易读的时候，请不要沮丧。研读过这本专著的人都觉得它的内容通常是很难的（但收获也同样很多！）。然而，每次我们分析遇到的困难时，得到的结论都是应该将这种困难“归咎于”实际讨论的问题，而不是有关的文字本身（即它的表达方式）。它的寓意是，一个非平凡的算法本身就是非平凡的，而与论证其设计的正确性的思考相比，在一个编程语言里做出的算法描述是高度紧凑的：不要受到最后的程序正文长度的误导！我的一个助理给出的建议——这也是我忠实地采纳的，因为它可以很有价值——是让学生分为一些小
　　组一起学习这本书。（在这里，我必须对书中正文的“困难程度”加一点附带的说明。我本人科学生涯中的许多年一直在致力于弄清楚程序员的任务，目标是设法使它成为智力上可以管理的工作。从事了多年的这种澄清性的工作之后，我感到好玩，也很吃惊地发现，反复出现的回馈是“我把编程弄得更困难了”。但困难始终在那里，只有将其变为明显可见的，我们才有希望设计出具有高度信任水平的程序，而不仅仅是做出了一些“胡乱涂抹出的代码”，即那种基于根本无法得到支持的假设，准备着被第一个反例推翻的程序正文。不用说，本书的任何一个程序都没有在机器上测试过。）
　　我还要给读者解释为什么我把这里的小型语言弄得这么小，小到没有包含过程和递归。由于任何一点语言扩充都会给这本书增加几章内容，并因此使它也相应地变得更昂贵，所以对于大部分可能的扩充（例如多道编程），我都不需要更多的解释。而过程总是在编程中居于核心的地位，递归对于计算科学而言也是最受学术界重视的标志，因此，我必须给出一些解释。
　　首先，这本专著不是为新手写的，因此，我期望本书的读者熟悉这些概念。其次，本书不是某个特殊编程语言的引论教材，缺乏这些结构和使用它们的例子，不会被解释为我不能或者不希望使用它们，也不会被作为是建议那些有能力使用这些结构的人不要用它们。这里的关键是我觉得在传递想给出的信息时我并不需要这些结构。我想讨论的是应该仔细地分离各种关注，以及为什么从各个方面看这种做法都是设计出高质量程序的最重要的基础。以这里的小型语言作为一种有节制的工具，对于给出各种非平凡而且非常令人满意的设计而言，已经能给我们足够的行动自由了。
　　前面的解释虽然已经很充分，但还不是故事的全部。在任何情况下，我都觉得必须把重复结构本身作为语言中的一种结构，因为在我看来，这样的阐释是早就应该有的东西。当编程语言诞生时，其赋值语句的“动态”性质看起来与传统数学的“静态”性质很不吻合。由于没有合适的理论，数学家就觉得很不喜欢它。而且，由于重复结构是需要变量赋值的最根本原因，数学家也很不喜欢重复结构。当人们开发出没有赋值，也没有重复结构的编程语言——例如，纯LISP——时，许多人都大大地松了一口气。这使他们又可以回到自己熟悉的场地里，看到了一点希望的微光：有可能将编程变成一种具有坚实的而且得到广泛尊重的数学基础
　　的活动。（直到目前，在更偏向于理论的计算科学家中仍然有一种广泛存在的感觉，认为递归程序比基于重复的程序“来得更自然”。）
　　另一种角度就是为“重复结构”和“给变量赋值”提供一种可靠的而且可用的数学基础，为此，我们又必须等待另一个十年。这方面研究的成果是，正如在这本专著里阐释的，一个重复结构的语义可以基于谓词之间的一个递归关系定义，而一个广义递归的语义定义则需要基于谓词转换器之间的一个递归关系。这一点很清楚地说明，为什么我认为广义递归的复杂性比重复结构高一个数量级。因此，我很害怕看到将下面这样重复结构的语义
　　定义为调用
　　其中的whiledo是如下定义的递归过程（用ALGOL 60的语法描述）
　　虽然这样做不错，但它却伤到我了，因为我不喜欢用一把大锤去敲一个鸡蛋，无论用大锤做这件事是多么的有效。对于在20世纪60年代涉足这一问题的那一代理论计算科学家来说，上面的定义常常不仅是“自然的那一个”，而且是“真正的那一个”。应该看到下面的事实：如果不诉诸重复的概念，我们甚至无法定义图灵机能够做什么。这说明需要重新做一些权衡。
　　对于没有参考文献的问题，我不准备解释，也不表示歉意。
　　致谢：下列人士对本书有直接影响，他们或者是提出过本书拟议中的内容的期望，或是请他们为本书（或其中一些部分）写评论：C. Bron，R.M. Burstall，W.H.J. Feijen，C.A.R. Hoare，D.E. Knuth，M. Rem，J.C. Reynolds，D.T. Ross，C.S. Scholten，G. Seegmüller，N. Wirth和M. Woodger。能写下对他们的合作的谢意是我的荣幸。我还要特别感谢Burroughs公司为我提供了机会和各方面的便利，感谢我妻子不断的支持和鼓励。
　　Edsgar W. Dijkstra
　　荷兰Nuenen

　　在本书中，作者以其习惯的文字风格，详尽地描述了他对计算机编程的基本性质的激进的新见解。基于这些见解，作者开发了一套编程方法以及与之相适应的记法工具，并用一大批优雅而且高效的实例展示和检验了它们。本书将注定成为在计算机编程的智力修炼领域发展中最杰出的成就之一。
　　——C.A.R.Hoare
　　

　　第1 章
　　编程语言的作用
　　在“执行抽象”一章中，我非形式化地描述了计算两个（不太大的）正整数的最大公因子的几种不同“机器”的设计。其中一部机器采用在纸板上移动石子的方式；另一部机器基于两个半拉石子，而且它们都在坐标轴上移动；最后一个基于两个寄存器，每个里面可以保存一个（直至某个上限的）整数值。从物理上说，这三台“机器”大相径庭；而从数学上看，它们却很类似，做出这一论断的主要原因是，三者都能计算最大公因子，这是三者的共性。由于这三台机器只不过是同样一组“游戏规则”中不同的具体实现，而实际上，这组规则才是一个发明的核心，该发明就是大名鼎鼎的“欧几里得算法”。
　　在前一章里，欧几里得算法是用一种相当非形式化的方式描述的。有人会提出，由于与之对应的可能计算的数目如此之大，因此，我们必须要有一个关于其正确性的证明。如果一个算法只是以非形式化的方式给出，它就不容易作为一种形式化处理的对象。为了形式化地处理，我们就需要用某种适当的形式化的记法来做算法的描述。
　　这样一种形式化记述技术的可能优势有许多方面。任何记述技术都蕴涵着一个事实：它所实际表述的任何东西都是它有可能描述的那个对象集合（通常是一个无穷集合）的一个特定成员。我们的记述技术当然应该能给出欧几里得算法的一个优雅而简洁的描述，而一旦做好了这件事，也就是把它表示成了一个包含各种算法的巨大的类中的一个成员。而在描述该类中的其他算法时，我们可能期望发现自己所用的记述技术的一些更有趣的应用。对于欧几里得算法，可能会有人说因为它如此简单，用一个非形式化的描述就能对付了。形式化记法的威力应该表现在一些没有它就绝不可能做到的成就方面。
　　形式化记述技术的第二个优势是，它使我们有可能将算法作为一种数学对象来研究，算法的形式化描述将成为我们的智力收获的抓手，使我们能证明一些有关算法类的定理，例如，由于算法所采用的描述而使之共有的一些结构性的性质。
　　最后，这样一种记述技术将使我们能毫无歧义地定义算法，这样，给定了用它描述的一个算法，并给定一组实际参数（输入），有关与之对应的答案（输出）应该是什么，将没有任何疑义或者非确定性。可以断言，相应的计算完全可以用一部自动机器完成：给它该算法（的形式化描述）和相应的实际参数，它就能产生出相应的答案，完全无须进一步的人工干预。这样一种能对付这种相互对应的算法和实际参数的自动机器已经造出来了，它就是人们说的“自动计算机”。为能在计算机上自动执行而写出的算法称为“程序”，而自20世纪50年代后期以来，用于写程序的形式化记述技术就被称为“编程语言”。（与程序的记述技术有关的术语“语言”的引入已受到多方面关注。一方面，现有的语言理论为相关讨论提供了一种很自然的框架和一套有用的术语，如“文法”、“语法”、“语义”等。另一方面，我们也必须注意到，与现存的“自然语言”的类似性也造成了许多误导，因为各种自然语言，无论怎样做形式化，其弱点和威力都来自它们的非明确性和非精确性。）
　　从历史情况看，这最后一个方面，即各种编程语言可以用作指挥现有的自动计算机的媒介，这个事实已经在很长时期里成为它们最重要的属性。现有的自动计算机执行某种特定语言写出的程序的效率，也成为评判该语言的质量的最重要标准。这种情况导致了一个令人遗憾的后果：不难看到，现有计算机的许多很反常的特性都被忠实地反映在现有的编程语言里，为此付出的代价是，用这样一个语言描述的程序是很难用智力去把握的（实际上，即使没有这种情况，编程的工作也已经非常困难了！）。在下面将要提出的方法中，我们将试着重新考虑这方面的平衡。按我们的认识，写出的程序需要实际地由一台计算机执行，这只是由于偶然性而导致的一种实际情况，它不应该居于我们考虑问题的中心。（在最近的一本培养PL/I程序员的教材里，可以看到作者强烈建议尽可能避免过程调用，理由是“因为它们会大大影响程序的效率”。由于过程是PL/I中描述结构的最重要的工具，上述建议实在太可怕了，以至于我完全无法把这本书看作真的能“用于教育”。如果你确信过程是一种有用的概念，而在你的工作环境中，过程机制的实现带来的开销却令人难以忍受，那么应该诅咒的是这些不适当的实现，而不应该是把它们的表现作为一种标准！这方面的权衡确实应该重新做！）
　　我把一种编程语言看作是一种工作媒介，用于描述（可能非常复杂的）抽象机制。正如在有关“抽象执行”一章里可以看到的，算法最突出的优点就在于对它们能够做出的论证的简洁性。我们对于有关机制的信心也是基于这个事实。如果失去了这种简洁性，算法就失去了其（存在的权利）中很大一部分，因此，我们将把保持这种简洁性作为始终如一的目标。另外，我们对所有编程语言的选择也将直面这一目标。