title: 形式手法を広めるには
author:  河野真治 <br> 比嘉健太
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

<style>
.slide.cover H2 {
    margin-top:72px;
    font-size:72px;
}
.slide.cover H3#author {
    margin-top:72px;
    font-size:42px;
}
</style>

<!-- vim: set filetype=markdown.slide: -->