Mercurial > hg > Papers > 2020 > soto-midterm
comparison tex/spec/spec.tex @ 2:0d85c5be9fb6
fix miss
author | soto@cr.ie.u-ryukyu.ac.jp |
---|---|
date | Tue, 08 Sep 2020 18:43:57 +0900 |
parents | 73127e0ab57c |
children |
comparison
equal
deleted
inserted
replaced
1:73127e0ab57c | 2:0d85c5be9fb6 |
---|---|
1 \section{検証手法} | |
2 手法は模索中であり、先行研究と同じ手法を取ろうとしている。本章では先行研究で述べられている検証手法について説明する。 | |
1 \subsection{CbC記法で書くagda} | 3 \subsection{CbC記法で書くagda} |
2 CbCプログラムの検証をするに当たり、agdaコードもCbC記法で記述を行う。つまり継続渡しを用いて記述する必要がある。 | 4 CbCプログラムの検証をするに当たり、agdaコードもCbC記法で記述を行う。つまり継続渡しを用いて記述する必要がある。 |
3 以下が例となるコードである。 | 5 以下が例となるコードである。 |
4 前述した加算を行うコードと比較すると、不定の型 (t) により継続を行なっている部分が見える。 | 6 前述した加算を行うコードと比較すると、不定の型 (t) により継続を行なっている部分が見える。 |
5 これがAgdaで表現された CodeGear となる。 | 7 これがAgdaで表現された CodeGear となる。 |