|
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}
|
|
3
|
21 \usepackage[top=2cm, bottom=2cm, left=1cm, right=1cm]{geometry}
|
|
|
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
|
|
0
|
54 \begin{document}
|
|
3
|
55 \ltjsetparameter{jacharrange={-3}}
|
|
|
56 \title{Continuation based C による赤黒木の Hoare Logic を用いた検証 \\ Verification of red-black tree implemented in Continuation based C using Hoare Logic}
|
|
1
|
57 \author{学籍番号 175706H 氏名 上地 悠斗 \\ 指導教員 : 河野 真治}
|
|
0
|
58 \date{}
|
|
|
59 \maketitle
|
|
1
|
60 \thispagestyle{fancy}
|
|
0
|
61
|
|
1
|
62 % 要旨
|
|
3
|
63 \input{./tex/abstract.tex}
|
|
1
|
64
|
|
3
|
65 % 2段組開始
|
|
|
66 \begin{multicols}{2}
|
|
|
67 \input{./tex/intro.tex} % 研究目的
|
|
|
68 \input{./tex/cbc.tex} % CbC の説明
|
|
|
69 \input{./tex/hoare.tex} % Hoare Logic の説明
|
|
|
70 \input{./tex/agda.tex} % agda の説明
|
|
|
71 \input{./tex/spec.tex}% 手法
|
|
1
|
72
|
|
|
73 \section{今後の課題}
|
|
|
74
|
|
3
|
75 % 参考文献
|
|
0
|
76 \begin{thebibliography}{9}
|
|
|
77
|
|
1
|
78 \bibitem{1}CbCの論文
|
|
|
79 \bibitem{2}外間先輩の先行研究
|
|
|
80 \bibitem{3}Hoare Logicの論文
|
|
|
81 \bibitem{4}Hoare Logicのスライド
|
|
|
82 \bibitem{5}agda のサイト
|
|
|
83 \bibitem{6}Aaron Stumpの本
|
|
|
84 \bibitem{7}atttonさんの論文
|
|
|
85 \bibitem{8}Haskell
|
|
|
86 \bibitem{9}Coq
|
|
3
|
87 \end{thebibliography}
|
|
0
|
88
|
|
1
|
89 \end{multicols}
|
|
|
90
|
|
0
|
91 \end{document}
|
