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

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

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

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

\begin{figure}[H]
  \begin{center}
    \includegraphics[height=3.5cm]{fig/rbt-stack.pdf}
  \end{center}
  \caption{tree を stack して目的の node まで辿った場合の例}
  \label{rbt-stack}
\end{figure}


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

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

Red Black Tree を実装しそれを検証する前段階として、
実装が簡単な 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 と、章Nで前述した木構造を持っておくための 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 の値を消すようにすると実装ができる。

\section{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 と同じように中身を記述することで検証を行える。

\section{まとめと今後の課題}
本論文では、Gears Agda にて Hoare Logic を用いて While Loop の検証を行えた。
これはプログラムが Code Gear という単位で分かれているため、
一つ一つの Code Gear に対して検証を行いながら実装を行っていくことも可能である。
そのため、従来の検証手法よりもスコープが小さく、簡単に検証と実装を行えると考える。

今後の課題として、Gears Agda による Red Black Tree の実装と検証を行う必要がある。
While Loop と同じように検証を行えると考えているが、研究目的である
「ループが存在し、かつ再代入がプログラムに含まれるデータ構造」を
Gaers Agda を実装することが難しく、それをさらに検証しなければならない。