\section{Gears Agda にて Hoare Logic を用いた検証の例}
ここでは Gears Agda にて Hoare Logic を用いた検証の例として、
 While Loop プログラムを実装・検証する。

\subsection{While Loop の実装}
まずは前述した Gears Agda の記述形式に基づいて While Loop を実装する。
実装はまず、 Code \ref{while-loop-dg} のように Code Gear に遷移させる Data Gear の定義から行う。
\lstinputlisting[label=while-loop-dg, caption=Data Gearの定義] {src/while_loop_impl/while_loop_dg.agda.replaced}

そのため最初の Code Gear は引数を受け取り、Envを作成する Code Gear となる Code \ref{while_init_cg}。

\lstinputlisting[label=while_init_cg, caption=Data Gear の定義を行う Code Gear] {src/while_loop_impl/init_cg.agda.replaced}

次に、目的である While Loop の実装を行う。ソースコードは Code \ref{while-loop} のようになる。

\lstinputlisting[label=while-loop, caption=Loop の部分を担う Code Gears] {src/while_loop_impl/while_loop.agda.replaced}

また Agda では停止性の検出機能が存在し、
プログラム中 に停止しない記述が存在するとコンパイル時にエラーが出る。
その場合は関数定義の直前に
\{-$\#$ TERMINATING $\#$-\} のタグを付けると
停止しないプログラムをコンパイルすることができる

これまでの Code Gear を繋げることで、 While Loop　を行う Code を実装することができる。

\lstinputlisting[label=while-loop, caption=While Loop を行う Code Gear] {src/while_loop_impl/while_loop_c.agda.replaced}

\subsection{While Loop の検証}

Gears Agda にて行なった While Loop の実装コードを元に、
5章にて述べた Pre / Post Condition を記述していくことで
Hoare Logic を用いた検証を行う。

検証を行う Code Gear も Gears Agda による単純な実装と同じく Data Gear の定義から行う。Code \ref{while_verif_init_cg} がそれに当たる。

\lstinputlisting[label=while_verif_init_cg, caption=While Loop を行う Code Gear] {src/while_loop_verif/init_cg.agda.replaced}

今回は検証を行いたいため 5.1 で述べたように、実装に加えて Pre / Post Condition を持つ必要がある。
init時の Pre Condition のみ特殊で　Agda での関数定義の際に記述し、
「Data Gear に正しく初期値が設定される」という条件を使用する。これが
((vari env) $\equiv$ 0) $\wedge$ ((varn env) $\equiv$ c10)
に当たる。
そしてinit時以外の、Pre Condition と Post Condition には実行開始から実行終了までの間で不変の条件を記述する。
今回は While Loop の不変条件として、
$今回loopさせたい回数(c10) = 残りのloopする回数(vern) + 今回loopした回数(vari)$
を設定した。これがinit時の Post Condition となる。

また、init時の Pre Condition と同じ値で
Post Condition を設定しなければならない。
init時の Pre Condition を Post Condition に変換する Code \ref{conversion} を記載する。

\lstinputlisting[label=conversion, caption=init時の Pre Condition を Post Condition に変換する Code Gear] {src/while_loop_verif/conversion.agda.replaced}

ここで変換されて作成された Post Condition はプログラム実行中の不変条件となるため、
この後の Pre / Post Condition は停止するまでこれを用いる。

以下の Code \ref{loop_verif_cg} は停止性の検証を行っていないが、 Wile Loop の Loop 部分の検証を行う Code Gear となる。

\lstinputlisting[label=loop_verif_cg, caption=停止性以外の Loop の検証も行う Code Gear] {src/while_loop_verif/while_loop.agda.replaced}

Loop が停止することを示していないため、関数定義の直前に \{-\# TERMINATING \#-\} が記述されている。
こちらも Loop の実装以外に、Pre / Post Condition を満たしているか検証を行い、次の Code Gear に渡している。

ここまでで定義した Pre / Post Consition が付いている Code Gear を繋げることで、
停止性以外の While Loop の検証を行う Code Gear を実装できる。

\lstinputlisting[label=loop_verif_cg, caption=停止性以外の While Loop の検証を行う Code Gear] {src/while_loop_verif/verif_term.agda.replaced}

停止性の検証も行う While Loop の検証を行う Code Gear を実装する

\lstinputlisting[label=loop_verif_cg, caption=停止性の検証も行う Loop 部分の Code Gear] {src/while_loop_verif/verif_loop.agda.replaced}

停止することを Agda が理解できるように記述すると良い。
そのため引数に減少していく変数 reduce を追加し、
loop するとデクリメントするように実装する。

loop には先ほど実装した loop の部分を担う Code Gear が次の関数遷移先を引数に受け取れるようにした
whileLoopSeg を使用する。

そしてこれらを繋げて While Loop の検証を行うことができる Code ref を実装できた。

\lstinputlisting[label=loop_verif_cg, caption=停止性の検証も行う While Loop の Code Gear] {src/while_loop_verif/verif.agda.replaced}