我好像已經把你搞糊涂了…… 我們先來科普一下 Hoare Logic。
Hoare Logic（https://en.wikipedia.org/wiki/Hoare_logic） 是一種形式驗證的方法，用于驗證程序的正確性。它的做法是，先給代碼標注一些“前條件”和“后條件”（pre-condition 和 post-condition），然后就可以進行邏輯推理，驗證代碼的某些基本屬性，比如轉賬之后余額是正確的。
舉一個很簡單的 Hoare Logic 例子：
{x=0} x:=x+1 {x>0}
它的意思是，如果開頭 x 等于 0，那么 x:=x+1 執行之后，x 應該大于 0。這里的前條件（pre-condition）是 x=0，后條件（post-condition）是 x > 0。如果 x 開頭是零，執行 x:=x+1 之后，x 就會大于 0，所以這句代碼就驗證通過了。
Hoare Logic 的系統把所有這些前后條件和代碼串接起來，經過邏輯推導驗證，就可以作出這樣的保證：在前條件滿足的情況下，執行代碼之后，后條件一定是成立的。如果所有這些條件都滿足，系統就認為這是“正確的程序”。注意這里的所謂“正確”，完全是由人來決定的，系統并不知道“正確”是什么意思。
Hoare Logic 對于程序的安全性，確實可以起到一定的效果，它已經被應用到了一些實際的項目。比如微軟 Windows 的驅動程序代碼里面，有一種“安全標注語言”，叫做 SAL，其實就是 Hoare Logic 的一個實現。然而前條件和后條件是什么，你必須自己給代碼加上標注，否則系統就不能工作。
比如上面的例子，系統如何知道我想要“x>0”這個性質呢？只有我自己把它寫出來。所以要使用 Hoare Logic，必須在代碼上標注很多的 pre-condtion 和 post-condition。這些條件要如何寫，必須要深入理解程序語言和形式邏輯的原理。這個工作需要經過嚴格訓練的專家來完成，而且需要很多的時間。
版權申明：本內容來自于互聯網，屬第三方匯集推薦平臺。本文的版權歸原作者所有，文章言論不代表鏈門戶的觀點，鏈門戶不承擔任何法律責任。如有侵權請聯系QQ：3341927519進行反饋。
