Mercurial > hg > Papers > 2020 > soto-midterm

comparison tex/future.tex @ 11:a8bc8c6b48bd default tip

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author soto@cr.ie.u-ryukyu.ac.jp
date Tue, 15 Sep 2020 07:06:29 +0900
parents 27a6616b6683
children
comparison
equal deleted inserted replaced
10:c162ca9b997e 11:a8bc8c6b48bd
1 \section{今後の課題} 1 \section{今後の課題}
2 今後の課題として、以下が挙げられる。 2 今後の課題として、以下が挙げられる。
3 赤黒木の基本操作として insert や delete が挙げられる。 3 RedBlackTree の基本操作として insert や delete が挙げられる。
4 通常は、再代入などを用いて実装を行うと思われるが、agda が変数への代入を許していないため、 4 通常は、再代入などを用いて実装を行うと思われるが、Agda が変数への代入を許していないため、
5 操作後の赤黒木を再構成するように実装を行う必要がある。 5 操作後の RedBlackTree を再構成するように実装を行う必要がある。
6 その際にどこの状態の検証を行うかが課題になっている。 6 その際にどこの状態の検証を行うかが課題になっている。
7 7
8 先行研究にて、 8 先行研究にて、
9 個々の Code Gear の条件を書いてそれを接続することは agda で実装されている。 9 個々の Code Gear の条件を書いてそれを接続することは Agda で実装されている。
10 しかし、接続された条件が健全であるか証明されていない。 10 しかし、接続された条件が健全であるか証明されていない。
11 11
12 今後はこの接続された条件の健全性の証明からしていく。 12 証明されていない部分というのは、プログラム全体はいくつかの Code Gear の集まりだが、
13 Code Gear 実行後の事後条件が正しく次に実行される Code Gear の事前条件として成り立っているか、
14 それが最初からプログラムの停止まで正しく行われているかという部分である。
15
16 今後はこの接続された条件の健全性の証明から行っていく。