前後斷言方法
pre-and post-assertion method
該證明方法源於R.Floycl，他在1967年提出在 流程圖的聯線上加上斷言使得程式到達該處時斷言 為真。後經C.A.R.HOare發展成型，成為程式設計 邏輯的主要部分。 前後斷言的主要形式有兩種: (l)Q{引R刻畫語句S的部分正確性。意 指:若前提條件Q滿足，且S執行終止，則S終止 時結果斷言R成立。 (2){Q}S{R}刻畫語句S的完全正確性。意 指:若前提條件Q滿足，則S執行終止，且S終止 時結果斷言R成立。 將Q{S}R或{Q}S{R}的整體作為一個謂詞 公式，若該公式永真，則S相對於前提條件Q和結 果斷言R分別是部分正確或完全正確的。為證明 複合語句Q{51;52}R的部分正確性，可在S，;52 之間插入斷言Q‘使得Q{S;}Q‘和Q‘{52}R都永 真。也可以插人多個斷言Ql，QZ，Q3等，使它們之 間是蘊涵關係，用以反映證明思路。對其它語句構 造可採用類似的方法。對於循環語句，除給出前後 斷言外，還須在循環中加入循環不變式，要求每次循 環到達該處時不變式都成立。用前後斷言可表示 語句的公理語義。利用這些語義規則可幫助我們 在程式正確性證明過程中確定該擂人何種斷言， 以達到引導證明的目的(參見最弱前里條件方法)。 前後斷言方法，特別是結合最弱前置條件方法現 已廣泛用於規約語言及其支撐系統，如VDM，Lareh 等。
