11
|
1 \chapter{まとめ}
|
3
|
2
|
11
|
3 本論文では、Agda による CbCの検証方法と Gears Agda による
|
|
4 Left Learning Red Black Tree の実装について述べた。
|
|
5 したがって、Gears Agda で再起処理と再代入を含んだ
|
|
6 複雑なアルゴリズムも記述できる事が判明した。
|
|
7 今回の研究中に複雑なアルゴリズムを Gears Agda にて実装することで
|
|
8 得られた知見は、今後の研究で大いに役立つと考える。
|
3
|
9
|
11
|
10 今後の課題として、検証を行う事が挙げられる。
|
|
11 検証には、Meta Code Gear が Pre / Post Condition の条件を
|
|
12 満たしているのか比較を行い、Hoare Logicに当てはめる事。
|
|
13 そして接続された条件の接続と健全性の証明を行う必要がある。
|
|
14 しかし、Imple を用いた Hoare Logic による証明は、
|
|
15 While Loop でも かなり長いコードになっていた。
|
|
16 これで Left Learning Red Black Tree の検証を
|
|
17 行うのは難しいため、別の手法を模索することも念頭に入れる。
|
3
|
18
|
11
|
19 展望としては、Gears Agda コードから CbC コードの変換をしたい。
|
|
20 Gears Agda は Agda の記述方法が特殊である事がコーディングを複雑にしているが、
|
12
|
21 CbC はC言語とアセンブラの中間に位置しているため、コーディングはさらに困難である。
|
|
22 そのため、Gears Agdaのコードを CbC に変換できるようにしたい。
|
|
23 これができるようになれば、CbC での記述も Agda での証明も容易になると考えている。
|
3
|
24
|