# 研究目的
- 愚直にプログラムを書くと、冗長なコードができてしまい、実行時間も遅くなることがある。
	- この場合に、コードに対してアルゴリズムを適応すると実行が最適化され実行時間が減り、かつ第三者がコードを読んだ場合にロジックが統一さてれいるため理解が容易くなる。一般的に言う良いコードが作成できる。
- しかし、世の中にはアルゴリズムが大量にあり、これを一人のプログラマーが全て覚え、また適応できる場面を思いつくというのは不可能
- そのため、人が愚直に書いたコードに対してアルゴリズムを使用するコードを自動で適用できるようにしたい

- この場合、アルゴリズム適用前と適用後で同じコードになっていることを証明するのは難しい。
	- 普通のプログラミング言語では恒等性を示す根拠が足りない

- また、普通のプログラミング言語では、関数の遷移が自由であることにより、関数遷移などで発生した暗黙の環境(変数)が存在するため、アルゴリズムの適応を行うのは難しい

- ここで、当研究室で開発している Gears Agda を用いる。
    - Gears Agdaとは当研究室で開発している Continuetion based C (CbC)の概念を取り入れた記法
	- 通常関数を遷移する際にはメインルーチンからサブルーチンに遷移する。この際メインルーチンで使用していた変数などの環境はスタックされる。しかしCbCの継続ではjmp命令で関数遷移を行い、スタックを持たず環境を保存しない。これにより暗黙な環境が存在せず検証がしやすくなる。

- アルゴリズムの適用は現状以下の方法を考えている

- Gears Agda にてあらかじめアルゴリズムの実装と検証を行ったアルゴリズムSetsを用意する

- 事前に定義していたアルゴリズムのInvariantが書いたCodeGearに当てはめられるのかを調べていく
    - 当てはまる場合にアルゴリズムを入れ替える

## SIGOSに出す研究の目的
- モデル検査といえば主流はSPIN
- しかし、上述したアルゴリズム入れ替えの可否判定にはGears Agda 内部でモデル検査をするのが最も妥当であると考えている。
    - バブルソートをマージソートに変える場合では定理証明を行っても内部動作が一致しないので、定理証明を行ったあとに使えない。
    - (そもそも何も考えずに書いたコードを定理証明で証明するのはコストが高い)
    - モデル検査でアルゴリズム側の不変条件(INvariant)を入れ替え元のCode Gearが満たしている場合に
      入れ替える形になる。
    - つまり、そのコード中で不変条件を満たしているのかをモデル検査で検証を行う
- このことから、Gears Agda上でモデル検査を行う。

- 課題として、Agda上では並列実行ができない。


## 今週の進捗
- 研究の申込みをした
- mercurialにリポジトリを用意した
- モデル検査について調べていた
    - DPPをSPINで解いているものがあったので動かしたり遊んでみた

- GearsAgda上のモデル検査
    - DPP入力の網羅とかはいつかなかったのでassartの例題を作るなどしていた
    - DPPの実装も並列の表現方法が思いついていない

### assertについて
- Meta Code Gearのように普通のMeta Code Gearの間に
  はさもうと考えています。(現在はBoolが入っていますが…)
- 欲を言えばassertにLTLが記述できるようになりたい
- Meta Data GearはData Gearをwrapしてassert errorを格納できるとよいかと思っています。

![meta_cg_dg.pdf](http://www.cr.ie.u-ryukyu.ac.jp/hg/Papers/2022/soto-sigos/raw-file/tip/Paper/fig/meta_cg_dg.pdf)