|
0
|
1 \section{Gears Agda における木構造の設計}
|
|
|
2
|
|
6
|
3 本研究では，Gears Agda にて Red Black Tree の検証を行うにあたり，
|
|
|
4 Agda が変数に対して再代入を許していないことが問題になってくる．
|
|
0
|
5
|
|
6
|
6 そのため下図 \ref{rbt-stack} のように，木構造の root から leaf に 辿る際に見ているnodeから
|
|
|
7 下の tree をそのまま stack に持つようにする．
|
|
0
|
8
|
|
6
|
9 そして insert や delete を行った後に stack から tree を取り出し，
|
|
|
10 元の木構造を再構築 していきながら rootへ戻る．
|
|
0
|
11
|
|
|
12 \begin{figure}[H]
|
|
|
13 \begin{center}
|
|
|
14 \includegraphics[height=3.5cm]{fig/rbt-stack.pdf}
|
|
|
15 \end{center}
|
|
|
16 \caption{tree を stack して目的の node まで辿った場合の例}
|
|
|
17 \label{rbt-stack}
|
|
|
18 \end{figure}
|
|
|
19
|
|
|
20
|
|
6
|
21 このようにして Gears Agda にて Red Black Tree を実装していく．
|
|
0
|
22
|
|
|
23 \section{Gears Agda における Binary Tree の実装}
|
|
|
24
|
|
6
|
25 Red Black Tree を実装しそれを検証する前段階として，
|
|
|
26 実装が簡単な Binary Tree の実装から行う．
|
|
0
|
27
|
|
6
|
28 まず Binary Tree と 遷移させる Data Gear となる Env の定義は Code \ref{bt_env} のようになる．
|
|
0
|
29
|
|
|
30 \lstinputlisting[label=bt_env, caption=Binary Tree の Data Gear] {src/bt_impl/bt_env.agda.replaced}
|
|
|
31
|
|
6
|
32 bt は，木での順序としての意味を持つ key とその中身 value はどのような型でも入れられるように
|
|
|
33 「A : Set n」となっている．
|
|
|
34 そして left, right には bt A を持つようにし，木構造を構築している．
|
|
0
|
35
|
|
6
|
36 Env では， find, insert, delete の対象となる値を保存し， Code Gear に与えられるようにするために
|
|
|
37 varn, varv を持っている．
|
|
|
38 加えて変更を加える bt を持つ vart と，章Nで前述した木構造を持っておくための List である
|
|
|
39 varl を Env に設定している．
|
|
0
|
40
|
|
|
41 7章で述べた Gears Agda での木構造を保ったまま root から目的のnodeまで辿る Code Gear が
|
|
6
|
42 Code \ref{bt_find_impl} になる．
|
|
0
|
43
|
|
|
44 \lstinputlisting[label=bt_find_impl, caption=root から目的のnodeまで辿る Code Gear] {src/bt_impl/find.agda.replaced}
|
|
|
45
|
|
6
|
46 まず，関数の実装が始まってすぐに Env の vartを指定したものと引数をそのまま find-c の関数に遷移している．
|
|
|
47 ここで展開しているのは Env の vart で，そのまま Env から展開した vart をパターンマッチすると
|
|
|
48 Agda が追えなくなってしまい，\{-$\#$ TERMINATING $\#$-\} を使用することになってしまう．
|
|
0
|
49
|
|
6
|
50 そのため関数を新たに定義し，展開したものを受け取り，パターンマッチすることで
|
|
0
|
51 \{-$\#$ TERMINATING $\#$-\} を使用せずに loopを定義できるようになる
|
|
|
52
|
|
6
|
53 木を stack に入れるのは単純で，操作の対象の key となる varn と
|
|
|
54 node のkeyを比較を行う．
|
|
|
55 そこからは本来の木構造と同じで，操作の対象の key が小さいなら
|
|
|
56 left の tree を次の node として遷移する．
|
|
|
57 大きいなら right の tree を次の node として遷移していく．
|
|
0
|
58
|
|
6
|
59 操作の対象となる node に辿り着き，操作を行った後，
|
|
|
60 Stack に持っている tree から再構築を行う．
|
|
0
|
61
|
|
|
62 そのコードが Code \ref{bt_replace_impl} となる
|
|
|
63
|
|
|
64 \lstinputlisting[label=bt_replace_impl, caption=Stack から tree を再構築する Code Gear] {src/bt_impl/replace.agda.replaced}
|
|
|
65
|
|
6
|
66 これも Code \ref{bt_find_impl} と同じように構成されており，
|
|
|
67 varn と node の key を比較し， vart を List から持ってきた node の どこに加えるかを決めるようになっている．
|
|
0
|
68
|
|
6
|
69 以上の流れを繋げることで， Binary Tree の insert と find を実装できた．
|
|
|
70 delete は insert の値を消すようにすると実装ができる．
|
|
0
|
71
|
|
|
72 \section{Gears Agda における Binary Tree の検証}
|
|
|
73
|
|
6
|
74 検証も前述した While Loop の 検証と同じようにしていく．
|
|
|
75 しかし， Binary Tree の不変条件は2つ以上あるため，これを関数定義の際に全て書くと
|
|
|
76 煩雑になってしまうため，事前に記述して関数化しておく．
|
|
|
77 それが Code \ref{bt_invariant} になる．
|
|
0
|
78
|
|
|
79 \lstinputlisting[label=bt_invariant, caption=Binary Tree の 不変条件] {src/bt_verif/invariant.agda.replaced}
|
|
|
80
|
|
6
|
81 この不変条件は， treeInvariant が tree の 左にある node の key が小さく，
|
|
|
82 右にある node の方が大きいことを条件としている．
|
|
0
|
83
|
|
6
|
84 stackInvariant は Stack にある tree が，次に取り出す Tree の一部であることを
|
|
|
85 条件としている．
|
|
0
|
86
|
|
6
|
87 これを先ほど実装した Code Gear に対して加えることで検証していく．
|
|
|
88 先ほど実装した Code \ref{bt_find_impl} に対して加えると Code ref のようになる．
|
|
0
|
89
|
|
|
90
|
|
|
91 \lstinputlisting[label=bt_invariant, caption=Binary Tree の 不変条件] {src/bt_verif/find.agda.replaced}
|
|
|
92
|
|
|
93 現時点では条件を満たしていることの証明まで行っていないが
|
|
6
|
94 コード中の {!!} に記述を行い，前述した While Loop と同じように中身を記述することで検証を行える．
|
|
0
|
95
|
|
|
96 \section{まとめと今後の課題}
|
|
6
|
97 本論文では，Gears Agda にて Hoare Logic を用いて While Loop の検証を行えた．
|
|
|
98 これはプログラムが Code Gear という単位で分かれているため，
|
|
|
99 一つ一つの Code Gear に対して検証を行いながら実装を行っていくことも可能である．
|
|
|
100 そのため，従来の検証手法よりもスコープが小さく，簡単に検証と実装を行えると考える．
|
|
0
|
101
|
|
6
|
102 今後の課題として，Gears Agda による Red Black Tree の実装と検証を行う必要がある．
|
|
|
103 While Loop と同じように検証を行えると考えているが，研究目的である
|
|
|
104 「ループが存在し，かつ再代入がプログラムに含まれるデータ構造」を
|
|
|
105 Gaers Agda を実装することが難しく，それをさらに検証しなければならない．
|
|
0
|
106
|
|
|
107
|
|
|
108
|
