diff Paper/tex/spec.tex @ 6:9ec2d2ac1309

DONE 一度これで提出
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Thu, 05 May 2022 22:32:45 +0900 (2022-05-05)
parents 14a0e409d574
children
line wrap: on
line diff
--- a/Paper/tex/spec.tex	Thu May 05 17:38:06 2022 +0900
+++ b/Paper/tex/spec.tex	Thu May 05 22:32:45 2022 +0900
@@ -1,31 +1,31 @@
 \section{検証手法}
-本章では検証する際の手法を説明する。
-CodeGear の引数となる DataGear が事前条件となり、
-それを検証する為のPre Conditionを検証する為の Meta Gearsが存在する。
-その後、さらに事後条件となる DetaGear も Meta Gears にて検証する。
-これらを用いて Hoare Logic によりプログラムの検証を行いたい。
+本章では検証する際の手法を説明する.
+CodeGear の引数となる DataGear が事前条件となり,
+それを検証する為のPre Conditionを検証する為の Meta Gearsが存在する.
+その後,さらに事後条件となる DetaGear も Meta Gears にて検証する.
+これらを用いて Hoare Logic によりプログラムの検証を行いたい.
 
 \subsection{CbC記法で書くagda}
-CbCプログラムの検証をするに当たり、AgdaコードもCbC記法で記述を行う。つまり継続渡しを用いて記述する必要がある。
-\coderef{agda-cg}が例となるコードである。
+CbCプログラムの検証をするに当たり,AgdaコードもCbC記法で記述を行う.つまり継続渡しを用いて記述する必要がある.
+\coderef{agda-cg}が例となるコードである.
 
 \lstinputlisting[caption= Agdaでの CodeGear の例, label=agda-cg]{src/cbc-agda.agda}
 
-前述した加算を行うコードと比較すると、不定の型 (t) により継続を行なっている部分が見える。
-これがAgdaで表現された CodeGear となる。
+前述した加算を行うコードと比較すると,不定の型 (t) により継続を行なっている部分が見える.
+これがAgdaで表現された CodeGear となる.
 
 \subsection{agda による Meta Gears}
-通常の Meta Gears はノーマルレベルの CodeGear、 DataGear では扱えないメタレベルの計算を扱う単位である。
-今回はその Meta Gears をAgdaによる検証の為に用いる。
+通常の Meta Gears はノーマルレベルの CodeGear, DataGear では扱えないメタレベルの計算を扱う単位である.
+今回はその Meta Gears をAgdaによる検証の為に用いる.
 
 \begin{itemize}
     \item Meta DataGear \mbox{}\\
-		Agda 上で Meta DataGear を持つことでデータ構造自体が関係を持つデータを作ることができる。
-		これを用いることで、仕様となる制約条件を記述することができる。
+		Agda 上で Meta DataGear を持つことでデータ構造自体が関係を持つデータを作ることができる.
+		これを用いることで,仕様となる制約条件を記述することができる.
 
 	\item Meta CodeGear\mbox{}\\
 		Meta CodeGear は 通常の CodeGear では扱えないメタレベルの計算を扱う CodeGear
-		である。Agda での Meta CodeGear は Meta DataGear を引数に取りそれらの関係を返
-		す CodeGear である。故に、Meta CodeGear は Agda で記述した CodeGear の検証そのものである
+		である.Agda での Meta CodeGear は Meta DataGear を引数に取りそれらの関係を返
+		す CodeGear である.故に,Meta CodeGear は Agda で記述した CodeGear の検証そのものである
 \end{itemize}