# 研究目的

愚直にプログラムを書くと、冗長なコードができてしまい、
実行時間も掛かってしまう

この場合、コードに対してアルゴリズムを適応すると、
実行が最適化され実行時間が減り、良いコードが作成できる

しかし、世の中にはアルゴリズムが大量にあり、
これを一人で全て覚え、また適応できる場面を思いつくというのは困難

そのため、人が愚直に書いたコードに対してアルゴリズムを使用するコードに
自動適用できるようにしたい（すでにあるかもしれないが）

適用前と適用後で同じコードになっていることを
保障するのは難しい。

また、普通のプログラミング言語では、関数の遷移が
自由であるため、これを行うのは難しいと考える

これによりGears Agdaにて書いたコードをアルゴリズムで
書いたコードに変更

# 今やっている研究の目的

- OS やアプリケーションの信頼性を高めることは重要な課題である。
- 信頼性を高める為にはプログラムが仕様を満たした実装を検証する必要がある。
- 具体的には「モデル検査」や「定理証明」などが検証手法としてあげられる。
- 当研究室では Continuation based C (CbC) という言語を開発している。
    - CbC とは、 C言語からループ制御構造とサブルーチンコールを取り除き、継続を導入した C 言語の下位言語である。その為、それを実装した際のプログラムが正確に動作するのか検証を行いたい。
- 検証には定理証明を用いるため、 定理証明支援器のAgda を用いる。
- agdaが変数への再代入を許していない為、ループが存在し、かつ再代入がプログラムに含まれるデータ構造である red black tree の検証を行う

# 進捗

- 卒論の際に Gears Agda で書いた left learning red black tree を reb black tree に書き直しています。