Mercurial > hg > Papers > 2022 > soto-sigos

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

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
DONE 一度これで提出
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Thu, 05 May 2022 22:32:45 +0900
parents 14a0e409d574
children
comparison
equal deleted inserted replaced
5:6c0b1fcbac2d 6:9ec2d2ac1309
1 \section{検証手法} 1 \section{検証手法}
2 本章では検証する際の手法を説明する。 2 本章では検証する際の手法を説明する．
3 CodeGear の引数となる DataGear が事前条件となり、 3 CodeGear の引数となる DataGear が事前条件となり，
4 それを検証する為のPre Conditionを検証する為の Meta Gearsが存在する。 4 それを検証する為のPre Conditionを検証する為の Meta Gearsが存在する．
5 その後、さらに事後条件となる DetaGear も Meta Gears にて検証する。 5 その後，さらに事後条件となる DetaGear も Meta Gears にて検証する．
6 これらを用いて Hoare Logic によりプログラムの検証を行いたい。 6 これらを用いて Hoare Logic によりプログラムの検証を行いたい．
7 7
8 \subsection{CbC記法で書くagda} 8 \subsection{CbC記法で書くagda}
9 CbCプログラムの検証をするに当たり、AgdaコードもCbC記法で記述を行う。つまり継続渡しを用いて記述する必要がある。 9 CbCプログラムの検証をするに当たり，AgdaコードもCbC記法で記述を行う．つまり継続渡しを用いて記述する必要がある．
10 \coderef{agda-cg}が例となるコードである。 10 \coderef{agda-cg}が例となるコードである．
11 11
12 \lstinputlisting[caption= Agdaでの CodeGear の例, label=agda-cg]{src/cbc-agda.agda} 12 \lstinputlisting[caption= Agdaでの CodeGear の例, label=agda-cg]{src/cbc-agda.agda}
13 13
14 前述した加算を行うコードと比較すると、不定の型 (t) により継続を行なっている部分が見える。 14 前述した加算を行うコードと比較すると，不定の型 (t) により継続を行なっている部分が見える．
15 これがAgdaで表現された CodeGear となる。 15 これがAgdaで表現された CodeGear となる．
16 16
17 \subsection{agda による Meta Gears} 17 \subsection{agda による Meta Gears}
18 通常の Meta Gears はノーマルレベルの CodeGear、 DataGear では扱えないメタレベルの計算を扱う単位である。 18 通常の Meta Gears はノーマルレベルの CodeGear， DataGear では扱えないメタレベルの計算を扱う単位である．
19 今回はその Meta Gears をAgdaによる検証の為に用いる。 19 今回はその Meta Gears をAgdaによる検証の為に用いる．
20 20
21 \begin{itemize} 21 \begin{itemize}
22 \item Meta DataGear \mbox{}\\ 22 \item Meta DataGear \mbox{}\\
23 Agda 上で Meta DataGear を持つことでデータ構造自体が関係を持つデータを作ることができる。 23 Agda 上で Meta DataGear を持つことでデータ構造自体が関係を持つデータを作ることができる．
24 これを用いることで、仕様となる制約条件を記述することができる。 24 これを用いることで，仕様となる制約条件を記述することができる．
25 25
26 \item Meta CodeGear\mbox{}\\ 26 \item Meta CodeGear\mbox{}\\
27 Meta CodeGear は 通常の CodeGear では扱えないメタレベルの計算を扱う CodeGear 27 Meta CodeGear は 通常の CodeGear では扱えないメタレベルの計算を扱う CodeGear
28 である。Agda での Meta CodeGear は Meta DataGear を引数に取りそれらの関係を返 28 である．Agda での Meta CodeGear は Meta DataGear を引数に取りそれらの関係を返
29 す CodeGear である。故に、Meta CodeGear は Agda で記述した CodeGear の検証そのものである 29 す CodeGear である．故に，Meta CodeGear は Agda で記述した CodeGear の検証そのものである
30 \end{itemize} 30 \end{itemize}
31 31