Mercurial > hg > Papers > 2020 > soto-midterm

comparison tex/spec.tex @ 4:35f0e5f12fe6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add verification method
author soto@cr.ie.u-ryukyu.ac.jp
date Fri, 11 Sep 2020 02:30:15 +0900
parents b124f02ea3f1
children acad18934981
comparison
equal deleted inserted replaced
3:b124f02ea3f1 4:35f0e5f12fe6
1 \section{検証手法} 1 \section{検証手法}
2 手法は模索中であり、先行研究と同じ手法を取ろうとしている。本章では先行研究で述べられている検証手法について説明する。 2 手法は模索中であり、大半が先行研究と同じ手法を考えている。
3 本章では先行研究で述べられている検証手法について説明する。
4 流れとしては、Hoare Logic は事前条件がある際、コマンド実行後の事後条件が成り立つ場合に
5 コマンドの部分的な正当性を導けることを前述した。
6 その為、agdaでのcbcの検証は下図のようになる。
7 流れを説明すると、
8 CodeGear の引数となる DataGear が事前条件となり、
9 それを検証する為のPre Conditionを検証する為の Meta Gearsが存在する。
10 その後、さらに事後条件となる DetaGear も Meta Gears にて検証する。
3 11
4 \subsection{CbC記法で書くagda} 12 \subsection{CbC記法で書くagda}
5 CbCプログラムの検証をするに当たり、agdaコードもCbC記法で記述を行う。つまり継続渡しを用いて記述する必要がある。 13 CbCプログラムの検証をするに当たり、agdaコードもCbC記法で記述を行う。つまり継続渡しを用いて記述する必要がある。
6 以下が例となるコードである。 14 以下が例となるコードである。
15
16 \lstinputlisting[caption= Agdaでの CodeGear の例, label=agda-cg]{src/cbc-agda.agda}
17
7 前述した加算を行うコードと比較すると、不定の型 (t) により継続を行なっている部分が見える。 18 前述した加算を行うコードと比較すると、不定の型 (t) により継続を行なっている部分が見える。
8 これがAgdaで表現された CodeGear となる。 19 これがAgdaで表現された CodeGear となる。
9 20
10 \subsection{agda による Meta Gears} 21 \subsection{agda による Meta Gears}
11 通常の Meta Gears はノーマルレベルの CodeGear、 DataGear では扱えないメタレベルの計算を扱う単位である。 22 通常の Meta Gears はノーマルレベルの CodeGear、 DataGear では扱えないメタレベルの計算を扱う単位である。
12 Meta DataGear はメタ計算で使われる DataGear で、実行するメタ計算によって異なる。
13 今回はその Meta Gears をagdaによる検証の為に用いる。 23 今回はその Meta Gears をagdaによる検証の為に用いる。
14 検証での Meta Gears は DataGear が持つ同値関係や、
15 大小関係などの関係を表す DataGear がそれに当たると考えられる。
16 24
17 \subsection{agda における Meta DataGear} 25 \begin{itemize}
18 Agda 上で Meta DataGear を持つことでデータ構造自体が関係を持つデータを作ることができる。 26 \item Meta DataGear
19 以下が While Program での制約条件をまとめたものになる。 27 \begin{itemize}
20 \lstinputlisting[label=agda-mdg, caption= Agda における Meta DataGear] {./src/agda-mdg.agda} 28 \item
21 whileTestState で Meta DataGear を識別するためのデータを分け、 29 Agda 上で Meta DataGear を持つことでデータ構造自体が関係を持つデータを作ることができる。
22 whileTestStatePでそれぞれの Meta DataGear を返している。 30 これを用いることで、仕様となる制約条件を記述することができる。
23 ここでは = の後ろの (vari env ≡ 0) (varn env ≡c10 env)/ などのデータを Meta DataGear として扱う。 31 \end{itemize}
32 \item Meta CodeGear
33 \begin{itemize}
34 \item
35 Meta CodeGear は 通常の CodeGear では扱えないメタレベルの計算を扱う CodeGear
36 である。Agda での Meta CodeGear は Meta DataGear を引数に取りそれらの関係を返
37 す CodeGear である。故に、Meta CodeGear は Agda で記述した CodeGear の検証そのものである
38 \end{itemize}
39 \end{itemize}
24 40
25 \subsection{agda における Meta CodeGear} 41 \subsection{Code Gear の 遷移の検証}
26 Meta CodeGear は 通常の CodeGear では扱えないメタレベルの計算を扱う CodeGear 42 これまで述べた手法にて、CodeGear の検証をすることができる。
27 である。Agda での Meta CodeGear は Meta DataGear を引数に取りそれらの関係を返 43 しかし、CodeGear から 次の CodeGear へ正しく事後条件と事前条件が遷移していることを検証する必要がある。
28 す CodeGear である。 44 % また、各 CodeGear が正しく停止することも重要である。
29 メタ計算で検証を行う際の Meta CodeGear は Agda で記述した CodeGear の検証その
30 ものである。例として ソースコード 5.3 を示す。
31 \lstinputlisting[label=agda-mcg, caption= Agda における Meta CodeGear] {./src/agda-mcg.agda}
32 45
46 遷移の検証のために implies という data 型を導入する。
47 \lstinputlisting[label=implies, caption=implies] {src/implies.agda}
48 これにより CodeGear が正しく遷移できることを検証する。
33 49