\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}