--- a/Makefile	Tue Sep 08 18:43:57 2020 +0900
+++ b/Makefile	Wed Sep 09 22:07:32 2020 +0900
@@ -2,32 +2,29 @@
 
 TARGET=mid_thesis
 
-LATEX=platex
+LATEX=lualatex
 BIBTEX=pbibtex
-DVIPDF=dvipdfmx -p a4
 #You need setting "-l" option if You think You get a landscape PDF
 #DVIPDF_OPT=-l
 
 #Embed fonts
 #DVIPDF_OPT=-f hiraginoEmbed.map
 
-.SUFFIXES: .tex .dvi .pdf
+.SUFFIXES: .tex .pdf
 
-.tex.dvi:
+.tex:
 	$(LATEX) $<
 	#$(BIBTEX) $(TARGET)
 	$(LATEX) $<
 	$(LATEX) $<
 
-.dvi.pdf:
+.pdf:
 	$(DVIPDF) $(DVIPDF_OPT) $<
 
 
 all: $(TARGET).pdf
 	open $(TARGET).pdf
 
-dvi: $(TARGET).dvi
-
 pdf: $(TARGET).pdf
 
 

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/make.sh	Wed Sep 09 22:07:32 2020 +0900
@@ -0,0 +1,2 @@
+lualatex mid_thesis.tex && open mid_thesis.pdf
+make clean

Binary file mid_thesis.pdf has changed

--- a/mid_thesis.tex	Tue Sep 08 18:43:57 2020 +0900
+++ b/mid_thesis.tex	Wed Sep 09 22:07:32 2020 +0900
@@ -1,11 +1,11 @@
-\documentclass[a4j,9.5pt]{jarticle}
-% \usepackage[dvips]{graphicx}
+\documentclass[a4j,9.5pt]{article}
+\usepackage{graphicx}
 \usepackage{picins}
 \usepackage{fancyhdr}
 \usepackage[]{multicol}
-\usepackage{listings,jlisting}
+\usepackage{listings}
 %\pagestyle{fancy}
-\lhead{\parpic{\includegraphics[height=1zw,keepaspectratio,bb=0 0 251 246]{pic/emblem-bitmap.pdf}}琉球大学主催 工学部工学科知能情報コース 中間発表予稿}
+\lhead{\parpic{\includegraphics[height=1\zw,keepaspectratio,bb=0 0 251 246]{pic/emblem-bitmap.pdf}}琉球大学主催 工学部工学科知能情報コース 中間発表予稿}
 \rhead{}
 \cfoot{}
 
@@ -18,14 +18,14 @@
 \setlength{\textheight}{261mm}
 \setlength{\footskip}{0mm}
 \pagestyle{empty}
-
-
-\usepackage{ascmac}
-\usepackage[dvipdfmx]{graphicx}
-\usepackage{amssymb}
-\usepackage{type1cm}
-\usepackage[usenames]{color}
-\usepackage{ulem}
+\usepackage[top=2cm, bottom=2cm, left=1cm, right=1cm]{geometry}
+% 特殊文字の表示に必要
+\usepackage{luatexja}
+\usepackage{fontspec}
+\setmainfont{STIX Math}%
+\setmonofont{STIXGeneralBol}[
+	Scale=MatchLowercase
+]
 
 \renewcommand{\abstractname}{要 旨}
 \lstset{
@@ -37,8 +37,8 @@
   keywordstyle={\ttfamily},
   basicstyle={\small\ttfamily},
   breaklines=true,
-  xleftmargin=0zw,
-  xrightmargin=0zw,
+  xleftmargin=0\zw,
+  xrightmargin=0\zw,
   framerule=.3pt,
   columns=[l]{fullflexible},
   numbers=none,
@@ -47,97 +47,36 @@
   numbersep=2em,
   language={},
   tabsize=4,
-  lineskip=-0.1zw,
+  lineskip=-0.1\zw,
   escapechar={@},
 }
 
 \begin{document}
-\title{Continuation based C での Hoare Logic を用いた赤黒木の検証 \\ Validation of red-black tree implemented in Continuation based C using Hoare Logic}
+\ltjsetparameter{jacharrange={-3}}
+\title{Continuation based C による赤黒木の Hoare Logic を用いた検証 \\ Verification of red-black tree implemented in Continuation based C using Hoare Logic}
 \author{学籍番号 175706H 氏名 上地 悠斗 \\ 指導教員 : 河野 真治}
 \date{}
 \maketitle
 \thispagestyle{fancy}
 
 % 要旨
-\input{./tex/abstract/abstract.tex}
-
-\begin{multicols}{2}
-\input{./tex/intro/intro.tex}
-
-\section{Continuation based C}
-	前述した通り CbC とはC言語からループ制御構造とサブルーチンコールを取り除き、
-	継続を導入したC言語の下位言語である。継続呼び出しは引数付き goto 文で表現される。
-	また、CodeGear を処理の単位、DataGear をデータの単位として記述するプログラミング言語である。
-	CbC のプログラミングでは DataGear を CodeGear で変更し、その変更を次の CodeGear に渡して処理を行う。
-
-\subsection{Code Gear / Data Gear}
-	CbCでは、検証しやすいプログラムの単位として DataGear と CodeGear という単位を用いるプログラミングスタイルを提案している。
-
-	CodeGear はプログラムの処理そのものであり、一般的なプログラム言語における関数と同じ役割である。
-	DataGear は CodeGear で扱うデータの単位であり、処理に必要なデータである。
-	CodeGear の入力となる DataGear を Input DataGear と呼び、出力は Output DataGear と呼ぶ。
-	
-	CodeGear 間の移動は継続を用いて行われる。
-	継続は関数呼び出しとは異なり、呼び出した後に元のコードに戻らず、次の CodeGear へ継続を行う。
-	これは、関数型プログラミングでは末尾関数呼び出しを行うことに相当する。
-
-
-\subsection{Meta Code Gear / Meta Data Gear}
-	プログラムの記述する際は、ノーマルレベルの計算の他に、メモリ管理、スレッド管理、
-	資源管理等を記述しなければならない処理が存在する。
-	これらの計算はノーマルレベルの計算と区別してメタ計算と呼ぶ。
-
-	メタ計算は OS の機能を通して処理することが多く、信頼性の高い記述が求められる。
-	そのため、 CbC ではメタ計算を分離するために Meta CodeGear、 Meta DataGear を定義している。
-
-	Meta CodeGear は CbC 上でのメタ計算で、通常の CodeGear を実行する際に必要なメタ計算を分離するための単位である。
-	CodeGear を実行する前後やDataGear の大枠として Meta Gear が存在している。
-
-	例として CodeGear が DataGear から値を取得する際に使われる、 stub CodeGear について説明する。
+\input{./tex/abstract.tex}
 
-	CbC では CodeGear を実行する際、ノーマルレベルの計算からは見えないが
-	必要な DataGear を Context と呼ばれる Meta DataGear を通して取得することになる。
-	これはユーザーが直接データを扱える状態では信頼性が高いとは言えないと考えるからである。
-	そのために、 Meta CodeGear として Context から必要な DataGear を取り出し、
-	CodeGear に接続する stub CodeGear という Meta CodeGear を定義している。
-
-	Meta DataGear は CbC 上のメタ計算で扱われる DataGear である。例えば stub
-	CodeGear では Context と呼ばれる接続可能な CodeGear、DataGear のリストや、DataGear
-	のメモリ空間等を持った Meta DataGear を扱っている。
-
-
-\section{Hoare Logic}
-	Hoare Logic とは C.A.R Hoare、 R.W Floyd が考案したプログラムの検証の手法である。
-	これは、「プログラムの事前条件(P)が成立しているとき、コマンド(C)実行して停止すると事後条件(Q)が成り立つ」
-	というもので、CbCの実行を継続するという性質に非常に相性が良い。
-	Hoare Logic を表記すると以下のようになる。
-	$$ \{P\}\ C\ \{Q\} $$
-	この3つ組は Hoare Triple と呼ばれる。
-
-	Hoare Triple の事後条件を受け取り異なる条件を返す別の Hoare Triple を繋げることでプログラムを記述していく。
-
-	Hoare Logic の検証では、「条件がすべて正しく接続されている」かつ「コマンドが停止する」ことが必要である。
-	これらを満たし、事前条件から事後条件を導けることを検証することで Hoare Logic の健全性を示すことができる。
-
-\section{agda}
-	agdaとは、Agda は依存型をもつ純粋関数型の言語である。 定理証明支援器でもある。
-
-\section{関連研究}
-	外間による研究では CbC にて実装された While Loop を Hoare Logic を用いて検証した。
-
-\section{検証手法}
-    手法は模索中であり、先行研究と同じ手法を取ろうとしている。本章では先行研究で述べられている検証手法について説明する。
-
-% 手法
-\input{./tex/spec/spec.tex}
+% 2段組開始
+\begin{multicols}{2}
+	\input{./tex/intro.tex} % 研究目的
+	\input{./tex/cbc.tex} % CbC の説明
+	\input{./tex/hoare.tex} % Hoare Logic の説明
+	\input{./tex/agda.tex} % agda の説明
+    \input{./tex/spec.tex}% 手法
 
 \section{今後の課題}
-    d
 
 \section{類似技術}
 
 \subsection{coq}
 
+% 参考文献
 \begin{thebibliography}{9}
 
 \bibitem{1}CbCの論文
@@ -149,8 +88,8 @@
 \bibitem{7}atttonさんの論文
 \bibitem{8}Haskell
 \bibitem{9}Coq
+\end{thebibliography}
 
-\end{thebibliography}
 \end{multicols}
 
 \end{document}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tex/abstract.tex	Wed Sep 09 22:07:32 2020 +0900
@@ -0,0 +1,9 @@
+\begin{abstract}
+	当研究室にて Continuation based C (以下CbC) なるC言語の下位言語に当たる言語を開発している。
+	外間による先行研究にて Floyd-Hoare Logic(以下Hoare Logic)を用いてその検証を行なった。
+	本稿では、先行研究にて実施されなかった CbC における赤黒木の検証を Hoare Logic を用いて検証することを目指す。
+	\\ \\
+	We are developing a language called Continuation based C (CbC), which is a Subordinate language of the C.
+	M.Eng Hokama verified it by using Floyd-Hoare Logic (Hoare Logic) in a previous study.
+	In this paper, we aim to use Hoare Logic to validate the red-black tree in CbC, which was not performed in previous studies.
+\end{abstract}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tex/agda.tex	Wed Sep 09 22:07:32 2020 +0900
@@ -0,0 +1,2 @@
+\section{agda}
+    agdaとは、Agda は依存型をもつ純粋関数型の言語である。 定理証明支援器でもある。

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tex/cbc.tex	Wed Sep 09 22:07:32 2020 +0900
@@ -0,0 +1,42 @@
+\section{Continuation based C}
+	前述した通り CbC とはC言語からループ制御構造とサブルーチンコールを取り除き、
+	継続を導入したC言語の下位言語である。継続呼び出しは引数付き goto 文で表現される。
+	また、CodeGear を処理の単位、DataGear をデータの単位として記述するプログラミング言語である。
+	CbC のプログラミングでは DataGear を CodeGear で変更し、その変更を次の CodeGear に渡して処理を行う。
+
+\subsection{Code Gear / Data Gear}
+	CbCでは、検証しやすいプログラムの単位として DataGear と CodeGear という単位を用いるプログラミングスタイルを提案している。
+
+	CodeGear はプログラムの処理そのものであり、一般的なプログラム言語における関数と同じ役割である。
+	DataGear は CodeGear で扱うデータの単位であり、処理に必要なデータである。
+	CodeGear の入力となる DataGear を Input DataGear と呼び、出力は Output DataGear と呼ぶ。
+	
+	CodeGear 間の移動は継続を用いて行われる。
+	継続は関数呼び出しとは異なり、呼び出した後に元のコードに戻らず、次の CodeGear へ継続を行う。
+	これは、関数型プログラミングでは末尾関数呼び出しを行うことに相当する。
+
+
+\subsection{Meta Code Gear / Meta Data Gear}
+	プログラムの記述する際は、ノーマルレベルの計算の他に、メモリ管理、スレッド管理、
+	資源管理等を記述しなければならない処理が存在する。
+	これらの計算はノーマルレベルの計算と区別してメタ計算と呼ぶ。
+
+	メタ計算は OS の機能を通して処理することが多く、信頼性の高い記述が求められる。
+	そのため、 CbC ではメタ計算を分離するために Meta CodeGear、 Meta DataGear を定義している。
+
+	Meta CodeGear は CbC 上でのメタ計算で、通常の CodeGear を実行する際に必要なメタ計算を分離するための単位である。
+	CodeGear を実行する前後やDataGear の大枠として Meta Gear が存在している。
+
+	例として CodeGear が DataGear から値を取得する際に使われる、 stub CodeGear について説明する。
+
+	CbC では CodeGear を実行する際、ノーマルレベルの計算からは見えないが
+	必要な DataGear を Context と呼ばれる Meta DataGear を通して取得することになる。
+	これはユーザーが直接データを扱える状態では信頼性が高いとは言えないと考えるからである。
+	そのために、 Meta CodeGear として Context から必要な DataGear を取り出し、
+	CodeGear に接続する stub CodeGear という Meta CodeGear を定義している。
+
+	Meta DataGear は CbC 上のメタ計算で扱われる DataGear である。例えば stub
+	CodeGear では Context と呼ばれる接続可能な CodeGear、DataGear のリストや、DataGear
+	のメモリ空間等を持った Meta DataGear を扱っている。
+
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tex/hoare.tex	Wed Sep 09 22:07:32 2020 +0900
@@ -0,0 +1,13 @@
+\section{Hoare Logic}
+	Hoare Logic とは C.A.R Hoare、 R.W Floyd が考案したプログラムの検証の手法である。
+	これは、「プログラムの事前条件(P)が成立しているとき、コマンド(C)実行して停止すると事後条件(Q)が成り立つ」
+	というもので、CbCの実行を継続するという性質に非常に相性が良い。
+	Hoare Logic を表記すると以下のようになる。
+    {P} C {Q}
+	この3つ組は Hoare Triple と呼ばれる。
+
+	Hoare Triple の事後条件を受け取り異なる条件を返す別の Hoare Triple を繋げることでプログラムを記述していく。
+
+	Hoare Logic の検証では、「条件がすべて正しく接続されている」かつ「コマンドが停止する」ことが必要である。
+	これらを満たし、事前条件から事後条件を導けることを検証することで Hoare Logic の健全性を示すことができる。
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tex/intro.tex	Wed Sep 09 22:07:32 2020 +0900
@@ -0,0 +1,15 @@
+\section{研究目的}
+	OS やアプリケーションの信頼性を高めることは重要な課題である。
+	信頼性を高める為には仕様を満たしたプログラムが実装されていることを検証する必要がある。
+	具体的には「モデル検査」や「定理証明」などが検証手法として挙げられる。
+
+	研究室で CbC という言語を開発している。
+	CbC とは、C言語からループ制御構造とサブルーチンコールを取り除き、継続を導入した C言語の下位言語である。
+	この言語の信用性を検証したい。
+	
+	仕様に合った実装を実施していることの検証手法として Hoare Logic が知られている。
+	Hoare Logic は事前条件が成り立っているときにある計算(以下コマンド)を実行した後に、
+	に事後条件が成り立つことでコマンドの検証を行う。
+	
+	CbC の実行を継続するという性質が Hoare Logic の事前条件と事後条件の定義から検証を行うことと非常に相性が良い。
+	これらのことから、本稿では Hoare Logic を用いて CbC を検証することを目指す。

--- /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}
+
+