view Paper/master_paper.tex @ 28:423f59b098ac

Add svg
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Wed, 15 Feb 2023 17:18:23 +0900
parents 19f19ec356f5
children 4915eaa51ee0
line wrap: on
line source

\documentclass[12pt,a4paper,uplatex]{ujreport}
\usepackage{master_paper}
\usepackage{ascmac}
\usepackage[dvipdfmx]{graphicx}
\usepackage{here}
\usepackage{listings}
\usepackage{comment}
\usepackage{url}
\usepackage[deluxe, multi]{otf}
% 以下はハイパーリンク 要ダウンロード
\usepackage[dvipdfmx]{hyperref}
\usepackage{pxjahyper}

\usepackage{ascmac}
\usepackage[fleqn]{amsmath}
\usepackage{amssymb}

%\input{dummy.tex} %% font

\jtitle{Gears Agda での形式手法を用いたプログラムの検証}
\etitle{Verification of programs using formal methods in Gears Agda} %
\year{2023年 3月}
\eyear{March 2023}
\author{上地 悠斗}
\eauthor{Yuto Uechi}
\chife{指導教員:教授 和田 知久}
\echife{Supervisor: Prof. Tomohisa Wada}

\marklefthead{% 左上に挿入
  \begin{minipage}[b]{.4\textwidth}
    琉球大学大学院学位論文(修士)
\end{minipage}}

% \markleftfoot{% 左下に挿入
%  \begin{minipage}{.8\textwidth}
%    Gears OS の Paging
% \end{minipage}}

\newcommand\figref[1]{図 \ref{fig:#1}}
\newcommand\tabref[1]{表 \ref{tab:#1}}
\newcommand\coderef[1]{ソースコード \ref{code:#1}}

\lstset{
  language=C, 
  tabsize=2, 
  frame=single, 
  basicstyle={\tt\footnotesize}, % 
  identifierstyle={\footnotesize}, % 
  commentstyle={\footnotesize\itshape}, % 
  keywordstyle={\footnotesize\ttfamily}, % 
  ndkeywordstyle={\footnotesize\ttfamily}, % 
  stringstyle={\footnotesize\ttfamily}, 
  breaklines=true, 
  captionpos=b, 
  columns=[l]{fullflexible}, % 
  xrightmargin=0zw, % 
  xleftmargin=1zw, % 
  aboveskip=1zw, 
  numbers=left,
  numberstyle={\scriptsize}, % 
  stepnumber=1, 
  numbersep=0.5zw, % 
  lineskip=-0.5ex, 
  escapechar= \! ,
}

\def\lstlistingname{ソースコード}
\def\lstlistlistingname{ソースコード目次}

% ハイパーリンク
\hypersetup{
setpagesize=false,
 bookmarksnumbered=true,%
 bookmarksopen=true,%
 colorlinks=true,%
 linkcolor=black,
 citecolor=black,
}

%%% 索引のために以下の2行を追加
%\usepackage{makeidx,multicol}
%\makeindex
\begin{document}
%rome
\maketitle
\pagenumbering{roman}
\setcounter{page}{0}
\newpage


\makecommission
%\input{chapter/signature.tex}

\newpage

%要旨
\input{tex/abst.tex}

%発表履歴
\input{tex/history.tex}
\addcontentsline{toc}{chapter}{研究関連論文業績}

\mainmatter
%目次
\tableofcontents

%図目次
\listoffigures

%表目次
% \listoftables

%リスト目次
\lstlistoflistings

%chapters
\input{tex/intro.tex}
\input{tex/cbc.tex}
\input{tex/agda.tex}
\input{tex/cbc_agda.tex}

\input{tex/hoare.tex}
\input{tex/while_loop.tex} % while loop の実装と検証(簡単に)
\input{tex/tree_desc.tex}% Gears Agda における木構造の設計

\input{tex/spin_dpp.tex}
\input{tex/dpp_impl.tex}
\input{tex/conclusion.tex}

% %謝辞
\input{tex/thanks.tex}


%参考文献
\nocite{*}
\bibliography{reference}
\bibliographystyle{junsrt}


%発表履歴
%\addcontentsline{toc}{chapter}{発表履歴}
%\input{chapter/history.tex}

%付録
% \addcontentsline{toc}{chapter}{付録}
% \appendix
% \input{tex/appendix.tex}
\end{document}