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