# HG changeset patch
# User soto@cr.ie.u-ryukyu.ac.jp
# Date 1599759015 -32400
# Node ID 35f0e5f12fe6472e23ded228453608af784b66c3
# Parent  b124f02ea3f1fec714e63e79b8b462f3fcbe6fc6
add verification method

diff -r b124f02ea3f1 -r 35f0e5f12fe6 mid_thesis.pdf
Binary file mid_thesis.pdf has changed
diff -r b124f02ea3f1 -r 35f0e5f12fe6 mid_thesis.tex
--- a/mid_thesis.tex	Wed Sep 09 22:07:32 2020 +0900
+++ b/mid_thesis.tex	Fri Sep 11 02:30:15 2020 +0900
@@ -72,10 +72,6 @@
 
 \section{今後の課題}
 
-\section{類似技術}
-
-\subsection{coq}
-
 % 参考文献
 \begin{thebibliography}{9}
 
diff -r b124f02ea3f1 -r 35f0e5f12fe6 tex/agda.tex
--- a/tex/agda.tex	Wed Sep 09 22:07:32 2020 +0900
+++ b/tex/agda.tex	Fri Sep 11 02:30:15 2020 +0900
@@ -1,2 +1,17 @@
-\section{agda}
-    agdaとは、Agda は依存型をもつ純粋関数型の言語である。 定理証明支援器でもある。
+\section{Agda}
+Agda とは定理証明支援器であり、関数型言語である。Agda は依存型という型システ
+ムを持ち、型を第一級オブジェクトとして扱うことが可能である。また、型システムは
+Curry-Howard 同型対応により命題と型付きラムダ計算が一対一で対応するため Agda で
+は記述したプログラムを証明することができる。
+
+%\subsection{Record 型}
+
+%\subsection{Data 型}
+
+%\subsection{Agdaの基本操作}
+
+%\subsection{定理証明支援器としての Agda}
+
+%\subsectoin{}
+
+
diff -r b124f02ea3f1 -r 35f0e5f12fe6 tex/spec.tex
--- a/tex/spec.tex	Wed Sep 09 22:07:32 2020 +0900
+++ b/tex/spec.tex	Fri Sep 11 02:30:15 2020 +0900
@@ -1,33 +1,49 @@
 \section{検証手法}
-手法は模索中であり、先行研究と同じ手法を取ろうとしている。本章では先行研究で述べられている検証手法について説明する。
+手法は模索中であり、大半が先行研究と同じ手法を考えている。
+本章では先行研究で述べられている検証手法について説明する。
+流れとしては、Hoare Logic は事前条件がある際、コマンド実行後の事後条件が成り立つ場合に
+コマンドの部分的な正当性を導けることを前述した。
+その為、agdaでのcbcの検証は下図のようになる。
+流れを説明すると、
+CodeGear の引数となる DataGear が事前条件となり、
+それを検証する為のPre Conditionを検証する為の Meta Gearsが存在する。
+その後、さらに事後条件となる DetaGear も Meta Gears にて検証する。
 
 \subsection{CbC記法で書くagda}
 CbCプログラムの検証をするに当たり、agdaコードもCbC記法で記述を行う。つまり継続渡しを用いて記述する必要がある。
 以下が例となるコードである。
+
+\lstinputlisting[caption= Agdaでの CodeGear の例, label=agda-cg]{src/cbc-agda.agda}
+
 前述した加算を行うコードと比較すると、不定の型 (t) により継続を行なっている部分が見える。
 これがAgdaで表現された CodeGear となる。
 
 \subsection{agda による Meta Gears}
 通常の Meta Gears はノーマルレベルの CodeGear、 DataGear では扱えないメタレベルの計算を扱う単位である。
-Meta DataGear はメタ計算で使われる DataGear で、実行するメタ計算によって異なる。
 今回はその Meta Gears をagdaによる検証の為に用いる。
-検証での Meta Gears は DataGear が持つ同値関係や、
-大小関係などの関係を表す DataGear がそれに当たると考えられる。
 
-\subsection{agda における Meta DataGear}
-Agda 上で Meta DataGear を持つことでデータ構造自体が関係を持つデータを作ることができる。
-以下が While Program での制約条件をまとめたものになる。
-\lstinputlisting[label=agda-mdg, caption= Agda における Meta DataGear] {./src/agda-mdg.agda}
-whileTestState で Meta DataGear を識別するためのデータを分け、
-whileTestStatePでそれぞれの Meta DataGear を返している。
-ここでは = の後ろの (vari env ≡ 0) (varn env ≡c10 env)/ などのデータを Meta DataGear として扱う。
+\begin{itemize}
+  \item Meta DataGear
+  \begin{itemize}
+    \item
+    Agda 上で Meta DataGear を持つことでデータ構造自体が関係を持つデータを作ることができる。
+    これを用いることで、仕様となる制約条件を記述することができる。
+  \end{itemize}
+  \item Meta CodeGear
+  \begin{itemize}
+    \item
+    Meta CodeGear は 通常の CodeGear では扱えないメタレベルの計算を扱う CodeGear
+    である。Agda での Meta CodeGear は Meta DataGear を引数に取りそれらの関係を返
+    す CodeGear である。故に、Meta CodeGear は Agda で記述した CodeGear の検証そのものである
+  \end{itemize}
+\end{itemize}
 
-\subsection{agda における Meta CodeGear}
-Meta CodeGear は 通常の CodeGear では扱えないメタレベルの計算を扱う CodeGear
-である。Agda での Meta CodeGear は Meta DataGear を引数に取りそれらの関係を返
-す CodeGear である。
-メタ計算で検証を行う際の Meta CodeGear は Agda で記述した CodeGear の検証その
-ものである。例として ソースコード 5.3 を示す。
-\lstinputlisting[label=agda-mcg, caption= Agda における Meta CodeGear] {./src/agda-mcg.agda}
+\subsection{Code Gear の 遷移の検証}
+これまで述べた手法にて、CodeGear の検証をすることができる。
+しかし、CodeGear から 次の CodeGear へ正しく事後条件と事前条件が遷移していることを検証する必要がある。
+% また、各 CodeGear が正しく停止することも重要である。
 
+遷移の検証のために implies という data 型を導入する。
+\lstinputlisting[label=implies, caption=implies] {src/implies.agda}
+これにより CodeGear が正しく遷移できることを検証する。