--- a/tex/spec.tex	Tue Sep 15 04:49:26 2020 +0900
+++ b/tex/spec.tex	Tue Sep 15 07:06:29 2020 +0900
@@ -1,15 +1,13 @@
 \section{検証手法}
-現在提案している手法は、Hoare Logic は事前条件がある際、コマンド実行後の事後条件が成り立つ場合に
-コマンドの部分的な正当性を導けることを前述した。
-その為、agdaでのcbcの検証は下図のようになる。
-流れを説明すると、
+本章では検証する際の手法を説明する。
 CodeGear の引数となる DataGear が事前条件となり、
 それを検証する為のPre Conditionを検証する為の Meta Gearsが存在する。
 その後、さらに事後条件となる DetaGear も Meta Gears にて検証する。
+これらを用いて Hoare Logic によりプログラムの検証を行いたい。
 
 \subsection{CbC記法で書くagda}
-CbCプログラムの検証をするに当たり、agdaコードもCbC記法で記述を行う。つまり継続渡しを用いて記述する必要がある。
-以下が例となるコードである。
+CbCプログラムの検証をするに当たり、AgdaコードもCbC記法で記述を行う。つまり継続渡しを用いて記述する必要がある。
+\coderef{agda-cg}が例となるコードである。
 
 \lstinputlisting[caption= Agdaでの CodeGear の例, label=agda-cg]{src/cbc-agda.agda}
 
@@ -18,7 +16,7 @@
 
 \subsection{agda による Meta Gears}
 通常の Meta Gears はノーマルレベルの CodeGear、 DataGear では扱えないメタレベルの計算を扱う単位である。
-今回はその Meta Gears をagdaによる検証の為に用いる。
+今回はその Meta Gears をAgdaによる検証の為に用いる。
 
 \begin{itemize}
     \item Meta DataGear \mbox{}\\
@@ -31,12 +29,3 @@
 		す CodeGear である。故に、Meta CodeGear は Agda で記述した CodeGear の検証そのものである
 \end{itemize}
 
-\subsection{Code Gear の 遷移の検証}
-これまで述べた手法にて、CodeGear の検証をすることができる。
-しかし、CodeGear から 次の CodeGear へ正しく事後条件と事前条件が遷移していることを検証する必要がある。
-% また、各 CodeGear が正しく停止することも重要である。
-
-遷移の検証のために implies という data 型を導入する。
-\lstinputlisting[label=implies, caption=implies] {src/implies.agda}
-これにより CodeGear が正しく遷移できることを検証する。
-