# HG changeset patch
# User soto@cr.ie.u-ryukyu.ac.jp
# Date 1600103668 -32400
# Node ID 2652bc4fc17f2924adfd9f20a820a4fb633c05d2
# Parent  27a6616b6683d631832ba5ee555739a7799e8fa2
set src code numbers

diff -r 27a6616b6683 -r 2652bc4fc17f mid_thesis.pdf
Binary file mid_thesis.pdf has changed
diff -r 27a6616b6683 -r 2652bc4fc17f mid_thesis.tex
--- a/mid_thesis.tex	Mon Sep 14 19:58:10 2020 +0900
+++ b/mid_thesis.tex	Tue Sep 15 02:14:28 2020 +0900
@@ -41,10 +41,10 @@
   xrightmargin=0\zw,
   framerule=.3pt,
   columns=[l]{fullflexible},
-  numbers=none,
+  numbers=left,
   stepnumber=1,
   numberstyle={\scriptsize},
-  numbersep=2em,
+%  numbersep=5pt,
   language={},
   tabsize=4,
   lineskip=-0.1\zw,
@@ -52,6 +52,10 @@
 }
 
 \usepackage{indentfirst}
+\usepackage{url}
+\usepackage{amssymb}
+
+\setlength{\columnsep}{10mm}
 
 \begin{document}
 \ltjsetparameter{jacharrange={-3}}
@@ -76,15 +80,20 @@
 	
 % 参考文献	
 \begin{thebibliography}{9}
-\bibitem{1}CbCの論文
-\bibitem{2}外間先輩の先行研究
-\bibitem{3}Hoare Logicの論文
-\bibitem{4}Hoare Logicのスライド
-\bibitem{5}agda のサイト
-\bibitem{6}Aaron Stumpの本
-\bibitem{7}atttonさんの論文
-\bibitem{8}Haskell
-\bibitem{9}Coq
+\bibitem{cbc}cbc-gcc - 並列信頼研 mercurial repository. \\
+	\url{http://www.cr.ie.u-ryukyu.ac.jp/hg/CbC/CbC_gcc/}
+\bibitem{先行研究}外間政尊. Continuation based C での Hoare Logic を用いた仕様記述と検証. Master’s thesis,\\
+	琉球大学 大学院理工学研究科 情報工学専攻, 2020. 
+\bibitem{hoaree}C. A. R. Hoare. An axiomatic basis for computer programming. \\
+	Commun. ACM, Vol. 12, No. 10, p. 576–580, October 1969.
+\bibitem{agda-wiki}The agda wiki.  \\
+	\url{http://wiki.portal.chalmers.se/agda/pmwiki.php}. 2020/09/10.
+\bibitem{agda-doc}Welcome to agda’s documentation!. \\ 
+	\url{http://agda.readthedocs.io/en/latest/}. 2020/09/10.
+\bibitem{agda-book}Aaron Stump. Verified Functional Programming in Agda. 
+	Association for Computing Machinery and Morgan; Claypool, New York, NY, USA, 2016.
+\bibitem{atton}比嘉健太. メタ計算を用いた continuation based c の検証手法. Master’s thesis, \\
+	琉球大学 大学院理工学研究科 情報工学専攻, 2017.
 \end{thebibliography}
 
 \end{multicols*}
diff -r 27a6616b6683 -r 2652bc4fc17f tex/abstract.tex
--- a/tex/abstract.tex	Mon Sep 14 19:58:10 2020 +0900
+++ b/tex/abstract.tex	Tue Sep 15 02:14:28 2020 +0900
@@ -1,14 +1,14 @@
 \renewcommand{\abstractname}{\normalsize 要 旨}
 \begin{abstract}
 	当研究室にて Continuation based C (以下CbC) なるC言語の下位言語に当たる言語を開発している。
-	外間による先行研究にて Floyd-Hoare Logic(以下Hoare Logic)を用いてその検証を行なった。
+	先行研究にて Floyd-Hoare Logic(以下Hoare Logic)を用いてその検証を行なった。
 	本稿では、先行研究にて実施されなかった CbC における赤黒木の検証を Hoare Logic を用いて検証することを目指す。
 \end{abstract}
 
 \renewcommand{\abstractname}{\normalsize Abstract}
 \begin{abstract}
-	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.
+	We are developing a language called Continuation based C (CbC), which is a lower language of the C.
+	In a previous study, Floyd-Hoare Logic (Hoare Logic) was used to validate it.
 	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}