- 815 名前：デフォルトの名無しさん mailto:sage [2009/07/13(月) 22:25:27 ]
- >>805
Hoare Logicだな
実行文の前でのxの値をX,実行文の後ではYとすると
このプログラムが正常に動作すると仮定すれば
{x=X} x:=x+1 {x=Y}というHoare Tripleが構成できて、代入の規則から
x=X ≡ (x+1=Y) <=> x=X ≡ (x=Y-1) ← X = Y - 1 ≡ Y = X + 1
ってな具合にxに1を加えるっていう動作をする事が証明できたりする
代入を感覚で理解できなくて、
a=10,b=20; a=b; a=?,b=?;っていう問題を解けない人でも、この技法を使えば
計算で解くことができる、素晴しい！！
勿論、こういう単純な例だけでなく分岐やループも扱えるんだけど
「ループで配列内要素の総和を求める」っていうような問題でも
A4レポート用紙2枚に収まるか怪しいような長い証明を
書く羽目になるから、そうバシバシ使っていけるものでもないな
これと比べるとdependently typeとcurry-howard対応の何と実用的なことか…
|
 |
