edubase勉強会Week - Formal Methods Forum

ustream

国立情報学研究所のお力をお借りして、
今回の発表をustreamにしていただきました。
http://www.ustream.tv/recorded/16660035
http://www.ustream.tv/recorded/16660582

振り返り議論

その場にいらっしゃった方の発言を適当にちりばめます。

  • 形式手法に対して懐疑的な意見として、「仕様書を書くのがプログラミングと同じになってしまう」というのがある
    • 上流にコストをかけるのは確かに効果がある。

たとえば、Haskell,OCaml,Schemeで同じプログラムを書いたとき、
Haskell,OCamlはSchemeの半分の時間でプログラムが完成した。
型の無い言語はとりあえず動かせるが、デバッグに時間がかかる。
型の厳密な言語はそもそもコンパイルを通すまでに時間がかかるが、
結局デバッグの時間が減るので元がとれている。

    • どこかで厳密な仕様にしないと、プログラミングに移れないのは確かである。
    • 上流成果物のすべてが形式記述になるべきだとは思わないが、上流の時点で論理的に検証すべき内容も確かにある。（実装のミスは割とすぐに直せるが、設計のミスは影響が大きすぎて直せないことがある）
  • 形式手法の適用例としてでてくるのは、図書館の貸し出しとか「特定の閉じられた世界」になっているのではないか
    • "Coders at Work"に出ていたが、現実の問題はもっと複雑で、形式手法は役に立たないとの話があった。
    • 形式記述のスキルよりも、ドメインの知識が絶対的に必要になってくる。ある手法が適用できるかどうかは、むしろドメインの知識にかかってくる。
    • 形式手法のモデルのサンプルが足りないのではないか。どう使えるのかがわからない、イメージできないのでは普及も難しい。
    • ドメインの知識を持ち、かつ形式記述のサンプルを見て、「ピン」をこなければ使えない、という状況になっている。
    • モデリングをする際に、モデル化対象以外までモデリングしなければいけないことがあり、さじ加減が難しい。
    • Coqで勉強会をやっている経験上、難しいのは、適切な規模のサンプルを見つけること。1行のコードに100行の証明、ということもある。

その他メモ

Alloy Analyzer入門 @kencoba
形式手法2.0 & 証明付きDSL @tmiya_

これ以外のツールも興味あるんだけど、とりあえず一つのツールを使えるようになりたい。
他のツールもやりたい人がいたらやりましょう。

    • 仕様アニメーション:実装前に動かす
    • モデル検査:網羅的にチェック
    • 定理証明系:プログラムを検証
  • 定理証明系とは?
    • プログラムの正しさを証明する
    • Gentzenの自然演繹
  • 証明って面倒なんでしょ?
    • 計算機にコードレビューしてもらうと思えばよい
    • 証明系＝型検査器＝コンパイラみたいなもの
  • ドメイン固有言語
    • Mechanized Metatheory
    • s70810-89.pdf
    • AURA: A Programming Language for Authorization and Audit" 2008 ICFP
    • 世の中の誰でもが証明できるべき、ともいえないけど、
    • フレームワーク作る人はできてもよいよね。
Coq入門

モデル検査は反例さがしができるのは強い。
CoqからJavaScriptのコードを生成する仕組みを作った人もいるよ