\section{検証手法}
本章では検証する際の手法を説明する。
CodeGear の引数となる DataGear が事前条件となり、
それを検証する為のPre Conditionを検証する為の Meta Gearsが存在する。
その後、さらに事後条件となる DetaGear も Meta Gears にて検証する。
これらを用いて Hoare Logic によりプログラムの検証を行いたい。

\subsection{CbC記法で書くagda}
CbCプログラムの検証をするに当たり、AgdaコードもCbC記法で記述を行う。つまり継続渡しを用いて記述する必要がある。
\coderef{agda-cg}が例となるコードである。

\lstinputlisting[caption= Agdaでの CodeGear の例, label=agda-cg]{src/cbc-agda.agda}

前述した加算を行うコードと比較すると、不定の型 (t) により継続を行なっている部分が見える。
これがAgdaで表現された CodeGear となる。

\subsection{agda による Meta Gears}
通常の Meta Gears はノーマルレベルの CodeGear、 DataGear では扱えないメタレベルの計算を扱う単位である。
今回はその Meta Gears をAgdaによる検証の為に用いる。

\begin{itemize}
    \item Meta DataGear \mbox{}\\
		Agda 上で Meta DataGear を持つことでデータ構造自体が関係を持つデータを作ることができる。
		これを用いることで、仕様となる制約条件を記述することができる。

	\item Meta CodeGear\mbox{}\\
		Meta CodeGear は 通常の CodeGear では扱えないメタレベルの計算を扱う CodeGear
		である。Agda での Meta CodeGear は Meta DataGear を引数に取りそれらの関係を返
		す CodeGear である。故に、Meta CodeGear は Agda で記述した CodeGear の検証そのものである
\end{itemize}