Hoare 逻辑(也叫做Floyd–Hoare 逻辑)是英国计算机科学家C. A. R. Hoare开发的形式系统，随后为 Hoare 和其他研究者所精制。它发表于 Hoare 1969年的论文"计算机程序的公理基础"中。这个系统的用途是为了使用严格的数理逻辑推理计算机程序的正确性提供一组逻辑规则。

Hoare 认可 Robert Floyd的早期贡献，他为流程图提供了类似的系统。

Hoare 逻辑的中心特征是Hoare 三元组。这种三元组描述一段代码的执行如何改变计算的状态。Hoare 三元组有如下形式

{P}C{Q}这里的 P 和 Q 是断言而 C 是命令。P 叫做前条件而 Q 叫做后条件。断言是谓词逻辑的公式。这个三元组在直觉上读做: 只要 P 在 C 执行前的状态下成立，则在执行之后 Q 也成立。注意如果 C 不终止，也就没有"之后"了，所以 Q 在根本上可以是任何语句。实际上，你可以选择 Q 为假来表达 C 不终止。

这叫做"部分正确"的。如果 C 终止并且在终止时 Q 是真，则表达式就是"全部正确"的。终止必须被单独证明。

Hoare 逻辑为简单的命令式编程语言的所有构造提供了公理和推理规则。除了给 Hoare 论文中的简单语言的规则，其他语言构造的规则也已经被 Hoare 和很多其他研究者开发出来了。包括并发、过程、goto语句，和指针。