\section{Gears Agda でのモデル検査}
\pagenumbering{arabic}

思い思いにプログラムを書くと,冗長なコードができてしまい,
実行時間も遅い場合がある。

この場合にコードに対してアルゴリズムを適応すると実行が最適化され
実行時間が減り,かつ第三者がコードを読んだ際にロジックが統一されているため理解が容易くなる。
つまり,一般的に良いコードが作成できる。

しかし,世の中にはすでに大量のアルゴリズムが存在するため,
これを一人のプログラマーが全て覚え,適応できる場面を思いつくというのは不可能に近い。
その道に詳しい人が複数人いる場面というのも稀だと考えられる。

そのため,人が書いたコードに対してアルゴリズムを使用するコードに変換できるようにしたい。

この際,アルゴリズム適応前後で処理が変わっていないか検証するのは普通のプログラミング言語では難しい。
一般的なプログラミング言語では,関数の遷移が自由であることから,関数遷移などで発生した
暗黙の環境が存在するためである。

この問題を解決するため,Gears Agda を用いる。

Gears Agda とは当研究室で開発している Continuation based C (CbC) の概念を取り入れた記法で書かれた Agda のことで,
通常のプログラミング言語では関数を実行する際にはメインルーチンからサブルーチンに遷移する。
この際メインルーチンで使用していた変数などの環境はスタックされ,サブルーチンが終了した際にメインルーチンに戻り,
スタックしていた変数をもとに戻す流れとなる。
CbCの場合はサブルーチンコールの際にアセンブラで言うjmpで関数遷移を行うことができ,スタックを持たず環境を保持しない。
更に遷移後にメインルーチンに戻ることもない。
つまり関数の実行では暗黙な環境が存在せず,関数が受け取った引数のみを使用する。
これにより限定的な実行条件を作成でき,検証がしやすくなる。

現在,アルゴリズムの適応可否は以下の方法を考えている。

あらかじめ,アルゴリズムの実装と検証をおこなったアルゴリズムSetsを用意しておく。

書いたコードが事前に定義していたアルゴリズムの仕様を満たしているかを検証していき,
満たしているコードがあった場合にそのコードを事前に定義してあるアルゴリズムに入れ替える方針を考えている。

この際,実装が仕様を満たしているか検証する手法には,定理証明やモデル検査などが挙げられる。

アルゴリズムの入れ替え可否判定には Gears Agda でモデル検査を行い,
アルゴリズムの仕様がコードに適応できるか検証するのが妥当だと考えている。
思い思いに書いたコードに対して定理証明を行うのはコストが高く,適応するものの内部動作が一致しない場合定理証明を行っても使えないためである。

本論文では Gears Agda でのモデル検査の先駆けとして Dining philosophers problem (DPP) のモデル検査を行う。