Mercurial > hg > Papers > 2020 > soto-midterm

comparison mid_thesis.tex @ 11:a8bc8c6b48bd default tip

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author soto@cr.ie.u-ryukyu.ac.jp
date Tue, 15 Sep 2020 07:06:29 +0900
parents c162ca9b997e
children
comparison
equal deleted inserted replaced
10:c162ca9b997e 11:a8bc8c6b48bd
53 53
54 \usepackage{indentfirst} 54 \usepackage{indentfirst}
55 \usepackage{url} 55 \usepackage{url}
56 \usepackage{amssymb} 56 \usepackage{amssymb}
57 57
58 %\bibliographystyle{plain} 58 \usepackage[backend=biber, style=numeric, bibstyle=ieee]{biblatex}
59 %\bibliography{soto}
60 \usepackage[backend=biber, style=numeric]{biblatex}
61 \nocite{*} 59 \nocite{*}
62 \addbibresource{soto.bib} 60 \addbibresource{soto.bib}
63 %\bibliography{soto} %hoge.bibから拡張子を外した名前
64 %\bibliographystyle{junsrt} %参考文献出力スタイル
65 61
66 \setlength{\columnsep}{5mm} 62 \setlength{\columnsep}{5mm}
63 \def\lstlistingname{ソースコード}
64
65 \newcommand\figref[1]{図 \ref{#1}}
66 \newcommand\coderef[1]{ソースコード \ref{#1}}
67 67
68 \begin{document} 68 \begin{document}
69 \ltjsetparameter{jacharrange={-3}} 69 \ltjsetparameter{jacharrange={-3}}
70 \title{\LARGE Continuation based C による RedBlackTree の Hoare Logic を用いた検証 \\ \Large Verification of red-black tree implemented in Continuation based C using Hoare Logic} 70 \title{\LARGE Continuation based C による RedBlackTree の Hoare Logic を用いた検証 \\ \Large Verification of red-black tree implemented in Continuation based C using Hoare Logic}
71 \author{学籍番号 175706H 氏名 上地 悠斗 \\ 指導教員 : 河野 真治} 71 \author{学籍番号 175706H 氏名 上地 悠斗 \\ 指導教員 : 河野 真治}
83 \input{tex/agda.tex} % agda の説明 83 \input{tex/agda.tex} % agda の説明
84 \input{tex/hoare.tex} % Hoare Logic の説明 84 \input{tex/hoare.tex} % Hoare Logic の説明
85 \input{tex/rbtree.tex} % 赤黒木の説明 85 \input{tex/rbtree.tex} % 赤黒木の説明
86 \input{tex/spec.tex}% 手法 86 \input{tex/spec.tex}% 手法
87 \input{tex/future.tex}% 今後の課題 87 \input{tex/future.tex}% 今後の課題
88 88 \printbibliography[title={参考文献}]
89 % 参考文献
90 % \begin{thebibliography}{9}
91 % \bibitem{cbc}
92 % cbc-gcc - 並列信頼研 mercurial repository. \\
93 % \url{http://www.cr.ie.u-ryukyu.ac.jp/hg/CbC/CbC_gcc/}. 2020/09/10.
94 % \bibitem{ryokka}
95 % Continuation based C での Hoare Logic を用いた仕様記述と検証. Master's thesis,\\
96 % 琉球大学 大学院理工学研究科 情報工学専攻, 2020.
97 % \bibitem{hoare}
98 % C. A. R. Hoare. An axiomatic basis for computer programming. \\
99 % Commun. ACM, Vol. 12, No. 10, p. 576–580, October 1969.
100 % \bibitem{agda-wiki}
101 % The agda wiki. \\
102 % \url{http://wiki.portal.chalmers.se/agda/pmwiki.php}. 2020/09/10.
103 % \bibitem{agda-doc}
104 % Welcome to agda’s documentation!. \\
105 % \url{http://agda.readthedocs.io/en/latest/}. 2020/09/10.
106 % \bibitem{agda-book}
107 % Aaron Stump. Verified Functional Programming in Agda.
108 % Association for Computing Machinery and Morgan; Claypool, New York, NY, USA, 2016.
109 % \bibitem{atton}
110 % 比嘉健太. メタ計算を用いた continuation based c の検証手法. Master's thesis, \\
111 % 琉球大学 大学院理工学研究科 情報工学専攻, 2017.
112 % \bibitem{meta}
113 % 徳森海斗. Llvm clang 上の continuation based c コンパイラ の改良. Master's thesis, \\
114 % 琉球大学 大学院理工学研究科 情報工学専攻, 2016.
115 % \bibitem{rbtree}
116 % 渡邉敏正. データ構造と基本アルゴリズム. \\
117 % 共立出版株式会社, 2015.
118 % \end{thebibliography}
119 % \printbibliography[title=参考文献]
120 \printbibliography
121 \end{multicols*} 89 \end{multicols*}
122 90
123 \end{document} 91 \end{document}