霍爾邏輯

這個想法起源於羅伯特·弗洛伊德於較早的研究，他為流程圖提供了類似的系統。東尼·霍爾於1969年首次發表[，隨後為其他研究者所精製。

Hoare 邏輯(也叫做Floyd–Hoare 邏輯)是英國計算機科學家C. A. R. Hoare開發的形式系統，隨後為 Hoare 和其他研究者所精製。它發表於 Hoare 1969年的論文"計算機程序的公理基礎"中。這個系統的用途是為了使用嚴格的數理邏輯推理計算機程序的正確性提供一組邏輯規則。

Hoare 認可 Robert Floyd的早期貢獻，他為流程圖提供了類似的系統。 ^[1] 

霍爾邏輯的中心特徵是霍爾三元組（Hoare triple）。這種三元組描述一段代碼的執行如何改變計算的狀態。Hoare三元組有如下形式

這裏的P和Q是斷言而C是命令。P叫做前條件而Q叫做後條件。斷言是謂詞邏輯的公式。因此，對Hoare三元組的直觀解讀是：當P在C執行之前成立，那麼Q將在C執行之後成立，或者C不終止。在後一種情況下，不存在程序片段C執行之後的情況，所以Q可以是任何語句。實際上，你可以選擇Q為假來表達C不終止。事實上，這種情形叫做 "部分正確（partial correctness）"。如果C終止並且在終止時Q是真，則表達式被稱作 "全部正確性（total correctness）"。終止必須被單獨證明。

霍爾邏輯為簡單的命令式編程語言的所有構造提供了公理和推理規則。除了給Hoare論文中的簡單語言的規則，其他語言構造的規則也已經被Hoare和很多其他研究者開發完成。包括併發、過程、goto語句，和指針。 ^[2] 

命令式編程（英語：Imperative programming），是一種描述計算機所需作出的行為的編程典範。幾乎所有計算機的硬件工作都是命令式的；幾乎所有計算機的硬件都是設計來運行機器代碼，使用命令式的風格來寫的。較高端的命令式編程語言使用變量和更復雜的語句，但仍依從相同的典範。菜譜和行動清單，雖非計算機程序，但與命令式編程有相似的風格：每步都是指令，有形的世界控制情況。因為命令式編程的基礎觀念，不但概念上比較熟悉，而且較容易具體表現於硬件，所以大部分的編程語言都是命令式的。