|
3
|
1 \documentclass[a4j,9.5pt]{article}
|
|
|
2 \usepackage{graphicx}
|
|
0
|
3 \usepackage{picins}
|
|
|
4 \usepackage{fancyhdr}
|
|
1
|
5 \usepackage[]{multicol}
|
|
3
|
6 \usepackage{listings}
|
|
0
|
7 %\pagestyle{fancy}
|
|
3
|
8 \lhead{\parpic{\includegraphics[height=1\zw,keepaspectratio,bb=0 0 251 246]{pic/emblem-bitmap.pdf}}琉球大学主催 工学部工学科知能情報コース 中間発表予稿}
|
|
0
|
9 \rhead{}
|
|
|
10 \cfoot{}
|
|
|
11
|
|
|
12 \setlength{\topmargin}{-1in \addtolength{\topmargin}{15mm}}
|
|
|
13 \setlength{\headheight}{0mm}
|
|
|
14 \setlength{\headsep}{5mm}
|
|
|
15 \setlength{\oddsidemargin}{-1in \addtolength{\oddsidemargin}{11mm}}
|
|
|
16 \setlength{\evensidemargin}{-1in \addtolength{\evensidemargin}{21mm}}
|
|
|
17 \setlength{\textwidth}{181mm}
|
|
|
18 \setlength{\textheight}{261mm}
|
|
|
19 \setlength{\footskip}{0mm}
|
|
|
20 \pagestyle{empty}
|
|
7
|
21 \usepackage[top=20mm, bottom=20mm, left=10mm, right=10mm]{geometry}
|
|
3
|
22 % 特殊文字の表示に必要
|
|
|
23 \usepackage{luatexja}
|
|
|
24 \usepackage{fontspec}
|
|
|
25 \setmainfont{STIX Math}%
|
|
|
26 \setmonofont{STIXGeneralBol}[
|
|
|
27 Scale=MatchLowercase
|
|
|
28 ]
|
|
1
|
29
|
|
8
|
30
|
|
1
|
31 \lstset{
|
|
|
32 frame=single,
|
|
|
33 keepspaces=true,
|
|
|
34 stringstyle={\ttfamily},
|
|
|
35 commentstyle={\ttfamily},
|
|
|
36 identifierstyle={\ttfamily},
|
|
|
37 keywordstyle={\ttfamily},
|
|
10
|
38 basicstyle={\ttfamily},
|
|
1
|
39 breaklines=true,
|
|
3
|
40 xleftmargin=0\zw,
|
|
|
41 xrightmargin=0\zw,
|
|
1
|
42 framerule=.3pt,
|
|
|
43 columns=[l]{fullflexible},
|
|
9
|
44 numbers=left,
|
|
1
|
45 stepnumber=1,
|
|
10
|
46 % numberstyle={\scriptsize},
|
|
|
47 numbersep=5pt,
|
|
1
|
48 language={},
|
|
|
49 tabsize=4,
|
|
3
|
50 lineskip=-0.1\zw,
|
|
1
|
51 escapechar={@},
|
|
|
52 }
|
|
|
53
|
|
7
|
54 \usepackage{indentfirst}
|
|
9
|
55 \usepackage{url}
|
|
|
56 \usepackage{amssymb}
|
|
|
57
|
|
10
|
58 %\bibliographystyle{plain}
|
|
|
59 %\bibliography{soto}
|
|
|
60 \usepackage[backend=biber, style=numeric]{biblatex}
|
|
|
61 \nocite{*}
|
|
|
62 \addbibresource{soto.bib}
|
|
|
63 %\bibliography{soto} %hoge.bibから拡張子を外した名前
|
|
|
64 %\bibliographystyle{junsrt} %参考文献出力スタイル
|
|
|
65
|
|
|
66 \setlength{\columnsep}{5mm}
|
|
7
|
67
|
|
0
|
68 \begin{document}
|
|
3
|
69 \ltjsetparameter{jacharrange={-3}}
|
|
7
|
70 \title{\LARGE Continuation based C による RedBlackTree の Hoare Logic を用いた検証 \\ \Large Verification of red-black tree implemented in Continuation based C using Hoare Logic}
|
|
8
|
71 \author{学籍番号 175706H 氏名 上地 悠斗 \\ 指導教員 : 河野 真治}
|
|
0
|
72 \date{}
|
|
|
73 \maketitle
|
|
1
|
74 \thispagestyle{fancy}
|
|
0
|
75
|
|
1
|
76 % 要旨
|
|
3
|
77 \input{./tex/abstract.tex}
|
|
1
|
78
|
|
3
|
79 % 2段組開始
|
|
5
|
80 \begin{multicols*}{2}
|
|
7
|
81 \input{tex/intro.tex} % 研究目的
|
|
|
82 \input{tex/cbc.tex} % CbC の説明
|
|
8
|
83 \input{tex/agda.tex} % agda の説明
|
|
7
|
84 \input{tex/hoare.tex} % Hoare Logic の説明
|
|
|
85 \input{tex/rbtree.tex} % 赤黒木の説明
|
|
|
86 \input{tex/spec.tex}% 手法
|
|
8
|
87 \input{tex/future.tex}% 今後の課題
|
|
5
|
88
|
|
8
|
89 % 参考文献
|
|
10
|
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
|
|
5
|
121 \end{multicols*}
|
|
1
|
122
|
|
0
|
123 \end{document}
|
