Mercurial > hg > Papers > 2020 > soto-midterm

comparison tex/spec.tex @ 7:acad18934981

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add description of rbtree
author soto@cr.ie.u-ryukyu.ac.jp
date Mon, 14 Sep 2020 05:41:23 +0900
parents 35f0e5f12fe6
children 27a6616b6683
comparison
equal deleted inserted replaced
6:4bf00f7ba825 7:acad18934981
21 \subsection{agda による Meta Gears} 21 \subsection{agda による Meta Gears}
22 通常の Meta Gears はノーマルレベルの CodeGear、 DataGear では扱えないメタレベルの計算を扱う単位である。 22 通常の Meta Gears はノーマルレベルの CodeGear、 DataGear では扱えないメタレベルの計算を扱う単位である。
23 今回はその Meta Gears をagdaによる検証の為に用いる。 23 今回はその Meta Gears をagdaによる検証の為に用いる。
24 24
25 \begin{itemize} 25 \begin{itemize}
26 \item Meta DataGear 26 \item Meta DataGear \mbox{}\\
27 \begin{itemize} 27 Agda 上で Meta DataGear を持つことでデータ構造自体が関係を持つデータを作ることができる。
28 \item 28 これを用いることで、仕様となる制約条件を記述することができる。
29 Agda 上で Meta DataGear を持つことでデータ構造自体が関係を持つデータを作ることができる。 29
30 これを用いることで、仕様となる制約条件を記述することができる。 30 \item Meta CodeGear\mbox{}\\
31 \end{itemize} 31 Meta CodeGear は 通常の CodeGear では扱えないメタレベルの計算を扱う CodeGear
32 \item Meta CodeGear 32 である。Agda での Meta CodeGear は Meta DataGear を引数に取りそれらの関係を返
33 \begin{itemize} 33 す CodeGear である。故に、Meta CodeGear は Agda で記述した CodeGear の検証そのものである
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} 34 \end{itemize}
40 35
41 \subsection{Code Gear の 遷移の検証} 36 \subsection{Code Gear の 遷移の検証}
42 これまで述べた手法にて、CodeGear の検証をすることができる。 37 これまで述べた手法にて、CodeGear の検証をすることができる。
43 しかし、CodeGear から 次の CodeGear へ正しく事後条件と事前条件が遷移していることを検証する必要がある。 38 しかし、CodeGear から 次の CodeGear へ正しく事後条件と事前条件が遷移していることを検証する必要がある。