作者在这一章叙述了编写正确程序的基本方法，在这个过程中介绍了断言、不变式等重要概念，主要介绍了人工程序验证这种检验程序正确性的方法。

　　用到的例子是二分搜索，作者在第一小节便强调，二分搜索从论文的发表到第一个没有错误的程序出现，历经了16年的时间，以此来强调编写正确程序的重要性和本章的必要性。

<li><strong>原理总结</strong></li>

　　断言。     输入、程序变量和输出之间的关系勾勒出了程序的“状态”，断言使得程序员可以准确阐述这些关系。
　　
　　顺序控制结构。     可以通过在语句之间添加断言并分别分析程序执行的每一步来理解这样的结构。
　　
　　选择控制结构。     我们通过分别分析 每一个分支说明了该结构的正确性。一定会选择某个分支的事实允许我们使用断言来证明。
　　
　　迭代控制结构。     要证明循环的正确性就必须为其确立3个性质：初始化、保持、终止。我们首先讨论由初始化确立的循环不变式，然后证明每次迭代都保持该不变式为真。第三步是证明无论循环在何时终止执行，所得的结果都是正确的。综合这些步骤可知：只要循环能停止运行，那么其结果就是正确的。因此我们还必须用其他方法证明循环一定能终止。
　　
　　函数。     要验证一个函数，首先需要使用两个断言（assertion）来陈述其目的。前置条件（precondition）是在调用该函数之前就应该成立的状态，后置条件（postcondition）的正确性由函数在终止执行时保证。这些条件与其说是事实陈述不如说是一个契约：如果在前置条件满足的情况下调用函数，那么函数的执行将确立后置条件。一旦证明函数体具有该性质，在以后的应用中就可以直接使用前置条件和后置条件之间的关系而不再需要考虑其实现。该方法在软件开发中通常称为“契约编程”。