\chapter{まとめ}

本論文では、Agda による CbCの検証方法と Gears Agda による
Left Learning Red Black Tree の実装について述べた。
したがって、Gears Agda で再起処理と再代入を含んだ
複雑なアルゴリズムも記述できる事が判明した。
今回の研究中に複雑なアルゴリズムを Gears Agda にて実装することで
得られた知見は、今後の研究で大いに役立つと考える。

今後の課題として、検証を行う事が挙げられる。
検証には、Meta Code Gear が Pre / Post Condition の条件を
満たしているのか比較を行い、Hoare Logicに当てはめる事。
そして接続された条件の接続と健全性の証明を行う必要がある。
しかし、Imple を用いた Hoare Logic による証明は、
While Loop でも かなり長いコードになっていた。
これで Left Learning Red Black Tree の検証を
行うのは難しいため、別の手法を模索することも念頭に入れる。

展望としては、Gears Agda コードから CbC コードの変換をしたい。
Gears Agda は Agda の記述方法が特殊である事がコーディングを複雑にしているが、
CbC はC言語とアセンブラの中間に位置しているため、コーディングはさらに困難である。
そのため、Gears Agdaのコードを CbC に変換できるようにしたい。
これができるようになれば、CbC での記述も Agda での証明も容易になると考えている。