算法分析引论：第2版

2010年图灵奖获得者、当时的微软剑桥研究院首席研究员托尼霍尔爵士（TonyHoare）在与中国科学院相关研究人员座谈时曾提到：“在我看来，语言设计的目标应该是确保它能够使我们以简便的方法来写出那些正确的程序……评测一种语言，应当根据它最后写出来的程序的正确性来进行评估，这才是评测一个语言质量的科学准则。”霍尔爵士的主要贡献在于对程序正确性证明方面的研究。