Hoare Logic

逐次なプログラムの検証です。割と簡単で、

　　{Pre} Command {Post}

という感じで、Command を実行すると、Pre condition が Post condtion になるっていうだけですね。

Loop の時には、

　　{Invariant} Loop {Invariant}

で入り口と出口が等しければ大丈夫。まぁ、Invariant 見つけるのめんどくさいとかいう話はあるけど、

　　ちゃんと動いているなら、なんかあるだろ

という感じらしいです。

Agda で書いた人も多いらしく、いろいろ見つかるらしいんですが、いかんせん Hoare Logic が古色蒼然なので、

　　プログラムの記述法が古くさい、いわゆる While Program

まぁ、While Program でなんでも書けるんだけどさ。

でも、本で読んだり、頭で理解したりしていることと、

　　実際に証明を書き下す

ことには結構ギャップがある。やっぱり、やってみないとね。

Axiom : Cond -> PrimComm -> Cond -> Set
Axiom pre comm post = ∀ (env : Env) → (pre env) ⇒ ( post (comm env)) ≡ true

こんな感じらしいです。これの鎖みたいなのをプログラムに対して書いて、で、この値の式をせこせこ証明していくわけね。

なんか細かい自然数論の証明がたくさん出てくるけど、そこくらい自動的にやってくれないかな...

http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/ryokka/HoareLogic/file/tip/whileTestPrim.agda