Mercurial > hg > Papers > 2020 > soto-midterm
view mid_thesis.tex @ 9:2652bc4fc17f
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 |
line wrap: on
line source
\documentclass[a4j,9.5pt]{article} \usepackage{graphicx} \usepackage{picins} \usepackage{fancyhdr} \usepackage[]{multicol} \usepackage{listings} %\pagestyle{fancy} \lhead{\parpic{\includegraphics[height=1\zw,keepaspectratio,bb=0 0 251 246]{pic/emblem-bitmap.pdf}}琉球大学主催 工学部工学科知能情報コース 中間発表予稿} \rhead{} \cfoot{} \setlength{\topmargin}{-1in \addtolength{\topmargin}{15mm}} \setlength{\headheight}{0mm} \setlength{\headsep}{5mm} \setlength{\oddsidemargin}{-1in \addtolength{\oddsidemargin}{11mm}} \setlength{\evensidemargin}{-1in \addtolength{\evensidemargin}{21mm}} \setlength{\textwidth}{181mm} \setlength{\textheight}{261mm} \setlength{\footskip}{0mm} \pagestyle{empty} \usepackage[top=20mm, bottom=20mm, left=10mm, right=10mm]{geometry} % 特殊文字の表示に必要 \usepackage{luatexja} \usepackage{fontspec} \setmainfont{STIX Math}% \setmonofont{STIXGeneralBol}[ Scale=MatchLowercase ] \lstset{ frame=single, keepspaces=true, stringstyle={\ttfamily}, commentstyle={\ttfamily}, identifierstyle={\ttfamily}, keywordstyle={\ttfamily}, basicstyle={\small\ttfamily}, breaklines=true, xleftmargin=0\zw, xrightmargin=0\zw, framerule=.3pt, columns=[l]{fullflexible}, numbers=left, stepnumber=1, numberstyle={\scriptsize}, % numbersep=5pt, language={}, tabsize=4, lineskip=-0.1\zw, escapechar={@}, } \usepackage{indentfirst} \usepackage{url} \usepackage{amssymb} \setlength{\columnsep}{10mm} \begin{document} \ltjsetparameter{jacharrange={-3}} \title{\LARGE Continuation based C による RedBlackTree の Hoare Logic を用いた検証 \\ \Large Verification of red-black tree implemented in Continuation based C using Hoare Logic} \author{学籍番号 175706H 氏名 上地 悠斗 \\ 指導教員 : 河野 真治} \date{} \maketitle \thispagestyle{fancy} % 要旨 \input{./tex/abstract.tex} % 2段組開始 \begin{multicols*}{2} \input{tex/intro.tex} % 研究目的 \input{tex/cbc.tex} % CbC の説明 \input{tex/agda.tex} % agda の説明 \input{tex/hoare.tex} % Hoare Logic の説明 \input{tex/rbtree.tex} % 赤黒木の説明 \input{tex/spec.tex}% 手法 \input{tex/future.tex}% 今後の課題 % 参考文献 \begin{thebibliography}{9} \bibitem{cbc}cbc-gcc - 並列信頼研 mercurial repository. \\ \url{http://www.cr.ie.u-ryukyu.ac.jp/hg/CbC/CbC_gcc/} \bibitem{先行研究}外間政尊. Continuation based C での Hoare Logic を用いた仕様記述と検証. Master’s thesis,\\ 琉球大学 大学院理工学研究科 情報工学専攻, 2020. \bibitem{hoaree}C. A. R. Hoare. An axiomatic basis for computer programming. \\ Commun. ACM, Vol. 12, No. 10, p. 576–580, October 1969. \bibitem{agda-wiki}The agda wiki. \\ \url{http://wiki.portal.chalmers.se/agda/pmwiki.php}. 2020/09/10. \bibitem{agda-doc}Welcome to agda’s documentation!. \\ \url{http://agda.readthedocs.io/en/latest/}. 2020/09/10. \bibitem{agda-book}Aaron Stump. Verified Functional Programming in Agda. Association for Computing Machinery and Morgan; Claypool, New York, NY, USA, 2016. \bibitem{atton}比嘉健太. メタ計算を用いた continuation based c の検証手法. Master’s thesis, \\ 琉球大学 大学院理工学研究科 情報工学専攻, 2017. \end{thebibliography} \end{multicols*} \end{document}