%% v3.1 [2018/04/18]
%\documentclass[Proof,technicalreport]{ieicej}
\documentclass[technicalreport]{ieicej}
%\usepackage{graphicx}
\usepackage[T1]{fontenc}
\usepackage{lmodern}
\usepackage{textcomp}
\usepackage{latexsym}
%\usepackage[fleqn]{amsmath}
%\usepackage{amssymb}

\def\IEICEJcls{\texttt{ieicej.cls}}
\def\IEICEJver{3.1}
\newcommand{\AmSLaTeX}{%
 $\mathcal A$\lower.4ex\hbox{$\!\mathcal M\!$}$\mathcal S$-\LaTeX}
%\newcommand{\PS}{{\scshape Post\-Script}}
\def\BibTeX{{\rmfamily B\kern-.05em{\scshape i\kern-.025em b}\kern-.08em
 T\kern-.1667em\lower.7ex\hbox{E}\kern-.125em X}}

\jtitle{GearsOSのHoare tripleをベースにした検証手法}
%% \jsubtitle{技術研究報告原稿のための解説とテンプレート}
%% \etitle{How to Use \LaTeXe\ Class File (\IEICEJcls\ version \IEICEJver) 
%%         for the Technical Report of the Institute of Electronics, Information 
%%         and Communication Engineers}
%% \esubtitle{Guide to the Technical Report and Template}
\authorlist{
 \authorentry[@cr.ie.u-ryukyu.ac.jp]{外間 政尊}{Masataka Hokama}{1}% 
 \authorentry[@cr.ie.u-ryukyu.ac.jp]{河野 真治}{Shinji Kono}{2}% 
}
\affiliate[1]{琉球大学大学院理工学研究科情報工学専攻}
  {Interdisciplinary Information Engineering, Graduate Sc k533 hool of Engineering and Science, University of the Ryukyus.}
\affiliate[2]{琉球大学工学部情報工学科}
  {Information Engineering, University of the Ryukyus.}
%\MailAddress{$\dagger$hanako@denshi.ac.jp,
% $\dagger\dagger$\{taro,jiro\}@jouhou.co.jp}
\begin{document}
\begin{jabstract}
  あらまし
\end{jabstract}
\begin{jkeyword}
  プログラミング言語,
  検証
  %% あと他…？
\end{jkeyword}
%% \begin{eabstract}
%%   %% メールを見た感じ日本語のみとなっていたので不必要…？
%% \end{eabstract}
%% \begin{ekeyword}
%%   %% 不必要？
%% \end{ekeyword}
\maketitle
\section{まえがき}
% とりあえずabstをそのまま
Gears OS は継続を主とするプログラミング言語 CbC で記
述されている。
OS やアプリケーションの信頼性を上げるには仕様を満
たしていることを確認する必要がある。
現在 GearsOS の仕様の確認には定理証明系である Agda を
用いている。
CbC では関数呼び出しを用いず goto 文により遷移する
。
これは Agda 上では継続渡しの記述を用いた関数として
記述する。
また、継続にはある関数を実行するための事前条件や
事後条件などをもたせることが可能である。
Hoare triple では事前条件が成り立っているときにある
関数を実行して、それが停止する際に事後条件を満た
すことを確認する。
これは継続を用いた Agda 上では事前条件を継続で関数
に渡し、関数からさらに継続した先で事後条件が成り
立つという形で記述できる。
本発表では GearsOS の仕様確認に Hoare triple をベースと
した証明を導入し、今まで行っていた証明との比較を
行う。
\section{GearsOS}
GearsOSについて

\section{CodeGearとDataGear}
CodeGearとDataGearについて

\section{AgdaとGearsOS}
Agda と GearsOS

\begin{thebibliography}{99}
%\bibitem{ohno}
%大野義夫編，\TeX\ 入門，
%共立出版，東京，1989. 

%\bibitem{Seroul}
%R. Seroul and S. Levy, A Beginner's Book of \TeX, 
%Springer-Verlag, New York, 1989. 

%\bibitem{nodera1}
%野寺隆志，楽々\LaTeX{}，
%共立出版，東京，1990. 

%\bibitem{itou}
%伊藤和人，\LaTeX\ トータルガイド，
%秀和システムトレーディング，1991. 

%\bibitem{nodera2}
%野寺隆志，今度こそ\AmSLaTeX{}，
%共立出版，東京，1991. 

\bibitem{ryokka-sigos}
外間政尊, 河野真治, GearsOSのAgdaによる記述と検証，
\\システムソフトウェアとオペレーティング・システム研究会, 2018.

\end{thebibliography}

\end{document}