程式邏輯是描述和論證程式行為的邏輯，又稱霍爾邏輯。程式和邏輯有著本質的聯絡。如果把程式看成一個執行過程，程式邏輯的基本方法是先給出建立程式和邏輯間聯絡的形式化方法，然後建立程式邏輯系統，並在此係統中研究程式的各種性質。簡介：　　Hoare 邏輯(也叫做Floyd–Hoare 邏輯)是英國計算機科學家C. A. R. Hoare開發的形式系統，隨後為 Hoare 和其他研究者所精製。它發表於 Hoare 1969年的論文"計算機程式的公理基礎"中。這個系統的用途是為了使用嚴格的數理邏輯推理計算機程式的正確性提供一組邏輯規則。　　Hoare 認可 Robert Floyd的早期貢獻，他為流程圖提供了類似的系統。　　Hoare 邏輯的中心特徵是Hoare 三元組。這種三元組描述一段程式碼的執行如何改變計算的狀態。Hoare 三元組有如下形式　　{P}C{Q}這裡的 P 和 Q 是斷言而 C 是命令。P 叫做前條件而 Q 叫做後條件。斷言是謂詞邏輯的公式。這個三元組在直覺上讀做: 只要 P 在 C 執行前的狀態下成立，則在執行之後 Q 也成立。注意如果 C 不終止，也就沒有"之後"了，所以 Q 在根本上可以是任何語句。實際上，你可以選擇 Q 為假來表達 C 不終止。　　這叫做"部分正確"的。如果 C 終止並且在終止時 Q 是真，則表示式就是"全部正確"的。終止必須被單獨證明。　　Hoare 邏輯為簡單的指令式程式設計語言的所有構造提供了公理和推理規則。除了給 Hoare 論文中的簡單語言的規則，其他語言構造的規則也已經被 Hoare 和很多其他研究者開發出來了。包括併發、過程、goto語句，和指標。