動的論理
dynamic logic
action$ aの後必然的に$ Pが成り立つ$ \lbrack a\rbrack P
action$ aの後$ Pが成り立つ事が可能である$ \lang a\rang P
$ \lbrack a\rbrack P\iff\neg\lang a\rang\neg P.
$ \lang a\rang P\iff\neg\lbrack a\rbrack\neg P.
action 閒の演算
特殊な action
$ 0。何もせず、終はらない。BLOCK とも呼ぶ
$ 1:=0^*。SKIP や NOP とも呼ぶ
演算子
選擇$ a\cup b。action$ aか$ bのどちらかを實行する
順次$ a;b。action$ aを實行し、次に action$ bを實行する
公理
$ \lbrack 0\rbrack p.
$ \lbrack 1\rbrack p\iff p.
$ \lbrack a\cup b\rbrack\iff\lbrack a\rbrack p\land\lbrack b\rbrack p.
$ \lbrack a;b\rbrack\iff\lbrack a\rbrack\lbrack b\rbrack p.
$ \lbrack a^*\rbrack p\iff p\land\lbrack a\rbrack\lbrack a^*\rbrack p。$ a^*=1\cup a;a^*として Kleene 代數になる $ p\land\lbrack a^*\rbrack(p\to\lbrack a\rbrack p)\to\lbrack a^*\rbrack p。數學的歸納法の公理 Hoare 論理での$ \lbrace P\rbrace a\lbrace Q\rbraceは動的論理で$ P\to\lbrack a\rbrack Qと書く