《从规范出发的程序设计》译者序

Carroll Morgan 的《Programming from Specifications》是一本非常有名的教材, 在世界许多重要大学,特别是欧洲各著名大学里广泛使用。 本书通常被作为学习过计算机科学的基础知识和基本程序设计之后, 第二门程序设计课程的教材。如作者所说,本书已经成功使用了十几年。

读者可能感到奇怪:在这个飞速发展的领域里, 计算机芯片三天两头翻花样,新语言、新软件层出不穷。难道还有什么书籍能 “十年一贯制”?这种书籍的内容是不是早已落伍了?还值得花时间看它吗? 与普通的程序设计教材和书籍不同,本书并不想教读者某种新的程序设计语言, 或者某个新软件系统的巧妙结构或使用技巧,也不是教某种特定的程序设计方法。 这里讨论的是程序和程序设计本身。讨论的是程序的内在规律,程序设计的道理。 我们怎么能说一个程序是“正确的”?如何能对自己的程序有这样的信心? 应该通过什么样的方式将程序构造出来?这些就是本书的基本论题。

这里所倡导的是一种严格的程序开发方法:首先分析问题,用严格方式写出程序的规范, 而后通过一系列具有严格理论基础的推导,最终得到可以运行的程序。 本书的讨论并不依赖于任何特定的程序设计语言(但基本上是以常规的过程性语言为背景)。 书中讨论了与程序设计过程有关的许多基本概念,如规范和程序、精化法则、不变式、 数据不变式、不同的抽象层次及其相互连接等等。这些概念在程序中都是极其重要的, 某种意义和某种程度上,它们主导着一切程序和程序开发工作,无论你是否意识到这些问题。

虽然我们已经有了威力强大的程序设计环境,它们可以帮我们跟踪程序执行中每个二进制位的变化。 但是,做程序的还是人。如果我们没有真正掌握程序设计的科学道理,通过玩命干,通过模仿, 也可能做出几个小程序。但把这种技术手段和工作方式推广到大型系统则是极其危险的。今天, 整个社会的正常运转对各领域中的基础信息系统的依赖性越来越强。 由于软件失误而造成的损失也可能越来越重大。因此,明天的专业软件开发需要更多的科学, 以使开发出的软件能够植根于更坚实的基础之上。看看今天建筑设计部门或者建筑公司, 并不是任何人都能去设计摩天大楼、建设跨江大桥和高速公路。其他成熟的技术领域也一样。 未来的软件开发也将需要有分级资格制度,只有达到一定水平,掌握相应的理论基础和实际工具, 按照某种必须的工作程序做事情,并有相应质量保证体系的软件公司, 才有资格去开发那些关系到人们生产生活的重要问题、关系到生命财产安全、 关系到整个社会正常运转的软件和系统。

专业软件和程序工作者与业余爱好者之间的差异, 最终将表现在他们对本领域的理论基础及其深刻内涵的认识程度上。而在今天, 这两类人之间的差异几乎被人们所忽略,似乎任何人在计算机上摸爬滚打一阵,就可以搞软件了。 实际上,这也正是目前软件质量低劣,故障频发的一个原因,是这个领域不成熟的一种表现。 任何领域的专业工作者都必须经过一段系统化的专业学习(未必是在学校,同样也可以经过自学), 掌握了本领域中基本的专业基础理论和技术,才能从事该领域的专业性工作。 这是已经被当代科学技术的发展所证明的道理,明天的软件工作者也必须是这样。 从这个意义上说,本书也可以看作是为培养明天的专业软件工作者的一种探索。

要读完这本书,学完(教好)一个基于本书的课程需要付出很大的努力,需要下功夫去思考, 努力弄清楚有关的基本思想和技术。不像去读一本有关流行软件或者语言的入门书, 而后到计算机上模仿出几个小程序那样轻松。但是,这个努力的回报也将是极其丰厚的。 在学完这本书,基本上理解了其中的思想和观点,对于其中的基本概念有了一定认识之后, 你会发现自己对程序的认识深入到了另一个层次,对自己的程序更有信心了, 在遇到各种情况时也更容易认识到如何找出分析问题的线索。

我们当然知道,大部分学软件的人最终是去做某些实践性的工作。 但也还是应该认识到学习理论的重要性。理论的最基本作用是帮助我们擦亮眼睛, 使人能看得更深,看得更远。理论能成为对实践性工作的指导, 为我们提供分析认识问题的线索和解决问题的基础。 今天,全社会都已经认识到信息科学与技术的发展对于整个社会发展的作用, 国家正在大力推动我国的软件产业和软件教育。我们认为, 如果有更多的重要学校能够将类似本书所倡导的软件理论和技术作为专业课程的基本内容和要求, 必定能对我国软件事业的明天起到重要的推动作用。

致谢

感谢 Carroll Morgan 教授提供了本书的 TeX 文件,使本书能够基本上保持原貌, 也避免了出现大量错误的可能性。感谢何积丰教授有关本书翻译的意见。 此外,秦胜潮、隗刚和张欣阅读了本书的原始译本,提出了一些意见, 发现了译本和原书的若干错误。细心的读者如果发现书中的错误,请与我联系: qzy@math.pku.edu.cn。

本书用 LaTeX 系统排版,并借助了若干自己写出的工具程序。 有关的英文原本可以在如下网址找到(感谢 Carroll Morgan 教授):
http://web.comlab.ox.ac.uk/oucl/publications/books/PfS/

裘宗燕,北京大学数学学院信息科学系
2002年1月