%% v3.1 [2018/04/18]
%\documentclass[Proof,technicalreport]{ieicej}
\documentclass[technicalreport]{ieicej}

\usepackage[dvipdfmx]{graphicx}
\usepackage{graphicx}
\usepackage[T1]{fontenc}
\usepackage{lmodern}
\usepackage{textcomp}
\usepackage{latexsym}
%\usepackage[fleqn]{amsmath}
%\usepackage{amssymb}

\usepackage{listings}
\lstset{
  frame=single,
  keepspaces=true,
  stringstyle={\ttfamily},
  commentstyle={\ttfamily},
  identifierstyle={\ttfamily},
  keywordstyle={\ttfamily},
  basicstyle={\ttfamily},
  breaklines=true,
  xleftmargin=0zw,
  xrightmargin=0zw,
  framerule=.2pt,
  columns=[l]{fullflexible},
  numbers=left,
  stepnumber=1,
  numberstyle={\scriptsize},
  numbersep=1em,
  language={},
  tabsize=4,
  lineskip=-0.5zw,
    inputencoding=utf8,
    extendedchars=true,
    escapechar={@}
}
\renewcommand{\lstlistingname}{Code}
\usepackage{caption}
\captionsetup[lstlisting]{font={small,tt}}

\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[masataka@cr.ie.u-ryukyu.ac.jp]{外間 政尊}{Masataka Hokama}{1}% 
 \authorentry[kono@cr.ie.u-ryukyu.ac.jp]{河野 真治}{Shinji Kono}{2}% 
}
\affiliate[1]{琉球大学大学院理工学研究科情報工学専攻}
  {Interdisciplinary Information Engineering, Graduate School 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}
  プログラミング言語,
  CbC, Gears OS, Agda
  %% あと他…？
\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}
Gears OS は信頼性をノーマルレベルの計算に対して保証し、拡張性をメタレベルの計算で実現することを目標に開発している OSである。

Gears OS は処理の単位を Code Gear、データの単位を Data Gear と呼ばれる単位でプログラムを構成する。
信頼性や拡張性はメタ計算として、通常の計算とは区別して記述する。


\section{CodeGearとDataGear}

Gears OS ではプログラムとデータの単位として CodeGear、 DataGear を用いる。 Gear
 は並列実行の単位、データ分割、 Gear 間の接続等になる。
CodeGear はプログラムの処理そのもので、図\ref{fig:cgdg}で示しているように任意の数の
Input DataGear を参照し、処理が完了すると任意の数の Output DataGear に書き込む。

CodeGear 間の移動は継続を用いて行われる。継続は関数呼び出しとは異なり、呼び出し
た後に元のコードに戻らず、次の CodeGear へ継続を行う。これは、関数型プログラミングでは末尾関数呼び出しを行うことに相当する。

Gear では処理やデータ構造が CodeGear、 DataGear に閉じている。したがって、
DataGear は Agda のデータ構造(data と record)で表現できる。
CodeGear は Agda の CPS (Continuation Passing Style) で関数として表現することができる。

\begin{figure}[htpb]
 \begin{center}
   \scalebox{0.3}{\includegraphics{pic/codeGear_dataGear.pdf}}
 \end{center}
 \caption{CodeGear と DataGear の関係}
 \label{fig:cgdg}
\end{figure}

また Gears OS 自体もこの Code Gear、Data Gear を用いた CbC(Continuation based C) で実装される。
そのため、Gears OS の実装は Code Gear、Data Gear を用いたプログラミングスタイルの指標となる。

CodeGear は Agda では継続渡しで書かれた関数と等価である。
継続は不定の型 (\verb+t+) を返す関数で表される。
CodeGear 自体も同じ型 \verb+t+ を返す関数となる。
例えば、 Stack への push を行う関数 pushStack は以下のような型を持つ。

\begin{lstlisting}[caption=pushStack の型,label=push-stack]
   pushStack : a -> (Stack a si -> t) -> t
\end{lstlisting}

\verb+pushStack+ が関数名で、コロンの後ろに型を記述する。
最初の引数は Stack に格納される型\verb+a+ を持つ。
二つ目の引数は継続であり、\verb+Stack a si+ (\verb+si+という実装を持つ\verb+a+を格納するStack)を受け取り不定の型\verb+t+を返す関数である。
この CodeGear 自体は不定の型\verb+t+を返す。

GearsOS で CodeGear の性質を証明するには、 Agda で記述された CodeGear と
DataGear に対してメタ計算として証明を行う。証明すべき性質は、不定の型を持つ継続
\verb+t+ に記述することができる。例えば、 Stack にある値\verb+x+をpushして、pop
すると \verb+ x'+ が取れてくる。\verb+Just x+ と\verb+Just x'+ は等しい必要があ
る。これは Agda では \verb+(Just x ≡ x' )+ と記述される。
ここで Just とは Agda の以下のデータ構造である。

% \begin{verbatim}
\begin{lstlisting}[caption=data型の例:Maybe,label=maybe]
data Maybe {n : Level } (a : Set n) : Set n where
  Nothing : Maybe a
  Just    : a -> Maybe a
\end{lstlisting}
% \end{verbatim}

これは DataGear に相当し、\verb+Nothing+ と \verb+Just+ の二つの状態を保つ。
pop した時に、 Stack が空であれば\verb+Nothing+ を返し、そうでなければ\verb+Just+ のついた返り値を返す。

この性質を Agda で表すと、以下のような型になる。
Agda では証明すべき論理式は型で表される。
継続部分に直接証明すべき性質を型として記述できる。
Agda ではこの型に対応する$\lambda$項を与えると証明が完了したことになる。

\begin{lstlisting}[caption=pushとpop,label=push-pop]
push->pop : {l : Level} {D : Set l} (x : D )
        (s : SingleLinkedStack D) -> 
        pushStack (stackInSomeState s)
        x (\s -> popStack s 
        ( \s3 x1 -> (Just x ≡ x1)))
\end{lstlisting}

このように、CodeGear を Agda で記述し、継続部分に証明すべき性質を Agda で記述する。

GearsOS での記述は interface によってモジュール化される。
よって、このモジュール化もAgda により記述する必要がある。
CbC で記述された任意の CodeGear と Meta CodeGear が Agda にそのまま変換されるわけではないが、変換可能なように記述されると仮定する。


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