Mercurial > hg > Papers > 2023 > soto-master
view Paper/tex/while_loop.tex @ 16:40a9af45b375
fix
author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Thu, 02 Feb 2023 17:49:33 +0900 (2023-02-02) |
parents | eaef105dff41 |
children | 785dd684c529 |
line wrap: on
line source
\section{Gears Agda にて Hoare Logic を用いた検証の例} ここでは Gears Agda にて Hoare Logic を用いた検証の例として, While Loop プログラムを実装・検証する. %% ここかその前にinvariantの説明した方がよい? \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 を行う \coderef{while-loop} を実装することができる. \lstinputlisting[label=code:while-loop, caption=While Loop を行う Code Gear] {src/while_loop_impl/while_loop_c.agda.replaced} \subsection{While Loop の検証} While Loop の実装コードを元に,前述した 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 の検証を行える\coderef{loop_verif_cg} を実装できた. \lstinputlisting[label=code:loop_verif_cg, caption=停止性の検証も行う While Loop の Code Gear] {src/while_loop_verif/verif.agda.replaced}