本书详细论述了有关规范程序设计的内容，包括：程序和精化、谓词演算、选择、迭代、构造类型、模块和封装等，最后几章还包含了大量的实例研究和一些更高级的程序设计技术。本书提倡一种严格的程序开发方法，分析问题要用严格方式写出程序的规范，而后通过一系列具有严格理论基础的推导，最终得到可以运行的程序。
　　本书是被世界上许多重要大学采用的教材，适于计算机及相关专业的本科生和研究生使用。

在数学里，等式x2＝1有多种含义，其中之一是它有两个解x＝1和x＝-1。但x=1和x＝一1本身也是等式，其形式上也是由“＝”隔开的两个表达式。既然这三个表述都是等式，那么后两个式子有什么特殊性质，使它们能被认为是问题的解呢
　　作为解应该具有两个特性。首先是它确实解决了某个问题。对于上面的例子，我们可以有如下的图示：这也表明了我们说x＝1“解决了”x2＝1的理由。因为它们之间存在一种蕴涵关系，“如果x＝1，那么x2＝1”(请注意，反向蕴涵在这里并不成立)。对于x＝-1也是如此。
　　解的第二个特性在于它们所确定的值可以直接看到，不需要再经过许多计算，不必再去讨论1是不是x的一个能使x＝1为真的值。无须任何思考就可以看清这个结果。
　　我们也可以用“求解”和“求得的解”这一类术语来分析今天人们所理解的计算机程序设计或程序开发过程。当然，我们在这里遇到的将不是等式而是程序：某些程序将被看作是对另一些程序的求解(我们将称之为“精化”)；另一些程序本身就非常简单，可以看作是所求出的解(这些程序将被称作“代码”)。
　　为“设置x使得x2＝1”等各类语句确定一些特殊的记法形式之后，我们就可以用一种看起来很像是程序设计的方式来写规范。在确定了细心定义的语义之后，我们甚至可以说它们本身“就是”程序。举例来说，上面这个句子所对应规范可以写成“x：[x2＝1]”。程序间的“精化为”关系用“”表示，这就使我们可以画出下面的“被求解”关系图示，与上面图示类似：
　　 这里的三个成分都是程序。解的第一个特性可以从下面说法中看到：“如果需要一个x使x2＝1，那么x:=1就是这样的一个x”。第二个特性也出现在右边程序中——这些程序都是“代码”——它们给出的值可以通过在计算机中运行而得到，根本不需要任何思考。
　　本书将要采用上面这种方式来讲授基本程序设计：我们把规范和代码都看作是程序，程序间有一种称为“精化”的序关系；这里存在着一个特殊的受限子语言，称为“代码”’用代码写出的程序可以“完全不必思考”地直接在计算机上执行。在其他地方则确实需要思考，需要去“发现”能作为给定规范的精化的某些代码。
　　这种方式的基础是Dijkstra、Hoare和Floyd的工作[Dij76，Hoa69，Flo67]。这里要使用的程序设计语言是Dijkstra的“卫式命令”，又扩充了一些为写规范而设置的结构，例如上面的“x：[x2＝1]”。语言本身将在本书的前几章介绍，其中每种结构的特性都用它所满足的一组精化法则刻画，这些结构在计算机上的作用则以非形式的方式描述，作为一种直观的补充。
　　随后的几章包含了一些实例研究和一些更高级的程序设计技术。每个实例研究都完整地处理了一个程序设计问题，使用了到那里已经能使用的方法。这些例子都是众所周知的，并不是非常困难的。高级的程序设计技术包括“过程”、“递归”、“递归数据结构”、“模块”，以及最后的“状态变换”(包括“数据精化”)。
　　此外，还有几章讨论了一些必要的基础性结构，应该特别指出的是谓词演算和基本类型。前者有它自己的法则，附录A里汇集了不少这方面的材料。我们首先设法避免依赖于任何特殊的逻辑证明方法(那些方面的讨论或许应该是另一本完全不同的书的论题)。当然，在导引性的第1章已经用到谓词演算，是在第2章里比较完整地讨论这个问题之前。不过，在这一章讨论的主题是精化演算，而不是谓词演算。另一方面，第2章本身也是完全独立的，如果需要的话也可以先读一读。那里的基本类型都是一些取自普通算术的常见
数集，还增加了幂集、包和序列等。
　　随后有一章是总结，其中综述了我们的程序设计风格的主要特征，还讨论了这种风格对于程序实践中的文档、程序修改、测试和排错等工作的影响。
　　这个总结之后还有几章，那里讨论的问题更高级一些。前两章包含了两个相当复杂的实例研究：第一个与迭代有关(是一个动态规划的例子)，第二个例子包含了一个真正的递归。有关高级论题的第三章是关于规范本身的一个实例研究，在那里我们将把精力集中在模块，(系统)设计、设计的改变等方面，使用常规的精化和数据精化作为细致设计的工具。
　　最后一章给出了有关前面所有材料的语义。
　　附录中包括汇集起来的一些命题和谓词演算法则，一些练习答案，以及对正文中所引进的所有精化规则的总结。最后是一些现成的在推导程序或者研究其他变形的过程中有用的材料，在这里给出就是为在教学过程中复制和分发。准备将这本书用于教学的人可以从出版社得到另一个小册子，其中包含了对精化规则的总结以及对所有练习的答案。
　　本书拟议中的读者包括两种人：那些正在学习程序的人，和那些已经是程序员，但还希望将自己已有的技术与程序规范(这是他们自己程序的源由)联系起来的人。这里的经验来自作者近10年来为计算专业二年级开设本科课程的实践。当然，最好的方法是首先对精化法则有所接触。对初学的编程序者而言，这种精化法则是辅助的，而不是规定性的。在这个学习阶段中，可以将精化法则表作为一种参考，而不是作为证据。有关对迭代使用不变式的学习本身就非常有价值。
　　无论以前是否已经接触过，作为规范，精化和代码各方面的基础性问题都是学生需要依靠的，这些基础还能帮助学生们理解其他课程以及更普遍的计算领域。更有经验的程序员则可能在其他规范和开发方法，例如Z和VDM[Jon86，Hay93，Kin90]里看到过这些特征，对于它们中一些，精化演算是一种附属物，但也可能作为其替代物。
　　与第1版的差别
　　第2版对第1版做了许多重新整理、修改和扩充。
　　前面关于程序设计语言的各章都更新做了安排，使各种语言特征的引入更连贯，也使这些章不受到过于技术性的讨论的干扰。有些技术性内容被推后了，在原来的地方只讨论了程序设计语言本身。
　　讨论过程和参数的那些部分，包括递归过程，都做了相当大的修改，以使其更容易些。付出的代价是少了一点普通性。原来对参数是单独处理的，而现在采用了对(递归)过程和参数一起处理的方式，这样做更方便一些。
　　第2版增加了相当多的新内容，包括有关函数和关系的一节(采用了“Z的风格”)；有关递归类型(比如说，树)，以及关于使用它们的简单控制结构的完整的一章；有关“函数式”精化的一节，这里包括状态转换的一种特殊情况和一种非常一般的情况，其中的法则比完全一般的情况要简单得多；还有两个“高级的”实例研究，再加上技术方面的递归和数据精化；这些都是实质性的改动。
　　书中增加的第一个实例研究是“直方图中的最大矩形”，这是一个人所共知的无论用什么技术都很不容易处理的问题。我们开发出一个真递归(不是简单尾递归)的解。
　　增加的第二个实例研究是“一个电子邮件系统”，其中相当详尽地阐述了在实现一个系统(而不是一个简单程序)的过程中，在规范、设计、重新规范和重新设计中某些时候可能会出现不可靠的相互作用，数据精化的作用在这里突显出来。
　　致谢
　　对我而言，最大的恩惠来自我的家庭：Sue、Tristan、Elliot和Ethan。
　　许多朋友和同事对第1版的提出了改进建议，我衷心地感谢他们。
　　Carroll Morgan
　　1994复活节

（美）Carroll Morgan：暂无简介

裘宗燕：裘宗燕: 北京大学数学学院信息科学系教授。长期从事计算机软件与理论、程序设计语言和符号计算方面的研究和教学工作。已出版多部著作和译著，包括《程序设计语言基础》（译著，北京大学出版社，1990），《Mathematica数学软件系统的应用与程序设计》（编著，北京大学出版社，1994），《计算概论（上）》（合著，高等教育出版社，1997），《从问题到程序—程序设计与C语言引论》（编著，北京大学出版社，1999）等；自2000年以来，他先后为机械工业出版社华章分社翻译了《程序设计实践》（2000），《C++程序设计语言（特别版）》（2001），《C++语言的设计和演化》（2002），《程序设计语言——概念和结构》（2002），《从规范出发的程序设计》（2003），《计算机程序的构造和解释》（2004）等一系列经典著作，他认真的工作作风、严谨的治学态度，以及所做出的巨大贡献，赢得广大读者的好评。 在北京大学教授的主要课程：计算概论（一年级本科生，主要内容为C语言程序设计），程序设计技术与方法（本科生），程序设计语言原理（研究生），算法和数据结构（本科生），算法设计与分析（本科生和研究生），数理逻辑（本科生）等。 点击进入[URL=http://www.math.pku.edu.cn/teachers/qiuzy/]作者主页[/URL]。

Carroll Morgan的《Programming from Specifications》是一本非常有名的教材，在世界许多重要大学，特别是欧洲各著名大学里广泛使用。本书通常被作为学习过计算机科学的基础知识和基本程序设计之后，第二门程序设计课程的教材。如作者所说，本书已经成功使用了十几年。
　　读者可能感到奇怪：在这个飞速发展的领域里，计算机芯片三大两头翻花样，新语言、新软件层出不穷。难道还有什么书籍能"十年一贯制"?这种书籍的内容是不是早已落伍了?还值得花时间看它吗?与普通的程序设计教材和书籍不同，本书并不想教读者某种新的程序设计语言，或者某个新软件系统的巧妙结构或使用技巧，也不是教某种特定的程序设计方法。这里讨论的是程序和程序设计本身。讨论的是程序的内在规律，程序设计的道理。我们怎么能说一个程序是"正确的"?如何能对自己的程序有这样的信心?应该通过什么样的方式将程序构造出来?这些就是本书的基本论题。
　　这里所倡导的是一种严格的程序开发方法：首先分析问题，用严格方式写出程序的规范，而后通过一系列具有严格理论基础的推导，最终得到可以运行的程序。本书的讨论并不依赖于任何特定的程序设计语言(但基本上是以常规的过程性语言为背景)。书中讨论了与程序设计过程有关的许多基本概念，如规范和程序、精化法则、不变式、数据不变式、不同的抽象层次及其相互连接等等。这些概念在程序中都是极其重要的，某种意义和某种程度上，它们主导着一切程序和程序开发工作，无论你是否意识到这些问题。
　　虽然我们已经有了威力强大的程序设计环境，它们可以帮我们跟踪程序执行中每个二进制位的变化。但是，做程序的还是人。如果我们没有真正掌握程序设计的科学道理，通过玩命干，通过模仿，也可能做出几个小程序。但把这种技术手段和工作方式推广到大型系统则是极其危险的。今天，整个社会的正常运转对各领域中的基础信息系统的依赖性越来越强。由于软件失误而造成的损失也可能越来越重大。因此，明天的专业软件开发需要更多的科学，以便开发出的软件能够植根于更坚实的基础之上。看看今天建筑设计部门或者建筑公司，并不是任何人都能去设计摩天大楼、建设跨江大桥和高速公路。其他成熟的技术领域也一样。未来的软件开发也将需要有分级资格制度，只有达到一定水平，掌握相应的理论基础和实际工具，按照某种必须的工作程序做事情，并有相应质量保证体系的软件公司，才有资格去开发那些关系到人们生产生活的重要问题、关系到生命财产安全、关系到整个社会正常运转的软件和系统。
　　专业软件和程序工作者与业余爱好者之间的差异，最终将表现在他们对本领域的理论基础及其深刻内涵的认识程度上。而在今天，这两类人之间的差异几乎被人们所忽略，似乎任何人在计算机上摸爬滚打一阵，就可以搞软件了。实际上，这也正是目前软件质量低劣，故障颁发的一个原因，是这个领域不成熟的一种表现。任何领域的专业工作者都必须经过一段系统化的专业学习(未必是在学校，同样也可以经过自学)，掌握了本领域中基本的专业基础理论和技术，才能从事该领域的专业性工作。这是已经被当代科学技术的发展所证明的道理，明天的软件工作者也必须是这样。从这个意义上说，本书也可以看作是为培养明天的专业软件工作者的一种探索。
　　要读完这本书，学完(教好)一个基于本书的课程需要付出很大的努力，需要下功夫去思考，努力弄清楚有关的基本思想和技术。不像去读一本有关流行软件或者语言的入门书；而后到计算机上模仿出几个小程序那样轻松。但是，这个努力的回报也将是极其丰厚的。在学完这本书，基本上理解了其中的思想和观点，对于其中的基本概念有了一定认识之后，你会发现自己对程序的认识深入到了另一个层次，对自己的程序更有信心了，在遇到各种情况时也更容易认识到如何找出分析问题的线索。
　　我们当然知道，大部分学软件的人最终是去做某些实践性的工作。但也还是应该认识到学习理论的重要性。理论的最基本作用是帮助我们擦亮眼睛，使人能看得更深，看得更远。理论能成为对实践性工作的指导，为我们提供分析认识问题的线索和解决问题的基础。今天，全社会都已经认识到信息科学与技术的发展对于整个社会发展的作用，国家正在大力推动我国的软件产业和软件教育。我们认为，如果有更多的重要学校能够将类似本书所倡导的软件理论和技术作为专业课程的基本内容和要求，必定能对我国软件事业的明天起到重要的推动作用。
　　致谢
　　感谢Carroll Morgan教授提供了本书的TEX文件，使本书能够基本上保持原貌，也避免了出现大量错误的可能性。感谢何积丰教授有关本书翻译的意见。此外，秦胜潮、隗刚和张欣阅读了本书的原始译本，提出了一些意见，发现了译本和原书的若干错误。细心的读者如果发现书中的错误，请与我联系：qzy@math．pku．edu．cn。
　　本书用LATEX系统排版，并借助了若干自己写出的工具程序。有关的英文原本可以在如下网址找到(感谢Carroll Morgan教授)：
　　http：／／web．comlab．ox．ac．uk／ouc1／publications／books／PfS／
　　裘宗燕，北京大学数学学院信息科学系
　　2002年1月

第1章　程序和精化
1．1　传统观点
1．2　一种新观点
1．3　程序作为契约：精化
1．4　抽象程序
1．5　可执行程序
1．6　混合程序
1．7　不可行程序
1．8　一些常见习惯用法
1．9　几个极端程序
1．10　练习
第2章　谓词演算
2．1　相关性
2．2　项
2．3　简单公式
2．4　命题公式
2．5　量词
2．6　(一般)公式
2．7　运算符的优先级
2．8　谓词演算
2．9　练习
第3章　赋值和顺序复合
3．1　引言
3．2　赋值
3．3　开赋值
3．4　skip命令
3．5　顺序复合
3．6　赋值与复合的结合
3．7　例：交换变量的值
3．8　练习
第4章　选择
4．1　操作性描述
4．2　精化法则
4．3　练习
第5章　迭代
5．1　操作性描述
5．2　精化法则：非形式的
5．3　迭代的终止性：变动量
5．4　迭代的精化法则
5．5　迭代的"核查表"
5．6　练习
第6章　类型和声明
6．1　类型
6．2　声明
6．3　局部块
6．4　类型与不变式的使用
6．5　关于可行性的最后注记
6．6　类型和不变式的检查
6．7　无定义表达式
6．8　练习
第7章　实例研究：平方根
7．1　抽象程序：出发点
7．2　除去"外来"运算符
7．3　寻找不变式
7．4　练习
第8章　初始变量
8．1　简单规范
8．2　初始变量的精确化
8．3　再看顺序复合
8．4　先导赋值
8．5　练习
第9章　构造类型
9．1　幂集
9．2　包
9. 3　序列
9．4　分配运算符
9．5　函数
9．6　关系
9．7　练习
第10章　实例研究：插入排序
10．1　什么叫排序
10．2　类似的前后条件
10．3　减小变动量
10．4　向上或向下迭代
10．5　一个巧妙的不变式
10．6　对序列赋值
10．7　删除局部不变式
10．8　练习
第11章　过程和参数
11．1　无参过程
11．2　用值做替换
11．3　带参数的过程
11．4　对过程调用的精化
11．5　多重替换
11．6　值结果替换
11．7　语法问题
11．8　引用替换
11．9　练习
第12章　实例研究：堆排序
12．1　代码的时间复杂性
12．2　堆
12．3　堆的收缩
12．4　建堆
12．5　过程Sift
12．6　练习
第13章　递归过程
13．1　部分正确性
13．2　递归的变动员
13．3　一个完整例子
13．4　跋：递归块
13．5　练月
第14章　实例研究：灰色编码
14．1　灰色编码
14．2　输入输出
14. 3　孤立的基础情况
14．4　练习
第13章　递归类型
15．1　不相交并
15．2　标志测试
15．3　对选择的模式匹配
15．4　类型声明
15．5　递归类型
15．6　结构序
15．7　迭代中的模式匹配
15．8　例子：树的求和
15．9　练习
第16章　模块和封装
16．1　模块声明
16．2　引出的和局部的过程
16．3　模块的精化
16．4　引入过程和变量
16．5　定义模块与实现模块
16．6　循环引出／引入
16．7　代码中的初始式
16．8　练习
第17章　状态变换和数据精化
17．1　我们还不能证明什么
17．2　状态变换
17．3　强制
17．4　加入变量：扩张
17．5　删除辅助变量：收缩
17．6　数据精化的一个实例
17．7　函数式抽象
17．8　练习
第18章　实例研究：多数表决
18．1　代码精化
18. 2　赢得选举
18．3　直接开发得到平方型代码
18．4　第二个尝试更快速
18．5　代码变换
18．6　简化的代码
18．7　练习
第19章　起源和总结
第20章 实 例研究：分段问题
20．1　均匀分段
20．2　最小损耗
20．3　生成均匀分段
20．4　练习
第21章　实例研究：直方图的最大矩形
21．1　做好基础性工作
21．2　分治法
21．3　强化不变式以恢复可行性
21．4　引入递归
21．5　包装
21．6　练习
第22章　实例研究：一个mail系统
22．1　第一个规范
22．2　标识符的重用
22．3　第二个规范：重用
22．4　第三个规范：延迟
22．5　第一个开发：异步发送
22．6　第二步开发：收条
22．7　最后的开发步骤：打包
22．8　练习
第23章　语义
23．1　引言
23．2　谓词变换器
23．3　语义定义
附录A　谓词演算的一些法则
A．1　一些命题法则
A．2　一些谓词法则
附录B　习题解答
附录C　法则汇编
参考文献
索引