Hoare 論理
Hoare logic
program$ Cが事前條件 (precondition)$ Pの下で實行され終了した時に事後條件 (postcondition)$ Qを滿たすなら$ \{P\}C\{Q\}と書く。これを Hoare triple と呼ぶ
公理
空文の公理$ \frac{}{\{P\}{\rm skip}\{P\}}
代入の公理$ \frac{}{\{P\lbrack E/x\rbrack\}x:=E\{P\}}
複合文の公理$ \frac{\{P\}S\{Q\}\quad\{Q\}T\{R\}}{\{P\}S;T\{R\}}
if の公理$ \frac{\{B\land P\}S\{Q\}\quad\{\neg B\land P\}T\{Q\}}{\{P\}{\rm if}B{\rm then}S{\rm else}T{\rm endif}\{Q\}}
歸結の公理$ \frac{P_1\to P_2\quad\{P_2\}S\{Q_2\}\quad Q_2\to Q_1}{\{P_1\}S\{Q_1\}}
while の公理$ \frac{\{P\land B\}S\{P\}}{\{P\}{\rm while}B{\rm do}S{\rm done}\{\neg B\land P\}}
完全正當性の爲の while の公理。$ <_Dを集合$ D上の整礎關係とし、$ \frac{\{P\land B\land t=_D z\}S\{P\land t<_D z\}}{\{P\}{\rm while}B{\rm do}S{\rm done}\{\neg B\land P\}}
demand-side
事前條件を滿たす義務
事後條件が滿たされる權利
supply-side
事前條件が滿たされる權利 (validation)
事後條件を滿たす義務 (sanitize)
述語變換意味論 (predicate transformer semantics)
擴張
動的論理 (dynamic logic)$ P\to\lbrack C\rbrack Q