计算机程序设计的公理基础

1969 · C. A. R. Hoare

Hoare 以公理和推理规则为核心，提出一种证明程序部分正确性的框架，并据此讨论程序证明、语言定义、文档和可移植性。