序

摘要

本书的意图是阐明和举例说明计算机程序正确性证明的一些基本技术。近几年来,致力于这一课题的研究已取得了巨大的成果。这些研究的大部分都是针对着证明的形式化和最终的机械化。但是,我们强调的却是这种典型的相当非形式的正确性证明(程序员可用它来设法系统地确定其本身的程序正确性)。当然,我们将会发觉非形式的正确性证明可能容易出错。因而,它并不是予防或者发现一切程序设计错误的灵丹妙药。但是,我们深信这种非形式的正确性证明将为