\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}