\documentclass[techrep]{ipsjpapers}
\usepackage[dvipdfmx]{graphicx}
\usepackage{url}
\usepackage{listings,jlisting}
\usepackage{enumitem}
\usepackage{bussproofs}
\usepackage{amsmath}
\usepackage{multirow}
\usepackage{here}
\usepackage{cite}
\usepackage{listings}
\usepackage{amssymb}

\lstset{
    language=C,
    tabsize=2,
    frame=single,
    basicstyle={\ttfamily\footnotesize},%
    identifierstyle={\footnotesize},%
    commentstyle={\footnotesize\itshape},%
    keywordstyle={\footnotesize\bfseries},%
    ndkeywordstyle={\footnotesize},%
    stringstyle={\footnotesize\ttfamily},
    breaklines=true,
    captionpos=b,
    columns=[l]{fullflexible},%
    xrightmargin=0zw,%
    xleftmargin=1zw,%
    aboveskip=1zw,
    numberstyle={\scriptsize},%
    stepnumber=1,
    numbersep=0.5zw,%
    lineskip=-0.5ex,
}
\renewcommand{\lstlistingname}{Code}
\usepackage{caption}
\captionsetup[lstlisting]{font={small,tt}}

\input{dummy.tex} %% Font

% ユーザが定義したマクロなど．
\makeatletter

\begin{document}

% 和文表題
\title{GearsOS の Agda による記述と検証}
% 英文表題
\etitle{}

% 所属ラベルの定義
\affilabel{1}{琉球大学大学院理工学研究科情報工学専攻 \\Interdisciplinary Information Engineering, Graduate School of Engineering and Science, University of the Ryukyus.}
\affilabel{2}{琉球大学工学部情報工学科\\Information Engineering, University of the Ryukyus.}

% 和文著者名
\author{
  外間 政尊\affiref{1}
  \and
  河野 真治\affiref{2}
}

% 英文著者名
\eauthor{
  Masataka HOKAMA\affiref{1}
  \and
  Shinji KONO\affiref{2}
}

% 連絡先（投稿時に必要．製版用では無視される．）
\contact{外間 政尊\\
        〒903-0213 沖縄県西原町千原1番地\\
	琉球大学工学部情報工学科\\
        TEL: (098)895-2221\qquad FAX: (098)895-8727\\
        email: masataka@cr.ie.u-ryukyu.ac.jp}

% 和文概要
\begin{abstract}
    Gears OS は継続を主とするプログラミング言語 CbC で記述されている。 OS やアプリケーションの信頼性を上げるには仕様を満たしていることを確認する必要がある。 確認方法にはモデル検査と証明がある。 ここでは定理証明支援系Agdaを用いた、CbC 言語の証明方法を考える。 CbC は関数呼び出しを用いず goto 文により遷移する。 これを継続を用いた関数型プログラムとして記述することができる。 この記述はAgda上で決まった形を持つ関数として表すことができる。 Gears OS のモジュールシステムは、実装とAPI を分離することを可能にしている。 このモジュールシステムを Agda 上で記述することができた。 継続は不定の型を返す関数で表されるので、継続に直接要求仕様を Agda の論理式として渡すことができる。 継続には仕様以外にも関数を呼び出すときの前提条件(pre-condition)を追加することが可能である。 これにより、Hoare Logic 的な証明を Agda で記述した CbC に直接載せることが可能になる。 Agda で記述された CbC と実装に用いる CbC は並行した形で存在する。 つまり、CbC のモジュールシステムで記述されたプログラムを比較的機械的に Agda で記述された CbC 変換することができる。 本論文ではAgda 上での CbC の記述手法とその上での Hoare Logic 的な証明手法について考察する。
\end{abstract}

% 英文概要
\begin{eabstract}
\end{eabstract}

% 表題などの出力
\maketitle

% 本文はここから始まる

% Introduce
% Code Gear は関数に比べて細かく分割されているのでメタ計算をより柔軟に記述できる。

% 研究目的

% 信頼性の高いOS

\section{定理証明系Agda を用いた GearsOS の検証}

動作するソフトウェアは高い信頼性を持つことが望ましい。
そのためにはソフトウェアが期待される動作をすることを保証する必要がある。
また、ソフトウェアが期待される動作をすることを保証するためには検証を行う必要が
ある。

当研究室では検証の単位として CodeGear、DataGear という単位を用いてソフトウェアを
記述する手法を提案しており、 CodeGear 、 DataGear という単位を用いてプログラミン
グする言語として Countinuation based C\cite{kaito:2015} (以下CbC)を開発している。
CbC はC言語と似た構文を持つ言語である。
また、 CodeGear、DataGear を用いて信頼性と拡張性をメタレベルで保証する GearsOS を CbC で開発している。

本研究では検証を行うために証明支援系言語 Agda を使用している。
Agda では型で証明したい論理式を書き、その型に合った実装を記述することで証明を記
述することができる。
 
本論文では CodeGear、DataGear での記述を Agda で表現した。
また、GearsOS で使われている interface の記述を Agda で表現し、その記述を通して
実装の仕様の一部に対して証明を行なった。
さらに、 Agda で継続を用いた記述をした際得られた知見や、継続と hoare logic を使っ
た今後の検証の方針を示す。

\section{CodeGear、 DataGear}

Gears OS ではプログラムとデータの単位として CodeGear、 DataGear を用いる。 Gear
 は並列実行の単位、データ分割、 Gear 間の接続等になる。
CodeGear はプログラムの処理そのもので、図\ref{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}

CodeGear は Agda では継続を用いた末尾呼び出しを行う関数として表現される。
継続は不定の型 (\verb+t+) を返す関数で表される。
CodeGear 自体も同じ型 \verb+t+ を返す関数となる。
例えば、 Stack への push を行う関数 pushStack は以下のような型を持つ。

\begin{verbatime}
   pushStack : a -> (Stack a si -> t) -> t
\end{verbatime}

\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'+ が取れてくる。Just x とJust x' は等しい必要がある。これはAgdaでは(Just x ≡ x' ) と記述される。
ここでJustとはAgdaの以下のデータ構造である。

\begin{verbtim}
data Maybe {n : Level } (a : Set n) : Set n where
  Nothing : Maybe a
  Just    : a -> Maybe a
\end{verbtim}

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

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


\begin{verbtim}
   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{verbtim}

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

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

以下の節では、Agda の基本について復習を行う。

\section{定理証明支援器 Agda での証明}


型システムを用いて証明を行うことができる言語として Agda \cite{agda}が存在する。
Agda は依存型という型システムを持つ。依存型とは型も第一級オブジェクトとする型シ
ステムで、依存型を持っている言語では型を基本的な操作に制限なしに使用できる
。
型システムは Curry-Howard 同型対応により命題と型付きラムダ計算が一対一で対応する。



\section{Agda の文法}

Agda はインデントに意味を持つため、きちんと揃える必要がある。
また、スペースの有無は厳格にチェックされる。

Agda における型指定は $:$ を用いて行う。

例えば、変数xが型Aを持つ、ということを表すには \verb/x : A/ と記述する。

データ型は、代数的なデータ構造で、その定義には \verb/data/ キーワードを用いる。
\verb/data/キーワードの後に \verb/data/ の名前と、型、 \verb/where/ 句を書きインデントを深くした後、値にコンストラクタとその型を列挙する。
Maybe はこのdata型の例である。


関数の定義は、関数名と型を記述した後に関数の本体を \verb/=/ の後に記述する。
関数の型には $ \rightarrow $ 、 または\verb/->/ を用いる。

例えば引数が型 \verb/A/ で返り値が型 \verb/B/ の関数は \verb/A -> B/ のように書
ける。
また、複数の引数を取る関数の型は \verb/A -> A -> B/ のように書ける。この
時の型は \verb/A -> (A -> B)/のように考えられる。
Bool 変数 \verb/x/ を取って true を返す関数 \verb/f/はリスト~\ref{agda-function}のようになる。

\lstinputlisting[label=agda-function, caption=Agda における関数定義] {src/AgdaFunction.agda}

引数は変数名で受けることもでき、具体的なコンストラクタを指定することでそのコンストラクタが渡された時の挙動を定義できる。
これはパターンマッチと呼ばれ、コンストラクタで case 文を行なっているようなもので
例えば Bool 型の値を反転する \verb/not/ 関数を書くとリスト~\ref{agda-not}のようになる。
% element の定義、縦棒　| の定義
% SingleLinkedStack の説明に必要なものだけ


パターンマッチでは全てのコンストラクタのパターンを含まなくてはならない。
例えば、Bool 型を受け取る関数で \verb/true/ の時の挙動のみを書くことはできない。
なお、コンストラクタをいくつか指定した後に変数で受けると、変数が持ちうる値は指定した以外のコンストラクタとなる。
例えばリスト~\ref{agda-pattern}の not は x には true しか入ることは無い。
なお、マッチした値以外の挙動をまとめて書く際には \verb/_/ を用いることもできる。

\lstinputlisting[label=agda-pattern, caption=Agdaにおけるパターンマッチ] {src/AgdaPattern.agda}

Agda にはラムダ式が存在している。ラムダ式とは関数内で生成できる無名の関数であり、
\verb/\arg1 arg2 -> function body/ のように書くことができる。
例えば Bool 型の引数 \verb/b/ を取って not を適用する \verb/not-apply/ をラムダ式で書くとリスト~\ref{agda-lambda}のようになる。
関数 \verb/not-apply/ をラムダ式を使わずに定義すると \verb/not-apply-2/ になるが、この二つの関数は同一の動作をする。

\lstinputlisting[label=agda-lambda, caption=Agda におけるラムダ式] {src/AgdaLambda.agda}

Agda では特定の関数内のみで利用できる関数を \verb/where/ 句で記述できる。
スコープは \verb/where/句が存在する関数内部のみであるため、名前空間が汚染させることも無い。
例えば自然数3つを取ってそれぞれ3倍して加算する関数 \verb/f/ を定義するとき、 \verb/where/ を使うとリスト~\ref{agda-where} のように書ける。
これは \verb/f'/ と同様の動作をする。
\verb/where/ 句は利用したい関数の末尾にインデント付きで \verb/where/ キーワードを記述し、改行の後インデントをして関数内部で利用する関数を定義する。

\lstinputlisting[label=agda-where, caption=Agda における where 句] {src/AgdaWhere.agda}

% Stackのinterface 部分を使ってrecord の説明をする
Agda のデータには C における構造体に相当するレコード型も存在する。
定義を行なう際は \verb/record/キーワードの後にレコード名、型、\verb/where/ の後に \verb/field/ キーワードを入れた後、フィールド名と型名を列挙する。
例えば x と y の二つの自然数からなるレコード \verb/Point/ を定義するとリスト~\ref{agda-record}のようになる。
レコードを構築する際は \verb/record/ キーワードの後の \verb/{}/ の内部に \verb/fieldName = value/ の形で値を列挙していく。
複数の値を列挙する際は \verb/;/ で区切る。

\lstinputlisting[label=agda-record, caption=Agdaにおけるレコード型の定義] {src/AgdaRecord.agda}

構築されたレコードから値を取得する際には \verb/RecordName.fieldName/ という名前の関数を適用する(リスト~\ref{agda-record-proj} 内2行目) 。
なお、レコードにもパターンマッチが利用できる(リスト~\ref{agda-record-proj} 内5行目)。
レコード内の値は \verb/record oldRecord {field = value ; ... }/ という構文を利用し更新することができる。
Point の中の x の値を5増やす関数 \verb/xPlus5/ はリスト~\ref{agda-record-proj}の 7,8行目のように書ける。

\lstinputlisting[label=agda-record-proj, caption=Agda におけるレコードの射影、パターンマッチ、値の更新] {src/AgdaRecordProj.agda}

% push と pop だけ書いて必要なものだけ説明する
% testStack08 を説明する。

\begin{itemize}
 \item 次に実行する CodeGear を指定する
 \item CodeGear に渡す DataGear を指定する
 \item 現在実行している CodeGear から制御を指定された CodeGear へと移す
\end{itemize}

の機能を持っている。

この機能を満たす関数はソースコード\ref{agda-goto} として定義されている。

\lstinputlisting[label=agda-goto, caption=Agdaにおける goto の定義] {src/Goto.agda}

goto は CodeGear よりも一つ Level が上の Meta CodeGear にあたり、次に実行する
CodeGear 型を受け取り、Input DataGear、 Output DataGear を返す。型になっている。


\section{Agda での Stack、 Binary Tree の実装}

ここでは Agda での Stack 、 Tree の実装を示す。

Stack の実装を以下のソースコード\ref{stack-impl}で示す。
実装は SingleLinkedStack という名前で定義されている。
定義されている API は一部を書き、残りは省略する。

\lstinputlisting[label=stack-impl, caption=Agdaにおける Stack の実装の一部] {src/AgdaStackImpl.agda}

Element は SingleLinkedStack で扱われる要素の定義で、現在のデータ datum と次のデー
タを Maybe 型という値の存在が不確かな場合の型で包み、自身で再帰的に定義している。
Maybe 型では値が存在する場合は Just 、 存在しない場合は　Nothing を返す。

SingleLinkedStack 型では、この Element の top 部分のみを定義している。

Stack に対する push 操作では stack と push する element 型の datum を受け取り、 datum
の next に現在の top を入れ、 stack の top を受け取った datum に切り替え、新しい
stack を返すというような実装をしている。

Tree の実装(以下のソースコード\ref{tree-impl})は RedBlackTree という名前で定義されている。
定義されている API は put 以後省略する。残りのの実装は付録に示す。 %~\

\lstinputlisting[label=tree-impl, caption=Agdaにおける Tree の実装] {src/AgdaTreeImpl.agda}

Node 型は key と value 、 Color と Node の rihgt 、 left の情報を持っている。
Tree を構成する末端の Node は leafNode 型で定義されている。

RedBlackTree 型は root の Node 情報と Tree に関する計算をする際に、そこまでの
Node の経路情報を保持するための nodeStack と 比較するための compare を持っている。

Tree の put 操作では tree 、 put するノードのキーと値(k1、value)を引数として受け
取り、Tree の root に Node が存在しているかどうかで場合分けしている。
Nothing が返ってきたときは RedBlackTree 型の tree 内に定義されている root に受け
取ったキーと値を新しいノードとして追加する。
Just が返ってきたときは root が存在するので、経路情報を積むために nodeStack を初
期化し、受け取ったキーと値で新たなノードを作成した後、ノードが追加されるべき位置
までキーの値を比べて新しい Tree を返すというような実装になっている。

\section{Agda における Interface の実装}

Agda で GearsOS のモジュール化の仕組みである interface を実装した。
interface とは、実装と仕様を分ける記述でここでは Stack の実装を
SingleLinkedStack 、 Stack の仕様を Stack とする。
interface は record で列挙し、ソースコード~\ref{agda-interface}のように紐付けることができる。
Agda では型を明記する必要があるため record 内に型を記述している。

例として Agda で実装した Stack 上の interface (ソースコード\ref{agda-interface})
の一部を見る。
Stack の実装は SingleLinkedStack(ソースコード\ref{agda-single-linked-stack}) として書かれている。それを Stack 側からinterface を通して呼び出している。

ここでの interface の型は Stack の record 内にある pushStack や popStack などで、
実際に使われる Stack の操作は StackMethods にある push や popである。この push
や pop は SingleLinkedStack で実装されている。

\lstinputlisting[label=agda-interface, caption=Agda における Interface の定義の
一部] {src/AgdaInterface.agda}

interface を通すことで、実際には Stack の push では stackImpl と何らかのデータ a を取
り、 stack を変更し、継続を返す型であったのが、 pushStack では 何らかのデータ a を取り stack を変更
して継続を返す型に変わっている。

また、 Tree でも interface を記述した。

\lstinputlisting[label=agda-tree, caption=Tree Interface の定義]{src/AgdaTree.agda}

interface を記述することによって、データを push する際に予め決まっている引数を省
略することができた。
また、 Agda で interface を記述することで CbC 側では意識していなかった型が、明確
化された。

% 元の push では 送り先の stack を関数に書く必要があり、異なる stack に push
% する可能性があったが、 pushStack では紐付けた Stack に push することになり

\section{継続を使った Agda における Test , Debug}
Agda ではプログラムのコンパイルが通ると型の整合性が取れていることは保証できるが、必ず
しも期待した動作をするとは限らない。そのため、本研究中に書いたプログラムが正しい動
作をしているかを確認するために行なった手法を幾つか示す。

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
今回は実験中にソースコード\ref{agda-stack-test}のような Test を書いた。
この Test では Stack をターゲットにしていて、 Stack に1、 2の二つの$ \mathbb{N} $型のデー
タを push した後、 pop2 Interface を使って Stack に入っている 1、 2 が Stack の
定義である First in Last out の通りに 2、 1 の順で取り出せるかを確認するために作成した。

\lstinputlisting[label=agda-stack-test, caption=Agdaにおけるテスト]{src/AgdaStackTest.agda}

上の Test では、02 が 2つのデータを push し、 03 で 二つのデータを pop する pop2
を行っている。それらをまとめて記述したものが 04 で 2 回 push し、 2つのデータを pop する動
作が正しく行われていれば 04 は True を返し、 05 で記述された型通りに互いに等しくなる
ため 05 が refl でコンパイルが通るようになる。
今回は、 pop2 で取れた値を確認するため 03 の後に 031、 032 の二つの作成した。
032 では 03 で扱っている値が Maybe であるため、 031 のような比較をする前に値が確
実に存在していることを示す補題である。 032 を通すことで 031 では 2つの値があり、
かつ$\mathbb{N}$型である事がわかる。 031 では直接取れた値が 2、 1 の順番で入って
いるかを確認している。

この Test でエラーが出なかったことから、 Stack に1、2の二つのデータを pushする
と、 push した値が Stack 上から消えることなく push した順番に取り出せることが分
かる。

また、継続を用いて記述することで関数の Test を書くことで計算途中のデータ内部をチェックするこ
とができた。

ここでの \$ は \( \) をまとめる糖衣構文で、 \$ が書かれた一行を\(\)でくくること
ができる。
% \ref{sintax}のようなコードを
% \begin{lstlisting}[frame=lrbt,label=sintax,caption={ 通常の継続の
%     コード}]

% \end{lstlisting}

% \begin{lstlisting}[frame=lrbt,label=sintax-sugar,caption={ 糖衣構文
%     を用いた継続のコード}]

% \end{lstlisting}

ソースコード~\ref{agda-tree-debug}のように関数本体に記述してデータを返し、C-c C-n
(Compute normal form) で関数を評価すると関数で扱っているデータを見ることができる。
また、途中の計算で受ける変数名を変更し、 Return 時にその変更した変数名に変えるこ
とで、計算途中のデータの中身を確認することができる。評価結果はソースコード内にコメントで記述した。

 \lstinputlisting[label=agda-tree-debug, caption=Agdaにおけるテスト]{src/AgdaTreeDebug.agda}

今回、この手法を用いることで複数の関数を組み合わせた findNode 関数内に異常があるこ
とが分かった。


%getRedBlackTree の関数に
% \lstinputlisting[label=agda-Debug, caption=Agdaにおけるデバッグ]{src/AgdaTreeDebug.agda}
% Tree全然載せてないけどどうしよ。。。どこに書こうかは考えておきましょう


\section{Agda による Interface 部分を含めた Stack の部分的な証明}
\label{agda-interface-stack}

% Stack の仕様記述
Stack や Tree の Interface を使い、 Agda で Interface を 経由した証明が可能であ
ることを示す。
ここでの証明とは Stack の処理が特定の性質を持つことを保証することである。

Stack の処理として様々な性質が存在する。例えば、

\begin{itemize}
 \item Stack に push した値は存在する
 \item Stack に push した値は取り出すことができる
 \item Stack に push した値を pop した時、その値は Stack から消える
 \item どのような状態の Stack に値を push しても中に入っているデータの順序は変わらない
 \item どのような状態の Stack でも、値を push した後 pop した値は直前に入れた値と一致する
\end{itemize}

などの性質がある。

ここでは「どのような状態の Stack でも、値を push した後 pop した値は直前
に入れた値と一致する」という性質を証明する。

まず始めに不定状態の Stack を定義する。ソースコード~\ref{agda-in-some-state}
の stackInSomeState 型は中身の分からない抽象的な Stack を表現している。ソースコー
ド~\ref{agda-in-some-state}の証明ではこのstackInSomeState に対して、 push を
2回行い、 pop2 をして取れたデータは push したデータと同じものになることを証明す
る。

 \lstinputlisting[label=agda-in-some-state, caption=抽象的なStackの定義とpush$->$push$->$pop2 の証明]{src/AgdaStackSomeState.agda}

この証明では stackInSomeState 型の s が抽象的な Stack で、そこに x 、 y の２つのデー
タを push している。また、 pop2 で取れたデータは y1 、 x1 となっていて両方が
Just で返ってくるかつ、 x と x1 、 y と y1 がそれぞれ合同であることが仮定として
型に書かれている。

 この関数本体で返ってくる値は$ x \equiv x1$ と $y \equiv y1$　のため record でまと
めて refl で推論が通る。
これにより、抽象化した Stack に対して push 、 pop を行うと push したものと同じも
のを受け取れることが証明できた。


% \lstinputlisting[label=agda-Test, caption=]{src/AgdaStackTest.agda}

% \section{Agda による Interface 部分を含めた Binary Tree の部分的な証明と課題}
% ここでは Binary Tree の性質の一部に対して証明を行う。
% Binary Tree の性質として挙げられるのは次のようなものである
% % 上の２つはデータ構造として最低限守られるべき部分ではあるがとりあえず書いてる

% \begin{itemize}
%  \item Tree に対して Node を Put することができる。
%  \item Tree に Put された Node は Delete されるまでなくならない。
%  \item Tree に 存在する Node とその子の関係は必ず「右の子 $>$ Node」かつ「Node $>$ 左の子」の関係になっている。
%  \item どのような状態の Tree に値を put しても Node と子の関係は保たれる
%  \item どのような状態の Tree でも値を Put した後、その値を Get すると値が取れる。
% \end{itemize}

% ここで証明する性質は

% ${!!}$ と書かれているところはまだ記述できていない部分で $?$ としている部分である。

% \lstinputlisting[label=agda-tree-proof, caption=Tree Interface の証
% 明]{src/AgdaTreeProof.agda}

% この Tree の証明では、不定状態の Tree を redBlackInSomeState で作成し、その状態の Tree
% に一つ Node を Put し、その Node を Get することができるかを証明しようとしたもの
% である。

% しかし、この証明は Node を取得する際に Put した Node が存在するか、 Get した
% Node が存在するのか、などの条件や、 Get した Node と Put した Node が合同なのか、
% key の値が等しい場合の eq は合同と同義であるのか等の様々な補題を証明する必要が
% あった。今回この証明では Put した Node と Get した
% Node が合同であることを記述しようとしていたがそれまでの計算が異なるため完全に合
% 同であることを示すことが困難であった。

% 今後の研究では\ref{hoare-logic} で説明する Hoare Logic を元に証明を
% 行おうと考えている。

\section{Hoare Logic}
\label{hoare-logic}

Hoare Logic \cite{Hoare1969AnAB} とは Tony Hoare によって提案されたプログラム正
しさを推論する手法である。図\ref{fig:hoare}のように、 P を前状態(Pre Condition)
、C を処理(Command) 、 Q を後状態(Post Condition) とし、$\{P\} \  C  \ \{Q\}$ のように考えたとき、
プログラムの処理を「前状態を満たした後、処理を行い状態が後状態に変化する」といった形で考える事ができる。

\begin{figure}[htpb]
 \begin{center}
  \scalebox{0.3}[0.3]{\includegraphics{pic/hoare-logic.pdf}}
 \end{center}
 \caption{hoare logicの流れ}
 \label{fig:hoare}
\end{figure}


このとき、後状態から前状態を推論することができればそのプログラムは部分的に正しい
動きをすることを証明することができる。

この Hoare Logic の前状態、処理、後状態を CodeGear、 input/output の DataGear が表
\ref{fig:cbc-hoare} のように表せると考えている。

\begin{figure}[htpb]
 \begin{center}
  \scalebox{0.3}[0.3]{\includegraphics{pic/cbc-hoare.pdf}}
 \end{center}
 \caption{cbc と hoare logic}
 \label{fig:cbc-hoare}
\end{figure}

この状態を当研究室で提案している CodeGear、 DataGear の単位で考えると
Pre Condition は CodeGear に入力として与えられる Input DataGear として、
 Command は処理の単位である CodeGear、 Post Condition を Output DataGear として当てはめることができると考える。

 ここでは binary tree での findNode、 replaceNode、 getRedBlackTree の流れを図
 \ref{fig:tree-hoare} で示す。

 \begin{figure}[htpb]
 \begin{center}
  \scalebox{0.3}[0.3]{\includegraphics{pic/funcLoopinAutomata.pdf}}
 \end{center}
 \caption{binary tree での hoare logic の考え方}
 \label{fig:tree-hoare}
\end{figure}

% ここでは key に 1 の入った Node を put する際に内部で動く findNode について考え
% ている。

% findNode では put した key1 と同じ Node が存在するかをループしながら探していく。
% このループ部分で invariant な変数を見つけ、それが findNode の逆の動きをする
% replaceNode で元に戻ることが分かればよい。
% この場合辿った Node は1ループごとに Stack に積まれる。そのため、loop invariant
% は Tree と Stack で共に使っている Node の総数がまとめられた record 型の変数にな
% ると考えている。


今後の研究では CodeGear、 DataGear、継続の概念を Hoare Logic に当てはめ Agda に
当てはめ、幾つかの実装を証明していく。


% Hoare Logic ではプログラムの動作が部分的に正しいことが証明できる。
% 最終的な Stack、Tree の証明は Hoare Logic ベースで行う。
%%
% 部分正当性がプログラムに関する構造機能法によって合成的に証明できるという考えを導
% 入した。
%%

\nocite{*}
\bibliographystyle{ipsjunsrt}
\bibliography{sigos}

\end{document}