Mercurial > hg > Papers > 2021 > soto-thesis

comparison paper/tex/hoare.tex @ 11:1cde48f23236

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
FIN proto
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Mon, 15 Feb 2021 03:51:35 +0900
parents bf1f62556b81
children
comparison
equal deleted inserted replaced
10:2ba2fa18fc7e 11:1cde48f23236
32 \end{center} 32 \end{center}
33 \caption{CodeGear、DataGear での Hoare Logic} 33 \caption{CodeGear、DataGear での Hoare Logic}
34 \label{hoare} 34 \label{hoare}
35 \end{figure} 35 \end{figure}
36 36
37 \begin{comment}
37 \section{CbCでの Hoare Logic を用いた検証} 38 \section{CbCでの Hoare Logic を用いた検証}
38 先行研究で行われている While Loop の Hoare Logic での検証を元に、 39 先行研究で行われている While Loop の Hoare Logic での検証を元に、
39 実際の Hoare Logic を用いた検証手法について解説する。 40 実際の Hoare Logic を用いた検証手法について解説する。
40 41
41 \subsection{CbC でのコードとそれに対応したAgdaのコード} 42 \subsection{CbC でのコードとそれに対応したAgdaのコード}
49 そのため Env → t の間に Meta Data Gear を記述する 50 そのため Env → t の間に Meta Data Gear を記述する
50 以下は Meta Data Gear の記述 51 以下は Meta Data Gear の記述
51 % Meta Data Gearのソースコードを貼る 52 % Meta Data Gearのソースコードを貼る
52 53
53 s1 が初期状態、 54 s1 が初期状態、
55 \end{comment}
54 56
55 57