|
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
|
|
|
30 \renewcommand{\abstractname}{要 旨}
|
|
|
31 \lstset{
|
|
|
32 frame=single,
|
|
|
33 keepspaces=true,
|
|
|
34 stringstyle={\ttfamily},
|
|
|
35 commentstyle={\ttfamily},
|
|
|
36 identifierstyle={\ttfamily},
|
|
|
37 keywordstyle={\ttfamily},
|
|
|
38 basicstyle={\small\ttfamily},
|
|
|
39 breaklines=true,
|
|
3
|
40 xleftmargin=0\zw,
|
|
|
41 xrightmargin=0\zw,
|
|
1
|
42 framerule=.3pt,
|
|
|
43 columns=[l]{fullflexible},
|
|
|
44 numbers=none,
|
|
|
45 stepnumber=1,
|
|
|
46 numberstyle={\scriptsize},
|
|
|
47 numbersep=2em,
|
|
|
48 language={},
|
|
|
49 tabsize=4,
|
|
3
|
50 lineskip=-0.1\zw,
|
|
1
|
51 escapechar={@},
|
|
|
52 }
|
|
|
53
|
|
7
|
54 \usepackage{indentfirst}
|
|
|
55
|
|
0
|
56 \begin{document}
|
|
3
|
57 \ltjsetparameter{jacharrange={-3}}
|
|
7
|
58 \title{\LARGE Continuation based C による RedBlackTree の Hoare Logic を用いた検証 \\ \Large Verification of red-black tree implemented in Continuation based C using Hoare Logic}
|
|
|
59 \author{学籍番号 175706H 氏名 上地 悠斗 \and 指導教員 : 河野 真治}
|
|
0
|
60 \date{}
|
|
|
61 \maketitle
|
|
1
|
62 \thispagestyle{fancy}
|
|
0
|
63
|
|
1
|
64 % 要旨
|
|
3
|
65 \input{./tex/abstract.tex}
|
|
1
|
66
|
|
3
|
67 % 2段組開始
|
|
5
|
68 \begin{multicols*}{2}
|
|
7
|
69 \input{tex/intro.tex} % 研究目的
|
|
|
70 \input{tex/cbc.tex} % CbC の説明
|
|
|
71 \input{tex/hoare.tex} % Hoare Logic の説明
|
|
|
72 \input{tex/agda.tex} % agda の説明
|
|
|
73 \input{tex/rbtree.tex} % 赤黒木の説明
|
|
|
74 \input{tex/spec.tex}% 手法
|
|
1
|
75
|
|
5
|
76 \section{今後の課題}
|
|
|
77 % 参考文献
|
|
|
78
|
|
0
|
79 \begin{thebibliography}{9}
|
|
1
|
80 \bibitem{1}CbCの論文
|
|
|
81 \bibitem{2}外間先輩の先行研究
|
|
|
82 \bibitem{3}Hoare Logicの論文
|
|
|
83 \bibitem{4}Hoare Logicのスライド
|
|
|
84 \bibitem{5}agda のサイト
|
|
|
85 \bibitem{6}Aaron Stumpの本
|
|
|
86 \bibitem{7}atttonさんの論文
|
|
|
87 \bibitem{8}Haskell
|
|
|
88 \bibitem{9}Coq
|
|
3
|
89 \end{thebibliography}
|
|
0
|
90
|
|
5
|
91 \end{multicols*}
|
|
1
|
92
|
|
0
|
93 \end{document}
|
