-
- いいね！0
Ikegami Daisuke
@ikegami__
プログラムの性質の証明といっても、Algebra of Programming (R. Bird & O-D. Moor 1996) の範疇をでるようなものもあるのだろうか、separation logic とか使えばいろいろできるのかな
2011-02-28 15:52:50
Ikegami Daisuke
@ikegami__
Coq が強力というより、Coq はインターフェースで、裏側では論理や代数(とかいうと、ひじょうに語弊があるがあえて)がはたらいている気がする、そしてそれの勉強はめんどうなので、まとまった文章があればいいとおもうけど、ボリューム大きそうだなー
2011-02-28 15:54:03
Ikegami Daisuke
@ikegami__
いいたいことは、Coq も論理もプログラムの性質の証明には、道具としては不十分なんだけど、たまにはまるとできることもあるので、やってみるといいよ的な気分で、「どんな性質でも、正しければ、証明できる、というわけではない」の視点が重要だとかいいたい
2011-02-28 15:56:11
Keigo Imai
@keigoi
@ikegami__ Applpi ( http://staff.aist.go.jp/reynald.affeldt/applpi/ ) とか使ってがんばれば並行性に関する性質も証明できるはず、しかし少なくともπ計算の線形型を知らないとだめとかいう
2011-02-28 16:07:11
Keigo Imai
@keigoi
たとえば、もしブラウザ(とそれを操作するユーザー)の挙動をπ計算モデル化して、書きたいJavaScriptプログラムをCoq+π計算で書いて、欲しい性質を証明して、最後にExtractするってのは…ああ、気が遠くなる…
2011-02-28 16:11:08
Ikegami Daisuke
@ikegami__
@keigoi affeldt さんはよい仕事していてすごいです、なんというか、プログラムの性質の証明は、知っておいたほうがいい前提がおおすぎて、まだぼくはついていけないです、すごい
2011-02-28 16:09:24