\section{Hoare Logic}
Hoare Logic\ref{hoare} とは C.A.R Hoare，
R.W Floyd が考案したプログラムの検証の手法である．
これは，「プログラムの事前条件(P)が成立しているとき，コマンド(C)実行して停止すると事後条件(Q)が成り立つ」
というもので，CbCの実行を継続するという性質に非常に相性が良い．
Hoare Logic を表記すると以下のようになる．
$$ \{P\}\ C \ \{Q\} $$
この3つ組は Hoare Triple と呼ばれる．

Hoare Triple の事後条件を受け取り，
異なる条件を返す別の Hoare Triple を繋げることでプログラムを記述していく．

Hoare Logic の検証では，
「条件がすべて正しく接続されている」かつ「コマンドが停止する」ことが必要である．
これらを満たし，
事前条件から事後条件を導けることを検証することで Hoare Logic の健全性を示すことができる．

\subsection{Hoare Logic による Code Gear の検証手法 }

\figref{hoare}が agda にて Hoare Logic を用いて Code Gear を検証する際の流れになる．
input DataGear が Hoare Logic上の Pre Condition(事前条件)となり，
output DataGear が Post Conditionとなる．
各DataGear が Pre / Post Condition を満たしているかの検証は，
各 Condition を Meta DataGear で定義し，
条件を満たしているのかをMeta CodeGear で検証する．

\begin{figure}[H]
  \begin{center}
    \includegraphics[height=2.4cm]{fig/hoare_cg_dg.pdf}
  \end{center}
  \caption{CodeGear，DataGear での Hoare Logic}
  \label{hoare}
\end{figure}