\section{Gears Agda における Binary Tree の検証}

ここでは Gears Agda にて再帰的なデータ構造を検証する例として、
Binary Tree \cite{rbtree} を実装・検証する。

\subsection{Gears Agda における木構造の設計}

本研究では、Gears Agda にて Binary Tree の検証を行う際に、
Agda が変数に対して再代入を許していないことが問題になってくる。

そのため下\figref{rbt-stack} のように、木構造の root から leaf に 辿る際に見ているnodeから
下の tree をそのまま stack に持つようにする。

そして insert や delete を行った後に stack から tree を取り出し、
元の木構造を再構築 していきながら rootへ戻る。

\begin{figure}[htpb]
  \begin{center}
   \scalebox{0.25}{\includegraphics{fig/rbt-stack.pdf}}
  \end{center}
  \caption{tree を stack して目的の node まで辿った例}
  \label{fig:rbt-stack}
\end{figure}


このようにして Gears Agda にて Binary Tree を実装していく。

\subsection{Gears Agda における Binary Tree の実装}

Binary Tree と 遷移させる DataGear となる Env の定義は \coderef{bt_env} のようになる。

\lstinputlisting[label=code:bt_env, caption=Binary Tree の DataGear] {src/bt_impl/bt_env.agda.replaced}

bt は、木での順序としての意味を持つ key とその中身 value はどのような型でも入れられるように
「A : Set n」となっている。
そして left, right には bt A を持つようにし、木構造を構築している。

Env では、 find, insert, delete の対象となる値を保存し、 CodeGear に与えられるようにするために
varn, varv を持っている。
加えて変更を加える bt を持つ vart と、前述した木構造を持っておくための List である
varl を Env に設定している。

7章で述べた Gears Agda での木構造を保ったまま root から目的のnodeまで辿る CodeGear が
\coderef{bt_find_impl} になる。

\lstinputlisting[label=code:bt_find_impl, caption=root から目的のnodeまで辿る CodeGear] {src/bt_impl/find.agda.replaced}

まず、関数の実装が始まってすぐに Env の vartを指定したものと引数をそのまま find-c の関数に遷移している。
ここで展開しているのは Env の vart で、そのまま Env から展開した vart をパターンマッチすると
Agda が追えなくなってしまい、\{-$\#$ TERMINATING $\#$-\} を使用することになってしまう。

そのため関数を新たに定義し、展開したものを受け取り、パターンマッチすることで
\{-$\#$ TERMINATING $\#$-\} を使用せずに loopを定義できるようになる。

木を stack に入れるのは単純で、操作の対象の key となる varn と
node のkeyを比較を行う。
その後、本来の木構造と同じで、操作の対象の key が小さいなら
left の tree を次の node として遷移する。
大きいなら right の tree を次の node として遷移していく。

操作の対象となる node に辿り着き、操作を行った後、
Stack に持っている tree から再構築を行う。

そのコードが \coderef{bt_replace_impl} となる。

\lstinputlisting[label=code:bt_replace_impl, caption=Stack から tree を再構築する CodeGear] {src/bt_impl/replace.agda.replaced}

これも \coderef{bt_find_impl} と同じように構成されており、
varn と node の key を比較し、vart を List から持ってきた node の どこに加えるかを決めるようになっている。

以上の流れを繋げることで、Binary Tree の insert と find を実装できた。
delete は insert の値を消すようにすると実装ができる。

\subsection{Gears Agda における Binary Tree の検証}

検証も前述した While Loop の 検証と同じようにしていく。
しかし、 Binary Tree の Invariant は2つ以上あるため、これを関数定義の際に全て書くと
煩雑になってしまうため、事前に記述して関数化しておく。
それが\coderef{bt_invariant}になる。

\lstinputlisting[label=code:bt_invariant, caption=Binary Tree の Invariant] {src/bt_verif/invariant.agda.replaced}

この Invariant は、treeInvariant が tree の 左にある node の key が小さく、
右にある node の方が大きいことを条件としている。

stackInvariant は Stack にある tree が、次に取り出す Tree の一部であることを
条件としている。

これを先ほど実装した CodeGear に対して加えることで検証していく。
先ほど実装した \coderef{bt_find_impl} に対して加えると \coderef{bt_invariant2} のようになる。


\lstinputlisting[label=code:bt_invariant2, caption=Binary Tree の検証] {src/bt_verif/find.agda.replaced}

現時点では条件を満たしていることの証明まで行っていないが
コード中の {!!} に記述を行い、前述した While Loop と同じように中身を記述することで検証を行える。