title: 形式手法を広めるには author: 河野真治
比嘉健太 profile: 琉球大学工学部情報工学科 lang: Japanese # Agenda * 大学ではどんなことをやっているか(講義, イベント, 研究) * ポジション(河野) * ポジション(比嘉) # 講義で使用している形式手法 * 仕様記述 * UML * model checking 的なアプローチ * Java Path Finder * 証明的なアプローチ * Haskell, Agda # 仕様記述 * モデリングと設計 の講義 * iOS Application を作成する * ユースケース図やクラス図を使って仕様を考える # model checking 的なアプローチ * [Operationg System](http://www.ie.u-ryukyu.ac.jp/%7Ekono/lecture/os/index.html) の講義 * Process/Thread Scheduling を考えた時に * Dead Lock を起こすような Scheduling を実際に書いて実行させる * Java Path Finder で Thread の実行順序を網羅的に実行する # 証明的なアプローチ * [ソフトウェア工学](http://www.ie.u-ryukyu.ac.jp/%7Ekono/lecture/software/index.html) の講義 * 集合, 論理, 関数, 自然演繹による証明 * 型システム, Curry-Howard Isomorphism を通して Haskell, Agda で証明 * Haskell : 自然演繹と lambda calculus * Agda : Category, Data type の証明 (Product, Sum, List, Functor, Monad ...) * Agda : SystemT を使った自然数に対する演算の証明 # Agda による証明を解説した例 * Open Source Conference * ソフトウェア工学で学んだ Agda を [Agda 入門](http://ie.u-ryukyu.ac.jp/~e115763/slides/events/osc2014/slide.html)として発表 * Agda で SystemT の Nat の加法の交換法則を解説 * 定義の解説にほとんどの時間を取られてしまう # 圏によるプログラムの形式化 : Delta Monad * プログラムの変更を Monad で表す * プログラムの変更時に変更前のプログラムも残したまま変更する * 全てのバージョンのプログラムを同時に実行できる * デバッグやテストと組み合せることでバグを見付けたい * 実行系と検証系を同時に走らせることもできる # ポジション(河野) * 形式手法を学習するには * 形式手法とツール * 形式手法とワークフロー * 形式手法と証明 * 形式手法の将来 # 形式手法を学習するには * 学習するには本や論文を読み、問題を一つ一つ解いていく必要がある * 長く手間がかかる作業 * 一方でルールの適用なので誰がやっても結果は同じ * 難しいのはルールの適用から意味のある結果を得ること * そこが想像できないと「わからない」ということになる * わからないのではなくて、わかることに価値を見出せなくなる # 形式手法とツール * 実際の形式ツールを使うためには * どういうツールがあるのか調べる * 環境を作ってそのツールを理解する * 使いこなすことでバグが取れたとして * その利益はどこにあるのか * 研究開発が速くなるのか, 質が良くなるのか * 理解して使う必要がある # 形式手法とワークフロー * 研究開発は分散版管理を用いて行なわれている * Pull Request, Project Management Tool などで研究状況を認識 * 分散版管理そのものは形式的に定義できると考えている * Delta Monad というものを提案している * 学んで理解する教育手順そのものを研究室のワークフローとしたい * ツールを組み込んだワークフローが有効であることを示したい * 例) Pull Requeset 単位での model checking # 形式手法と証明 * Agda は積極的に導入している * 時間がかかるので使いどころは限られる * 形式手法を学んだり証明の見落しを調べるのに便利 * 証明を研究開発の過程に組込むのは難しい * しかし方向性を示すのに用いることはできる # 形式手法の将来 * 将来的にプログラムのかなりの部分は証明される * ライブラリもほとんど論文では証明が存在する * 形式手法で示すことは信頼性のにも繋がる * しかしプログラム全体に広めるのは時間がかかるしできるか不明 * 形式手法の基本を理解し、いくつかのツールを使える人材を企業に送りこむのが良い # ポジション(比嘉) * 講義などでつまづいたポイント * つまづきの解決策 * どのような講義をするべきか? # 学習コスト * 論理, 自然演繹 -> Haskell -> Agda * それぞれのステップに壁がある * 論理とプログラム間で変換できないなど * 自然演繹では解けるけれど lambda term で書き直す * Haskell では定義できるけれど Agda で証明できない # つまづくポイント * Haskell -> Agda の壁を考える * コードを書いてる人なら型を合わせることは分かる * 型によって証明を書くことに繋げるには? * プログラムと論理の対応を把握してもらう必要がある * どうしたら把握してもらえるか? # つまづきをどう解決するか * 書き続ける * 論理とプログラムの対応を見えるようにする * Agda は対話的に項を書き換えることができる * どこでつまづいても情報が手に入るようにしたい * 論理側でも、プログラム側でも、どのステップでも * 対話的に情報を引き出す手段そのものを学ぶ # 他に講義に取りいれるもの? * 仕様記述 * 他の証明支援系 * Coq, ... * 他の理論 * Hoare Logic, Computational Tree Logic, ... * どのようなカリキュラムが良いか? # データ構造 Delta の定義 * Monad によってプログラムの変更を表す * データ構造としては長さ1以上のリスト * nil に相当するものが元のプログラムの値 * プログラムの変更は変更した後の値を List に追加する * 全ての関数は Delta を返し、値は Delta によって定義する ``` data Delta a = Mono a | Delta a (Delta a) ``` # Delta に対する Monad の instance 定義 * return はバージョンが無いプログラムをバージョン1とする * ``>>=`` は同じバージョンの値に対する計算を同時に行なう ``` instance Monad Delta where return x = Mono x (Mono x) >>= f = f x (Delta x d) >>= f = Delta (headDelta (f x)) (d >>= (tailDelta . f)) ``` # 元のプログラムとプログラムの変更 ![original_program](pictures/original_program.svg) # Delta によって記述されたプログラムの実行 ![delta_program](pictures/delta_program.svg) # Delta のメリット * 全てのバージョンを同時に実行できる * 任意のバージョンの組み合せを同時に実行できる * デバッグに利用したり 通常系/検証系 として動かす * Monad なので Category との対応がある * 2 つのバージョンを選ぶことは Delta が持つプログラムの product * 任意のバージョンを生成できる Colimit は Program の Repository