霍爾邏輯

霍爾邏輯（英語：Hoare Logic），又稱弗洛伊德-霍爾邏輯（Floyd–Hoare logic），是英國計算機科學家東尼·霍爾開發的形式系統，這個系統的用途是為了使用嚴格的數理邏輯推理來替電腦程式的正確性提供一組邏輯規則。

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

霍爾三元組

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

$\{P\}\;C\;\{Q\}$

這裏的 P 和 Q 是 斷言 而 C 是命令 。P 叫做 前條件 而 Q 叫做 後條件 。斷言是謂詞邏輯的公式。這個三元組在直覺上讀做：只要 P 在 C 執行前的狀態下成立，則在執行之後 Q 也成立。注意如果 C 不終止，也就沒有"之後"了，所以 Q 在根本上可以是任何語句。實際上，你可以選擇 Q 為假來表達 C 不終止。事實上，這種情形叫做 "部分正確（partial correctness）"。如果 C 終止並且在終止時 Q 是真，則表達式被稱作 "全部正確性（total correctness）"。終止必須被單獨證明。

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

部分正確性

空語句公理

${\frac {}{\{P\}\ {\textbf {skip}}\ \{P\}}}\!$

如果P在一個空語句之前成立，那麼在執行這個空語句之後也是成立的。 "skip"在這裏表示空語句（Empty statement）。

賦值公理模式

賦值公理聲稱，關於對賦值右手端的變量的以前為真的任何命題在賦值之後仍然成立:

${\frac {}{\{P[E/x]\}\ x:=E\ \{P\}}}\!$

這裏的$P[E/x]$指示表達式P中所有的自由變量x都被替代為表達式E。

有效的三元組的兩個例子:

$\{x+1=43\land x=42\}\ y:=x+1\ \{y=43\land x=42\}\!$

$\{x+1=N\}\ x:=x+1\ \{x=N\}$

順序規則

${\frac {\{P\}\ S\ \{Q\}\ ,\ \{Q\}\ T\ \{R\}}{\{P\}\ S;T\ \{R\}}}\!$

例如，考慮賦值公理的下列兩個實例:

$\{x+1=43\}\ y:=x+1\ \{y=43\}$

和

$\{y=43\}\ z:=y\ \{z=43\}$

通過順序規則，將得到:

$\{x+1=43\}\ y:=x+1;z:=y\ \{z=43\}$

條件規則

${\frac {\{B\wedge P\}\ S\ \{Q\}\ ,\ \{\neg B\wedge P\}\ T\ \{Q\}}{\{P\}\ {\textbf {if}}\ B\ {\textbf {then}}\ S\ {\textbf {else}}\ T\ {\textbf {endif}}\ \{Q\}}}\!$

While規則

${\frac {\{P\wedge B\}\ S\ \{P\}}{\{P\}\ {\textbf {while}}\ B\ {\textbf {do}}\ S\ {\textbf {done}}\ \{\neg B\wedge P\}}}\!$

這裏的P是循環不變條件。

推論規則

${\frac {P^{\prime }\rightarrow \ P\ ,\ \lbrace P\rbrace \ S\ \lbrace Q\rbrace \ ,\ Q\rightarrow \ Q^{\prime }}{\lbrace P^{\prime }\ \rbrace \ S\ \lbrace Q^{\prime }\rbrace }}\!$

全部正確性

上述規則只證明部分正確性。可以通過擴展版本的While規則證明全部正確性。

• 全部正確性的While規則:

${\frac {\{P\wedge B\wedge t=z\}\ S\ \{P\wedge t<z\}\ ,\ P\rightarrow t\geq 0}{\{P\}\ {\textbf {while}}\ B\ {\textbf {do}}\ S\ {\textbf {done}}\ \{\neg B\wedge P\}}}\!$

在本文中，除了維持循環不變條件，還能通過其值在每次重複期間遞減的項就是這裏的t的方式來證明終止。注意t必須從良定集合中取值，所以循環的每一步都通過遞減有限鏈的成員來計數。

參見

• 契約式設計
• 動態邏輯
• 艾茲赫爾·戴克斯特拉
• 謂詞變換者語義
• 程序驗證

參考文獻

來源

刊物文章

• C. A. R. Hoare. "An axiomatic basis for computer programming". Communications of the ACM, 12(10):576–585, October 1969. doi:10.1145/363235.363259

書籍

• Robert D. Tennent: "Specifying Software" (a recent textbook that includes an introduction to Hoare logic) ISBN 0-521-00401-2 [1] （頁面存檔備份，存於互聯網檔案館）