[科普中国]-霍尔逻辑

霍尔逻辑（英语：Hoare Logic），又称弗洛伊德-霍尔逻辑（Floyd–Hoare logic），是英国计算机科学家东尼·霍尔开发的形式系统，这个系统的用途是为了使用严格的数理逻辑推理来替计算机程序的正确性提供一组逻辑规则。

起源这个想法起源于罗伯特·弗洛伊德于较早的研究，他为流程图提供了类似的系统。东尼·霍尔于1969年首次发表[，随后为其他研究者所精制。

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

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

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

这里的P和Q是断言而C是命令。P叫做前条件而Q叫做后条件。断言是谓词逻辑的公式。这个三元组在直觉上读做:只要P在C执行前的状态下成立，则在执行之后Q也成立。注意如果C不终止，也就没有"之后"了，所以Q在根本上可以是任何语句。实际上，你可以选择Q为假来表达C不终止。事实上，这种情形叫做 "部分正确（partial correctness）"。如果C终止并且在终止时Q是真，则表达式被称作 "全部正确性（total correctness）"。终止必须被单独证明。

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

命令式编程命令式编程（英语：Imperative programming），是一种描述计算机所需作出的行为的编程典范。几乎所有计算机的硬件工作都是命令式的；几乎所有计算机的硬件都是设计来运行机器代码，使用命令式的风格来写的。较高端的命令式编程语言使用变量和更复杂的语句，但仍依从相同的典范。菜谱和行动清单，虽非计算机程序，但与命令式编程有相似的风格：每步都是指令，有形的世界控制情况。因为命令式编程的基础观念，不但概念上比较熟悉，而且较容易具体表现于硬件，所以大部分的编程语言都是命令式的。

本词条内容贡献者为:

杨晓红 - 副教授 - 西南大学