annotate paper/tex/future.tex @ 14:a63df15c9afc default tip

DONE
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Mon, 15 Feb 2021 23:36:39 +0900
parents 68485f45c265
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
11
1cde48f23236 FIN proto
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
1 \chapter{まとめ}
3
959f4b34d6f4 add final thesis
soto
parents:
diff changeset
2
11
1cde48f23236 FIN proto
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
3 本論文では、Agda による CbCの検証方法と Gears Agda による
1cde48f23236 FIN proto
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
4 Left Learning Red Black Tree の実装について述べた。
1cde48f23236 FIN proto
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
5 したがって、Gears Agda で再起処理と再代入を含んだ
1cde48f23236 FIN proto
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
6 複雑なアルゴリズムも記述できる事が判明した。
1cde48f23236 FIN proto
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
7 今回の研究中に複雑なアルゴリズムを Gears Agda にて実装することで
1cde48f23236 FIN proto
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
8 得られた知見は、今後の研究で大いに役立つと考える。
3
959f4b34d6f4 add final thesis
soto
parents:
diff changeset
9
11
1cde48f23236 FIN proto
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
10 今後の課題として、検証を行う事が挙げられる。
1cde48f23236 FIN proto
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
11 検証には、Meta Code Gear が Pre / Post Condition の条件を
1cde48f23236 FIN proto
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
12 満たしているのか比較を行い、Hoare Logicに当てはめる事。
1cde48f23236 FIN proto
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
13 そして接続された条件の接続と健全性の証明を行う必要がある。
1cde48f23236 FIN proto
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
14 しかし、Imple を用いた Hoare Logic による証明は、
1cde48f23236 FIN proto
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
15 While Loop でも かなり長いコードになっていた。
1cde48f23236 FIN proto
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
16 これで Left Learning Red Black Tree の検証を
1cde48f23236 FIN proto
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
17 行うのは難しいため、別の手法を模索することも念頭に入れる。
3
959f4b34d6f4 add final thesis
soto
parents:
diff changeset
18
11
1cde48f23236 FIN proto
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
19 展望としては、Gears Agda コードから CbC コードの変換をしたい。
1cde48f23236 FIN proto
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
20 Gears Agda は Agda の記述方法が特殊である事がコーディングを複雑にしているが、
12
68485f45c265 ADD slide
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
21 CbC はC言語とアセンブラの中間に位置しているため、コーディングはさらに困難である。
68485f45c265 ADD slide
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
22 そのため、Gears Agdaのコードを CbC に変換できるようにしたい。
68485f45c265 ADD slide
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
23 これができるようになれば、CbC での記述も Agda での証明も容易になると考えている。
3
959f4b34d6f4 add final thesis
soto
parents:
diff changeset
24