程序邏輯表達

① 什麼是程序邏輯

程序邏輯是描述和論證程序行為的邏輯，又稱霍爾邏輯。程序和邏輯有著本質的聯系。如果把程序看成一個執行過程，程序邏輯的基本方法是先給出建立程序和邏輯間聯系的形式化方法，然後建立程序邏輯系統，並在此系統中研究程序的各種性質。

簡介：
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語句，和指針。

② 結構化程序的三種基本邏輯結構是什麼

1、順序結構：

順序結構表示程序中的各操作是按照它們出現的先後順序執行的。

2、選擇結構：

選擇結構表示程序的處理步驟出現了分支，它需要根據某一特定的條件選擇其中的一個分支執行。選擇結構有單選擇、雙選擇和多選擇三種形式。

3、循環結構：

循環結構表示程序反復執行某個或某些操作，直到某條件為假（或為真）時才可終止循環。在循環結構中最主要的是：什麼情況下執行循環？哪些操作需要循環執行？循環結構的基本形式有兩種：當型循環和直到型循環。

(2)程序邏輯表達擴展閱讀

由於模塊相互獨立，因此在設計其中一個模塊時，不會受到其它模塊的牽連，因而可將原來較為復雜的問題化簡為一系列簡單模塊的設計。模塊的獨立性還為擴充已有的系統、建立新系統帶來了不少的方便，因為可以充分利用現有的模塊作積木式的擴展。

按照結構化程序設計的觀點，任何演算法功能都可以通過由程序模塊組成的三種基本程序結構的組合: 順序結構、選擇結構和循環結構來實現。

結構化程序設計的基本思想是採用"自頂向下，逐步求精"的程序設計方法和"單入口單出口"的控制結構。

自頂向下、逐步求精的程序設計方法從問題本身開始，經過逐步細化，將解決問題的步驟分解為由基本程序結構模塊組成的結構化程序框圖。

"單入口單出口"的思想認為一個復雜的程序，如果它僅是由順序、選擇和循環三種基本程序結構通過組合、嵌套構成，那麼這個新構造的程序一定是一個單入口單出口的程序。據此就很容易編寫出結構良好、易於調試的程序來。