资源描述：
《引言(Introduction)》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。
1、第零章序言(Preface)0.0引言(Introduction)程序设计理论有什么用?谁需要它呢?没有任何理论，成千上万的程序员还是每天都在编程,那么又何必费心去学一门理论呢？该问题的答案其实和任何其他理论一样。譬如,为什么人人都要学习运动学理论?你可以在不懂理论的情况下行动自如,也可以在不懂理论的情况下投球。但我们仍然认为在中学讲授运动学理论是相当重要的。对这个的问题的回答之一是,通过提供演算的方法，数学理论达到了一个高得多的精确程度。没有关于运动学的理论,我们根本不可能发射火箭到木星。甚至
2、投球手们也发现理论专家可以帮助他们改进投球技术。同样,没有理论的帮助,许多一般的程序设计也可以完成,但对更复杂的程序设计,没有好的理论就难以正确无误的完成。软件产业有数不清的因程序错误造成的惨痛教训无一不证明了这点。况且,即使是通常的编程也会因适当运用理论而得到改进。而回答之二是,理论可以提高理解能力。当我们学会了运动学的理论时,我们对运动的控制和预见能力从艺术走向了科学。同样,当我们学会以理解数学定理的方式来理解程序时,程序设计也从艺术走向了科学。有了科学的观点,我们就改变了对世界的看法。更少
3、地依赖灵感或运气，更明白什么是可能的,什么是不可能的。对任何人而言，这都是通过宝贵的教育才能达到的。专业工程学在社会上维持很高的声誉,就是因为它坚持这样一点:要成为一名专业工程师,一个人必须懂得和应用相关的理论。一个土木工程师必须懂得和运用几何和材料力学,一个电气工程师必须懂得和运用电磁理论,软件工程师要想名副其实,也必须懂得和运用程序设计理论。本书的主题有时称为“程序设计方法学”,有时又称为“程序设计科学”,“程序设计逻辑”,“程序设计理论”,“程序开发形式化方法”,或“程序证明”,它涉及程序
4、设计中经得起数学证明的那些方面。一个好的理论能帮助我们书写精确的规范,并设计出其执行可被证明满足规范的程序。我们将考虑计算的状态、计算的时间、计算的空间以及计算的交互。但有一些软件设计和制作的重要方面本书没有论及,例如人员管理,用户界面,文档化和测试等。第一个有用的程序设计理论通常称为“Hoare逻辑”,仍可能是最广为人知的。在Hoare逻辑中,一条规范是一对谓词：前置条件和后置条件(这两个术语及其后提及的所有术语都将在以后的相应章节中给出定义)。另一个紧密相关的理论使用了Dijkstra的最弱
5、前置谓词转换器,它将程序和后置条件通过转换得到前置条件，它后来发展成了Back的精化演算。Jones的维也纳开发方法已被某些产业采用并获益,其中,一条规范是一对谓词(正如Hoare逻辑),但其中第二个谓词是一个关系。另外，还有一些专门用于实时程序设计、概率程序设计、交互式程序设计的理论。本书中的理论比上面提到的都要简单。在该理论中,一条规范就是一个布尔表达式,精化就是通常的蕴含式。该理论也比上述理论更为通用,同时适用于终止和非终止计算,顺序和并行计算,以及独立和交互式计算。我们可以同时有只对其初
6、值和终值感兴趣的变量、对0其值始终感兴趣的变量、只知道其可能值的变量和用于计算时间和空间的变量。它们都适合于同一理论中，其基础在于将规范表示成布尔表达式，而布尔表达式的变量可以是任何感兴趣的变量。有一种通过穷举测试所有输入来证明程序的方法，称为模型检测（modelchecking）。它优于本书中理论的一点在于可以完全自动化。通过明智的布尔表达式的表示（见练习6），60模型检测当前声称可以处理约10个状态。这比宇宙中所估计的原子个数还多！这个数字60200令人印象深刻，可是后来我们意识到10约为2
7、，这意味这我们所谈论的是200位二进制数，也就是6个32位二进制数变量的状态空间。对任何一个超过六个变量的程序进行模型检测就需要抽象，每个抽象要求证明其保持所感兴趣的性质。这些抽象和证明不是自动的。为了保证实用，模型检测必须与其他的证明方法相结合，例如本书中的方法。本书还要一直强调的一点是，程序开发的每一步都是伴随证明的，而不是在开发以后进行证明。---------------------------------------------------------------------------
8、------------------------------------------------引言结束0.1当前版本(CurrentEdition)在本书的当前版本中，我们增加了空间约束和概率程序设计的新的资料，归纳了for循环规则，简化了对并发的处理，且对并行进程之间的合作提供了选择：通信（如第一版），和交互变量。本书加强了解释和说明，并增加了更多整理过的例子。在增加的同时，也有删减。为了保证本书的精练，任何在课程中将略过的资料被删除了。本书只有147页，后面的只是练习和参考材料。授课教师可
