霍尔逻辑

（计算机程序）

霍尔逻辑（英语：Hoare Logic），又称弗洛伊德-霍尔逻辑（Floyd–Hoare logic），是英国计算机科学家东尼·霍尔开发的形式系统，这个系统的用途是为了使用严格的数理逻辑推理来替计算机程序的正确性提供一组逻辑规则。这个想法起源于罗伯特·弗洛伊德于较早的研究，他为流程图提供了类似的系统。东尼·霍尔于1969年首次发表[，随后为其他研究者所精制。