更新时间：2022-08-26 10:55
霍尔逻辑（英语：Hoare Logic），又称弗洛伊德-霍尔逻辑（Floyd–Hoare logic），是英国计算机科学家东尼·霍尔开发的形式系统，这个系统的用途是为了使用严格的数理逻辑推理来替计算机程序的正确性提供一组逻辑规则。
这个想法起源于罗伯特·弗洛伊德于较早的研究，他为流程图提供了类似的系统。东尼·霍尔于1969年首次发表[，随后为其他研究者所精制。
Hoare 逻辑(也叫做Floyd–Hoare 逻辑
Hoare 认可 Robert Floyd的早期贡献，他为流程图提供了类似的系统。
霍尔逻辑的中心特征是霍尔三元组（Hoare triple）。这种三元组描述一段代码的执行如何改变计算的状态。Hoare三元组有如下形式
这里的P和Q是断言而C是命令。P叫做前条件而Q叫做后条件。断言是谓词逻辑的公式。因此，对Hoare三元组的直观解读是：当P在C执行之前成立，那么Q将在C执行之后成立，或者C不终止。在后一种情况下，不存在程序片段C执行之后的情况，所以Q可以是任何语句。实际上，你可以选择Q为假来表达CC终止并且在终止时Q
霍尔逻辑为简单的命令式编程语言的所有构造提供了公理和推理规则。除了给Hoare论文中的简单语言的规则，其他语言构造的规则也已经被Hoare和很多其他研究者开发完成。包括并发、过程、goto语句，和指针。
命令式编程（英语：Imperative programming），是一种描述计算机所需作出的行为的编程典范。几乎所有计算机的硬件工作都是命令式的；几乎所有计算机的硬件都是设计来运行机器代码，使用命令式的风格来写的。较高端的命令式编程语言使用变量和更复杂的语句，但仍依从相同的典范。菜谱和行动清单，虽非计算机程序，但与命令式编程有相似的风格：每步都是指令，有形的世界控制情况。因为命令式编程的基础观念，不但概念上比较熟悉，而且较容易具体表现于硬件，所以大部分的编程语言都是命令式的。