# HG changeset patch
# User soto@cr.ie.u-ryukyu.ac.jp
# Date 1600112966 -32400
# Node ID c162ca9b997e9462f85163d4f8270124acadd42a
# Parent  2652bc4fc17f2924adfd9f20a820a4fb633c05d2
add reference

diff -r 2652bc4fc17f -r c162ca9b997e make.sh
--- a/make.sh	Tue Sep 15 02:14:28 2020 +0900
+++ b/make.sh	Tue Sep 15 04:49:26 2020 +0900
@@ -1,2 +1,2 @@
-lualatex mid_thesis.tex && open mid_thesis.pdf
+lualatex mid_thesis && biber mid_thesis &&  lualatex mid_thesis && lualatex mid_thesis && open mid_thesis
 make clean
diff -r 2652bc4fc17f -r c162ca9b997e mid_thesis.pdf
Binary file mid_thesis.pdf has changed
diff -r 2652bc4fc17f -r c162ca9b997e mid_thesis.tex
--- a/mid_thesis.tex	Tue Sep 15 02:14:28 2020 +0900
+++ b/mid_thesis.tex	Tue Sep 15 04:49:26 2020 +0900
@@ -35,7 +35,7 @@
   commentstyle={\ttfamily},
   identifierstyle={\ttfamily},
   keywordstyle={\ttfamily},
-  basicstyle={\small\ttfamily},
+  basicstyle={\ttfamily},
   breaklines=true,
   xleftmargin=0\zw,
   xrightmargin=0\zw,
@@ -43,8 +43,8 @@
   columns=[l]{fullflexible},
   numbers=left,
   stepnumber=1,
-  numberstyle={\scriptsize},
-%  numbersep=5pt,
+%  numberstyle={\scriptsize},
+  numbersep=5pt,
   language={},
   tabsize=4,
   lineskip=-0.1\zw,
@@ -55,7 +55,15 @@
 \usepackage{url}
 \usepackage{amssymb}
 
-\setlength{\columnsep}{10mm}
+%\bibliographystyle{plain}
+%\bibliography{soto}
+\usepackage[backend=biber, style=numeric]{biblatex}
+\nocite{*}
+\addbibresource{soto.bib}
+%\bibliography{soto} %hoge.bibから拡張子を外した名前
+%\bibliographystyle{junsrt} %参考文献出力スタイル
+
+\setlength{\columnsep}{5mm}
 
 \begin{document}
 \ltjsetparameter{jacharrange={-3}}
@@ -79,23 +87,37 @@
     \input{tex/future.tex}% 今後の課題
 	
 % 参考文献	
-\begin{thebibliography}{9}
-\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}
-
+% \begin{thebibliography}{9}
+% \bibitem{cbc} 
+% 	cbc-gcc - 並列信頼研 mercurial repository. \\
+% 	\url{http://www.cr.ie.u-ryukyu.ac.jp/hg/CbC/CbC_gcc/}. 2020/09/10.
+% \bibitem{ryokka} 
+% 	Continuation based C での Hoare Logic を用いた仕様記述と検証. Master's thesis,\\
+% 	琉球大学 大学院理工学研究科 情報工学専攻, 2020. 
+% \bibitem{hoare} 
+% 	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.
+% \bibitem{meta} 
+% 	徳森海斗. Llvm clang 上の continuation based c コンパイラ の改良. Master's thesis, \\
+% 	琉球大学 大学院理工学研究科 情報工学専攻, 2016.
+% \bibitem{rbtree} 
+% 	渡邉敏正. データ構造と基本アルゴリズム. \\
+% 	共立出版株式会社, 2015.
+% \end{thebibliography}
+% \printbibliography[title=参考文献]
+	\printbibliography
 \end{multicols*}
 
 \end{document}
diff -r 2652bc4fc17f -r c162ca9b997e soto.bib
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/soto.bib	Tue Sep 15 04:49:26 2020 +0900
@@ -0,0 +1,4 @@
+@misc{cbc-gcc,
+    title = {Hoare Logic - 並列信頼研 mercurial repository},
+    howpublished = {\url{http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/ryokka/HoareLogic/}},
+    note = {Accessed: 2020/2/9(Sun)},}
diff -r 2652bc4fc17f -r c162ca9b997e tex/abstract.tex
--- a/tex/abstract.tex	Tue Sep 15 02:14:28 2020 +0900
+++ b/tex/abstract.tex	Tue Sep 15 04:49:26 2020 +0900
@@ -1,6 +1,6 @@
 \renewcommand{\abstractname}{\normalsize 要 旨}
 \begin{abstract}
-	当研究室にて Continuation based C (以下CbC) なるC言語の下位言語に当たる言語を開発している。
+	当研究室にて Continuation based C \cite{cbc-gcc} (以下CbC) なるC言語の下位言語に当たる言語を開発している。
 	先行研究にて Floyd-Hoare Logic(以下Hoare Logic)を用いてその検証を行なった。
 	本稿では、先行研究にて実施されなかった CbC における赤黒木の検証を Hoare Logic を用いて検証することを目指す。
 \end{abstract}
diff -r 2652bc4fc17f -r c162ca9b997e tex/hoare.tex
--- a/tex/hoare.tex	Tue Sep 15 02:14:28 2020 +0900
+++ b/tex/hoare.tex	Tue Sep 15 04:49:26 2020 +0900
@@ -19,7 +19,7 @@
 条件を満たしているのかをMeta CodeGear で検証する。
 
 \begin{center}
-\includegraphics[height=3.5cm]{pic/hoare_cg_dg.pdf}
+\includegraphics[height=3.4cm]{pic/hoare_cg_dg.pdf}
 \caption{CodeGear、DataGear での Hoare Logic}
 \label{hoare}
 \end{center}