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

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

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

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

そのため下図 \ref{fig: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 と 遷移させる Data Gear となる Env の定義は Code \ref{bt_env} のようになる．

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

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

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

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

\lstinputlisting[label=bt_find_impl, caption=root から目的のnodeまで辿る Code Gear] {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 から再構築を行う．

そのコードが Code \ref{bt_replace_impl} となる

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

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

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

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

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

\lstinputlisting[label=bt_invariant, caption=Binary Tree の 不変条件] {src/bt_verif/invariant.agda.replaced}

この不変条件は， treeInvariant が　tree の 左にある node の key が小さく，
右にある node の方が大きいことを条件としている．

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

これを先ほど実装した Code Gear に対して加えることで検証していく．
先ほど実装した Code \ref{bt_find_impl} に対して加えると Code ref のようになる．


\lstinputlisting[label=bt_invariant, caption=Binary Tree の 不変条件] {src/bt_verif/find.agda.replaced}

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