|
3
|
1 \chapter{Red Black Tree の検証}
|
|
10
|
2 実装が困難であったため、検証するまでには至らなかった。
|
|
|
3
|
|
|
4 \section{Meta Data Gearの記述}
|
|
|
5 検証するにあたり、Meta Deta Gear を作成し Pre / Post Condition と
|
|
|
6 比較することで Hoare Triple に当てはめることは第5章で前述した。
|
|
|
7 \subsection{大小関係を検証する Meta Data Gear}
|
|
|
8 Red Black Tree は Binary Search Tree の 定義を持っているので、
|
|
|
9 parent から見て left node には parent の値より小さい値が、
|
|
|
10 right node には大きい値が入る。これを検証する必要がある。
|
|
|
11
|
|
|
12 大小関係を検証するにあたり、Fresh List を用いた検証手法が考えられた。
|
|
11
|
13 Fresh Listの記述を\coderef{fresh}に示す。
|
|
10
|
14 % ソースコードを載せる。
|
|
11
|
15 \lstinputlisting[label=fresh, caption=Fresh List の定義, firstline=47,lastline=49] {src/agda/_fresh.agda}
|
|
|
16
|
|
|
17 これを用いて Frash List への定数の insert を\coderef{fresh-test}に示す。
|
|
|
18 \lstinputlisting[label=fresh-test, caption=Fresh List への定数のinsert, firstline=10,lastline=15] {src/agda/fresh_test.agda}
|
|
10
|
19
|
|
|
20 Fresh Listは一つの値に対して、それより後の値との大小関係の証明が入っている。
|
|
11
|
21 そのため、正確性が増すが、関数内でFresh List への insert は困難であったため、
|
|
10
|
22 証明付き Data 構造を持った List を \coderef{list_v}
|
|
|
23 のように定義した。
|
|
3
|
24
|
|
11
|
25 \lstinputlisting[label=list_v, caption=証明付き Data 構造を持った List,firstline=12,lastline=30] {src/agda/rbt_varif.agda}
|
|
10
|
26 証明付き Data 構造を持った List の定義は right-List で行っている。
|
|
|
27 List の Top と比較した際に、
|
|
|
28 Topの値より大きい値でなければ insert できない。
|
|
|
29 加えて insert できた値が Top より大きい事を示す証明も持つ事ができる。
|
|
3
|
30
|
|
10
|
31 mutual は 以下の記述全てに対して掛かっている。
|
|
|
32 これは right-List の定義の中で、top-r を呼び出しており、
|
|
|
33 top-r は定義の部分で right-List を使用している。
|
|
|
34 したがって相互呼び出しとなっている。
|
|
|
35 Agdaは 逐次処理であるため、プログラムの上に宣言してある関数や型しか使用できない。
|
|
|
36 mutual を掛けることで、プログラムの下で宣言している関数や型を使用する事ができる。
|
|
|
37
|
|
|
38 right-List の定義は、何も入っていない場合は right-List で停止するようにしている。
|
|
|
39 List に一つしか値が入っていない場合は、証明付き Data 構造を持つ必要がない。
|
|
|
40 そのため特記して記述している。
|
|
|
41 List に他の値が入っている場合は、top とその次の値との比較を証明を持っている。
|
|
|
42
|
|
|
43 top-r は Listに入っている Top の値を持ってくる関数を記述している。
|
|
|
44 insert-r は right-List に 値を insert するための関数で、
|
|
|
45 right-List の top と入れる引数を比較し、
|
|
|
46 inserする際は値とその証明の両方を持つ事で 証明付き Data 構造を
|
|
|
47 持った List となっている。
|
|
3
|
48
|
|
|
49
|
|
10
|
50
|
|
|
51
|
|
|
52 以上を用いて Meta Data Gear を作成する Gears Agda は以下になる。
|
|
|
53
|
|
|
54
|
|
|
55 これを用いることで、各 node より上の node の大小関係を検証できると考えた。
|
|
3
|
56
|
|
10
|
57 %\subsection{Black node の数え上げ}
|
|
|
58 %他にも、Left Learning Red Brack Tree の black node の数え上げを記述した。
|
|
|
59
|
|
|
60 %\subsection{Meta Data Gear の作成}
|
|
|
61
|
|
|
62
|
|
|
63
|
|
|
64
|
