Mercurial > hg > Papers > 2022 > soto-sigos
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}