Mercurial > hg > Papers > 2022 > soto-sigos

comparison Paper/tex/future.tex @ 6:9ec2d2ac1309

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
DONE 一度これで提出
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Thu, 05 May 2022 22:32:45 +0900
parents 14a0e409d574
children
comparison
equal deleted inserted replaced
5:6c0b1fcbac2d 6:9ec2d2ac1309
1 \chapter{まとめ} 1 \chapter{まとめ}
2 2
3 本論文では、Agda による CbCの検証方法と Gears Agda による 3 本論文では，Agda による CbCの検証方法と Gears Agda による
4 Left Learning Red Black Tree の実装について述べた。 4 Left Learning Red Black Tree の実装について述べた．
5 したがって、Gears Agda で再起処理と再代入を含んだ 5 したがって，Gears Agda で再起処理と再代入を含んだ
6 複雑なアルゴリズムも記述できる事が判明した。 6 複雑なアルゴリズムも記述できる事が判明した．
7 今回の研究中に複雑なアルゴリズムを Gears Agda にて実装することで 7 今回の研究中に複雑なアルゴリズムを Gears Agda にて実装することで
8 得られた知見は、今後の研究で大いに役立つと考える。 8 得られた知見は，今後の研究で大いに役立つと考える．
9 9
10 今後の課題として、検証を行う事が挙げられる。 10 今後の課題として，検証を行う事が挙げられる．
11 検証には、Meta Code Gear が Pre / Post Condition の条件を 11 検証には，Meta Code Gear が Pre / Post Condition の条件を
12 満たしているのか比較を行い、Hoare Logicに当てはめる事。 12 満たしているのか比較を行い，Hoare Logicに当てはめる事．
13 そして接続された条件の接続と健全性の証明を行う必要がある。 13 そして接続された条件の接続と健全性の証明を行う必要がある．
14 しかし、Imple を用いた Hoare Logic による証明は、 14 しかし，Imple を用いた Hoare Logic による証明は，
15 While Loop でも かなり長いコードになっていた。 15 While Loop でも かなり長いコードになっていた．
16 これで Left Learning Red Black Tree の検証を 16 これで Left Learning Red Black Tree の検証を
17 行うのは難しいため、別の手法を模索することも念頭に入れる。 17 行うのは難しいため，別の手法を模索することも念頭に入れる．
18 18
19 展望としては、Gears Agda コードから CbC コードの変換をしたい。 19 展望としては，Gears Agda コードから CbC コードの変換をしたい．
20 Gears Agda は Agda の記述方法が特殊である事がコーディングを複雑にしているが、 20 Gears Agda は Agda の記述方法が特殊である事がコーディングを複雑にしているが，
21 CbC はC言語とアセンブラの中間に位置しているため、コーディングはさらに困難である。 21 CbC はC言語とアセンブラの中間に位置しているため，コーディングはさらに困難である．
22 そのため、Gears Agdaのコードを CbC に変換できるようにしたい。 22 そのため，Gears Agdaのコードを CbC に変換できるようにしたい．
23 これができるようになれば、CbC での記述も Agda での証明も容易になると考えている。 23 これができるようになれば，CbC での記述も Agda での証明も容易になると考えている．
24 24