托尼·霍尔

托尼·霍尔（Tony Hoare，论文署名 C. A. R. Hoare）早年在牛津学习哲学与古典语言，数学逻辑引发了他对计算的兴趣。1959年，他在莫斯科研究机器翻译时，为提高词典查询效率构思了快速排序。1960年回英国后，他在 Elliott Brothers 从事编译器开发，领导的团队中也包括后来成为其妻子的 Jill。

随后一项操作系统工程遭遇失败，使他更加关注复杂软件为何难以可靠建造。1968年他到贝尔法斯特女王大学任教，1977年转至牛津，发展原由克里斯托弗·斯特雷奇建立的程序研究组。工程问题没有被理论取代，而成为其研究程序语言与并发的背景。

参考：[1]

霍尔于1961年发表快速排序，1962年的长篇论文进一步解释方法及实现细节。基本思想是选择一个分界值，交换位置不合适的元素，把待排序区间分成两部分，再分别处理，直到子问题足够小。分割后并非所有元素已经处于最终位置，但两侧的大小关系使问题可以继续分解。

论文在分界元素具有相应随机性假设时分析平均代价，得到与元素数乘其对数同阶的比较次数。这个结论不是对每一次运行的固定耗时承诺。分割方式、重复元素处理、小区间策略与存储安排都影响实现；把今天某个库的具体变体全部归给霍尔，也会抹去后续改进。

参考：[3] [2]

1969年的论文将前置条件、程序与后置条件联系起来。用今天常见的三元组写法，可把它理解为：满足前置条件时执行程序，如果正常结束，结果应满足后置条件。赋值规则、顺序组合规则与循环不变式，使较大程序的性质能够由较小步骤推导，而不必只靠列举输入试运行。

这里的“如果结束”至关重要。原文明确指出，这组规则本身不证明程序一定终止；无限循环、数值范围或存储限制都须另行考虑。算术模型与实际机器是否一致也会影响结论。因而部分正确性证明、终止性证明和实现符合性是不同问题，不能把一个逻辑推导说成对现实系统所有故障的保险。

参考：[4]

霍尔后来发展通信顺序进程模型 CSP，用数学方式描述并发系统的交互并研究其性质。它影响了 occam 等语言及工业验证工具。他与何积丰合作开展的程序设计统一理论，则试图在共同基础上联系不同编程范式。牛津研究群体还推进了 Z 等形式方法，这些成果有各自的合作历史，并非都由他一人独创。

1980年，霍尔因程序语言定义与设计方面的贡献获得图灵奖；1999年从牛津退休后进入微软研究院。牛津于2026年3月发布悼文。他留下的研究路线不是一句简单的“证明胜过测试”，而是把规范、设计和可检验的推理联系起来，并持续寻找理论进入工程实践的办法。

参考：[1] [2]