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

%% ここかその前にinvariantの説明した方がよい？

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

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

\lstinputlisting[label=code:while_init_cg, caption=DataGear の定義を行う CodeGear] {src/while_loop_impl/init_cg.agda.replaced}

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

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

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

これらの CodeGear を繋げることで、 While Loop を行う \coderef{while-loop2} を実装することができる。

\lstinputlisting[label=code:while-loop2, caption=While Loop を行う CodeGear] {src/while_loop_impl/while_loop_c.agda.replaced}

\subsection{While Loop の検証}

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

検証を行う CodeGear も Gears Agda による単純な実装と同じく DataGear から行う。\coderef{while_verif_init_cg} がそれに当たる。

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

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

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

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

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

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

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

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

ここまでで定義した Pre / Post Consition が付いている CodeGear を繋げることで、
停止性以外の While Loop の検証を行う CodeGear を実装できる。\coderef{loop_verif_cg2}のようになる。

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

\coderef{loop_verif_cg3} 停止性の検証も行う While Loop の検証を行う CodeGear を実装する

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

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

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

そしてこれらを繋げて While Loop の検証を行える\coderef{loop_verif_cg4} を実装できた。

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