Mercurial > hg > Papers > 2020 > soto-midterm
diff tex/spec.tex @ 3:b124f02ea3f1
post agda code
author | soto@cr.ie.u-ryukyu.ac.jp |
---|---|
date | Wed, 09 Sep 2020 22:07:32 +0900 |
parents | |
children | 35f0e5f12fe6 |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tex/spec.tex Wed Sep 09 22:07:32 2020 +0900 @@ -0,0 +1,33 @@ +\section{検証手法} +手法は模索中であり、先行研究と同じ手法を取ろうとしている。本章では先行研究で述べられている検証手法について説明する。 + +\subsection{CbC記法で書くagda} +CbCプログラムの検証をするに当たり、agdaコードもCbC記法で記述を行う。つまり継続渡しを用いて記述する必要がある。 +以下が例となるコードである。 +前述した加算を行うコードと比較すると、不定の型 (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 として扱う。 + +\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} + +