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