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},
|
|
38 basicstyle={\small\ttfamily},
|
|
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,
|
|
46 numberstyle={\scriptsize},
|
9
|
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
|
|
58 \setlength{\columnsep}{10mm}
|
7
|
59
|
0
|
60 \begin{document}
|
3
|
61 \ltjsetparameter{jacharrange={-3}}
|
7
|
62 \title{\LARGE Continuation based C による RedBlackTree の Hoare Logic を用いた検証 \\ \Large Verification of red-black tree implemented in Continuation based C using Hoare Logic}
|
8
|
63 \author{学籍番号 175706H 氏名 上地 悠斗 \\ 指導教員 : 河野 真治}
|
0
|
64 \date{}
|
|
65 \maketitle
|
1
|
66 \thispagestyle{fancy}
|
0
|
67
|
1
|
68 % 要旨
|
3
|
69 \input{./tex/abstract.tex}
|
1
|
70
|
3
|
71 % 2段組開始
|
5
|
72 \begin{multicols*}{2}
|
7
|
73 \input{tex/intro.tex} % 研究目的
|
|
74 \input{tex/cbc.tex} % CbC の説明
|
8
|
75 \input{tex/agda.tex} % agda の説明
|
7
|
76 \input{tex/hoare.tex} % Hoare Logic の説明
|
|
77 \input{tex/rbtree.tex} % 赤黒木の説明
|
|
78 \input{tex/spec.tex}% 手法
|
8
|
79 \input{tex/future.tex}% 今後の課題
|
5
|
80
|
8
|
81 % 参考文献
|
0
|
82 \begin{thebibliography}{9}
|
9
|
83 \bibitem{cbc}cbc-gcc - 並列信頼研 mercurial repository. \\
|
|
84 \url{http://www.cr.ie.u-ryukyu.ac.jp/hg/CbC/CbC_gcc/}
|
|
85 \bibitem{先行研究}外間政尊. Continuation based C での Hoare Logic を用いた仕様記述と検証. Master’s thesis,\\
|
|
86 琉球大学 大学院理工学研究科 情報工学専攻, 2020.
|
|
87 \bibitem{hoaree}C. A. R. Hoare. An axiomatic basis for computer programming. \\
|
|
88 Commun. ACM, Vol. 12, No. 10, p. 576–580, October 1969.
|
|
89 \bibitem{agda-wiki}The agda wiki. \\
|
|
90 \url{http://wiki.portal.chalmers.se/agda/pmwiki.php}. 2020/09/10.
|
|
91 \bibitem{agda-doc}Welcome to agda’s documentation!. \\
|
|
92 \url{http://agda.readthedocs.io/en/latest/}. 2020/09/10.
|
|
93 \bibitem{agda-book}Aaron Stump. Verified Functional Programming in Agda.
|
|
94 Association for Computing Machinery and Morgan; Claypool, New York, NY, USA, 2016.
|
|
95 \bibitem{atton}比嘉健太. メタ計算を用いた continuation based c の検証手法. Master’s thesis, \\
|
|
96 琉球大学 大学院理工学研究科 情報工学専攻, 2017.
|
3
|
97 \end{thebibliography}
|
0
|
98
|
5
|
99 \end{multicols*}
|
1
|
100
|
0
|
101 \end{document}
|