\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 での証明も容易になると考えている．