\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}

\chapter{Gears Agda による定理証明}
先行研究では、Hoare Logic を 使用して while loop の検証を行っていた。
本研究では、invariant というプログラムの不変条件を定義し、それを検証することで、比較的容易に検証を行うことができるようになった(本章2節)
本章では Gears Agda による定理証明の方法について説明する。

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

\input{tex/spin_dpp.tex}% Gears Agda の記法　loopのやつやる
\input{tex/dpp_impl.tex}% Gears Agda の記法　loopのやつやる

\chapter{まとめと今後の展望}
本論文では Gears Agda による形式手法を用いたプログラムの検証について述べた。そこで、定理証明については Invariant を用いて定理証明を行った。モデル検査については Gears Agda にて dead lock を検知できるようになった。

実際に Invariant を用いることで、プログラムに与える入力とその出力に対して条件を与え、Hoare Logic による検証を行えるようになった。
これにより、いままでより容易に Gears Agda にて検証が進められるようになった。

また、先行研究での課題にて、CbCで開発、検証を行いたいと考えている Gears OSの並列並列動作の検証があった。これもモデル検査により、Gears Agda 内で並列動作に対する検証も行えるようになった。


\section{今後の課題}
今後の課題としてモデル検査による検証、定理証明による検証、Gears Agda の今後の展望について述べる。
モデル検査においては、有効オートマトンによるプログラムの遷移を全自動探索することと、live lockやアサーションの検証を行いたい。
加えて、State List のデータ構造を brunced tree にすることで、並列にモデル検査が行えるようになると考えられる。
これにより、状態が膨大になるモデル検査に対応できる。

定理証明においては、Red Black Tree の検証を行いたいと思っている。
これで検証を行ったものをモデル検査や Gears OS のファイルシステムなどに転用できると考えている。

Gears Agda の展望について、CbC に変換することが挙げられる。
CbC はアセンブラに近いため記述が複雑かつ困難であるが、Gears Agda で記述したものを CbC に変換できるようになれば、その点を解決できる。更に、Gears Agda で検証を行ったプログラムであるため、プログラムの信頼性もある。
加えて、モデル検査の実行には速度が求められるが、CbCで高速に実行できるようになることが期待される。

% %謝辞
\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}