Mercurial > hg > Papers > 2020 > soto-midterm

comparison mid_thesis.tex @ 9:2652bc4fc17f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
set src code numbers
author soto@cr.ie.u-ryukyu.ac.jp
date Tue, 15 Sep 2020 02:14:28 +0900
parents 27a6616b6683
children c162ca9b997e
comparison
equal deleted inserted replaced
8:27a6616b6683 9:2652bc4fc17f
39 breaklines=true, 39 breaklines=true,
40 xleftmargin=0\zw, 40 xleftmargin=0\zw,
41 xrightmargin=0\zw, 41 xrightmargin=0\zw,
42 framerule=.3pt, 42 framerule=.3pt,
43 columns=[l]{fullflexible}, 43 columns=[l]{fullflexible},
44 numbers=none, 44 numbers=left,
45 stepnumber=1, 45 stepnumber=1,
46 numberstyle={\scriptsize}, 46 numberstyle={\scriptsize},
47 numbersep=2em, 47 % numbersep=5pt,
48 language={}, 48 language={},
49 tabsize=4, 49 tabsize=4,
50 lineskip=-0.1\zw, 50 lineskip=-0.1\zw,
51 escapechar={@}, 51 escapechar={@},
52 } 52 }
53 53
54 \usepackage{indentfirst} 54 \usepackage{indentfirst}
55 \usepackage{url}
56 \usepackage{amssymb}
57
58 \setlength{\columnsep}{10mm}
55 59
56 \begin{document} 60 \begin{document}
57 \ltjsetparameter{jacharrange={-3}} 61 \ltjsetparameter{jacharrange={-3}}
58 \title{\LARGE Continuation based C による RedBlackTree の Hoare Logic を用いた検証 \\ \Large Verification of red-black tree implemented in Continuation based C using Hoare Logic} 62 \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 氏名 上地 悠斗 \\ 指導教員 : 河野 真治} 63 \author{学籍番号 175706H 氏名 上地 悠斗 \\ 指導教員 : 河野 真治}
74 \input{tex/spec.tex}% 手法 78 \input{tex/spec.tex}% 手法
75 \input{tex/future.tex}% 今後の課題 79 \input{tex/future.tex}% 今後の課題
76 80
77 % 参考文献 81 % 参考文献
78 \begin{thebibliography}{9} 82 \begin{thebibliography}{9}
79 \bibitem{1}CbCの論文 83 \bibitem{cbc}cbc-gcc - 並列信頼研 mercurial repository. \\
80 \bibitem{2}外間先輩の先行研究 84 \url{http://www.cr.ie.u-ryukyu.ac.jp/hg/CbC/CbC_gcc/}
81 \bibitem{3}Hoare Logicの論文 85 \bibitem{先行研究}外間政尊. Continuation based C での Hoare Logic を用いた仕様記述と検証. Master’s thesis,\\
82 \bibitem{4}Hoare Logicのスライド 86 琉球大学 大学院理工学研究科 情報工学専攻, 2020.
83 \bibitem{5}agda のサイト 87 \bibitem{hoaree}C. A. R. Hoare. An axiomatic basis for computer programming. \\
84 \bibitem{6}Aaron Stumpの本 88 Commun. ACM, Vol. 12, No. 10, p. 576–580, October 1969.
85 \bibitem{7}atttonさんの論文 89 \bibitem{agda-wiki}The agda wiki. \\
86 \bibitem{8}Haskell 90 \url{http://wiki.portal.chalmers.se/agda/pmwiki.php}. 2020/09/10.
87 \bibitem{9}Coq 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.
88 \end{thebibliography} 97 \end{thebibliography}
89 98
90 \end{multicols*} 99 \end{multicols*}
91 100
92 \end{document} 101 \end{document}