Mercurial > hg > Papers > 2021 > soto-thesis

comparison paper/tex/rbt_verif.tex @ 14:a63df15c9afc default tip

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 Mon, 15 Feb 2021 23:36:39 +0900
parents 4361e7b7d3db
children
comparison
equal deleted inserted replaced
13:4361e7b7d3db 14:a63df15c9afc
1 \chapter{Red Black Tree の検証} 1 \chapter{Left Learning Red Black Tree の検証}
2 実装が困難であったため、検証するまでには至らなかった。 2 本章では、Left Learning Red Black Tree の
3 検証方法について述べる
3 4
4 \section{Meta Data Gearの記述} 5 \section{Meta Data Gearの記述}
5 検証するにあたり、Meta Deta Gear を作成し Pre / Post Condition と 6 検証するにあたり、Meta Deta Gear を作成し Pre / Post Condition と
6 比較することで Hoare Triple に当てはめることは第5章で前述した。 7 比較することで Hoare Triple に当てはめることは第5章で前述した。
7 \subsection{大小関係を検証する Meta Data Gear} 8 \subsection{大小関係を検証する Meta Data Gear}
44 insert-r は right-List に 値を insert するための関数で、 45 insert-r は right-List に 値を insert するための関数で、
45 right-List の top と入れる引数を比較し、 46 right-List の top と入れる引数を比較し、
46 inserする際は値とその証明の両方を持つ事で 証明付き Data 構造を 47 inserする際は値とその証明の両方を持つ事で 証明付き Data 構造を
47 持った List となっている。 48 持った List となっている。
48 49
50 これを Left Learning Red Black Tree の 仕様を満たすように、
51 全てに対して行う。
52 その後、条件が接続されているのかを検証したのち、健全性について示す事で
53 Hoare Logic による検証ができる。
49 54
50 55
51 以上を用いて Meta Data Gear を作成する Gears Agda は以下になる。
52 56
53
54 これを用いることで、各 node より上の node の大小関係を検証できると考えた。
55 57
56 %\subsection{Black node の数え上げ} 58 %\subsection{Black node の数え上げ}
57 %他にも、Left Learning Red Brack Tree の black node の数え上げを記述した。 59 %他にも、Left Learning Red Brack Tree の black node の数え上げを記述した。
58 60
59 %\subsection{Meta Data Gear の作成} 61 %\subsection{Meta Data Gear の作成}