|
0
|
1 \section{検証手法}
|
|
6
|
2 本章では検証する際の手法を説明する．
|
|
|
3 CodeGear の引数となる DataGear が事前条件となり，
|
|
|
4 それを検証する為のPre Conditionを検証する為の Meta Gearsが存在する．
|
|
|
5 その後，さらに事後条件となる DetaGear も Meta Gears にて検証する．
|
|
|
6 これらを用いて Hoare Logic によりプログラムの検証を行いたい．
|
|
0
|
7
|
|
|
8 \subsection{CbC記法で書くagda}
|
|
6
|
9 CbCプログラムの検証をするに当たり，AgdaコードもCbC記法で記述を行う．つまり継続渡しを用いて記述する必要がある．
|
|
|
10 \coderef{agda-cg}が例となるコードである．
|
|
0
|
11
|
|
|
12 \lstinputlisting[caption= Agdaでの CodeGear の例, label=agda-cg]{src/cbc-agda.agda}
|
|
|
13
|
|
6
|
14 前述した加算を行うコードと比較すると，不定の型 (t) により継続を行なっている部分が見える．
|
|
|
15 これがAgdaで表現された CodeGear となる．
|
|
0
|
16
|
|
|
17 \subsection{agda による Meta Gears}
|
|
6
|
18 通常の Meta Gears はノーマルレベルの CodeGear， DataGear では扱えないメタレベルの計算を扱う単位である．
|
|
|
19 今回はその Meta Gears をAgdaによる検証の為に用いる．
|
|
0
|
20
|
|
|
21 \begin{itemize}
|
|
|
22 \item Meta DataGear \mbox{}\\
|
|
6
|
23 Agda 上で Meta DataGear を持つことでデータ構造自体が関係を持つデータを作ることができる．
|
|
|
24 これを用いることで，仕様となる制約条件を記述することができる．
|
|
0
|
25
|
|
|
26 \item Meta CodeGear\mbox{}\\
|
|
|
27 Meta CodeGear は 通常の CodeGear では扱えないメタレベルの計算を扱う CodeGear
|
|
6
|
28 である．Agda での Meta CodeGear は Meta DataGear を引数に取りそれらの関係を返
|
|
|
29 す CodeGear である．故に，Meta CodeGear は Agda で記述した CodeGear の検証そのものである
|
|
0
|
30 \end{itemize}
|
|
|
31
|
