Mercurial > hg > Papers > 2021 > soto-thesis

comparison paper/tex/future.tex @ 11:1cde48f23236

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
FIN proto
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Mon, 15 Feb 2021 03:51:35 +0900
parents 959f4b34d6f4
children 68485f45c265
comparison
equal deleted inserted replaced
10:2ba2fa18fc7e 11:1cde48f23236
1 \chapter{今後の課題} 1 \chapter{まとめ}
2 2
3 \section{今後の課題} 3 本論文では、Agda による CbCの検証方法と Gears Agda による
4 今後の課題として、以下が挙げられる。 4 Left Learning Red Black Tree の実装について述べた。
5 RedBlackTree の基本操作として insert や delete が挙げられる。 5 したがって、Gears Agda で再起処理と再代入を含んだ
6 通常は、再代入などを用いて実装を行うと思われるが、Agda が変数への代入を許していないため、 6 複雑なアルゴリズムも記述できる事が判明した。
7 操作後の RedBlackTree を再構成するように実装を行う必要がある。 7 今回の研究中に複雑なアルゴリズムを Gears Agda にて実装することで
8 その際にどこの状態の検証を行うかが課題になっている。 8 得られた知見は、今後の研究で大いに役立つと考える。
9 9
10 先行研究にて、 10 今後の課題として、検証を行う事が挙げられる。
11 個々の Code Gear の条件を書いてそれを接続することは Agda で実装されている。 11 検証には、Meta Code Gear が Pre / Post Condition の条件を
12 しかし、接続された条件が健全であるか証明されていない。 12 満たしているのか比較を行い、Hoare Logicに当てはめる事。
13 そして接続された条件の接続と健全性の証明を行う必要がある。
14 しかし、Imple を用いた Hoare Logic による証明は、
15 While Loop でも かなり長いコードになっていた。
16 これで Left Learning Red Black Tree の検証を
17 行うのは難しいため、別の手法を模索することも念頭に入れる。
13 18
14 証明されていない部分というのは、プログラム全体はいくつかの Code Gear の集まりだが、 19 展望としては、Gears Agda コードから CbC コードの変換をしたい。
15 Code Gear 実行後の事後条件が正しく次に実行される Code Gear の事前条件として成り立っているか、 20 Gears Agda は Agda の記述方法が特殊である事がコーディングを複雑にしているが、
16 それが最初からプログラムの停止まで正しく行われているかという部分である。 21 CbC はC言語の下位言語であり、
17 22
18 今後はこの接続された条件の健全性の証明から行っていく。 23
24