\documentclass[techrep]{ipsjpapers}
\usepackage[dvipdfmx]{graphicx}

\usepackage{listings}
\usepackage{enumitem}
% \usepackage{bussproofs}
\usepackage{multirow}
\usepackage{here}
\usepackage{ucs}
\usepackage{autofe}
\usepackage{fancyvrb}
\usepackage{ascmac}
\usepackage[deluxe, multi]{otf}
\usepackage{url}
\usepackage{cite}
\usepackage{listings}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{colonequals}
\usepackage[utf8x]{inputenc}

\DeclareUnicodeCharacter{8852}{$\sqcup$}
\DeclareUnicodeCharacter{8909}{$\simeq$}

% \uc@dclc{8852}{default}{\ensuremath{\sqcup}}

\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
% \def<\UTF{2294}>{$\sqcup$}

\begin{document}

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

% 所属ラベルの定義
\affilabel{1}{琉球大学大学院理工学研究科情報工学専攻 \\Interdisciplinary Information Engineering, Graduate Sc k533 hool 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{cbc} (以下CbC)を開発している。
CbC はC言語と似た構文を持つ言語である。
また、 CodeGear、DataGear を用いて信頼性と拡張性をメタレベルで保証する GearsOS\cite{mitsuki:2017} を CbC で開発している。

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

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

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 にそのまま変換されるわけではないが、変換可能なように記述されると仮定する。

以下の節では、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(Code \ref{maybe})はこのdata型の例である。

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

例えば引数が型 \verb+A+ で返り値が型 \verb+B+ の関数は \verb+A -> B+ のように書
ける。
また、複数の引数を取る関数の型は \verb+A -> A -> B+ のように書ける。この
時の型は \verb+A -> (A -> B)+ のように考えられる。
前節に出てきた pushStack の型(Code \ref{push-stack})はこの例である。
pushStack の型の本体は Code \ref{push-stack-func}のようになる。
Code \ref{push-stack-funk} では\verb+\+の表記が出ている。これは$\lambda$式で初め
の pushStack で返した stack である s1 を受け取り、次の関数へ渡している。 Agda の
$\lambda$式では\verb+\+の他に\verb+λ+で表記することもできる。
\verb++

\begin{lstlisting}[caption=pushStack の関数定義,label=push-stack-func]
  pushStack d next = push (stackMethods ) (stack ) d (\s1 -> next (record {stack = s1 ; stackMethods = stackMethods } ))
\end{lstlisting}

ここで書かれている \verb+record+ は C における構造体に相当するレコード型というデー
タを構築しており、 \verb+record+ キーワードの後の {} の内部に \verb+fieldName = value+
の形で値を列挙していく。複数の値を列挙する際は \verb+;+ で区切る必要がある。

定義を行う際は \verb+record+ のキーワード後にレコード名、型、 \verb+where+ の後
に \verb+field+ キーワードを入れ、フィールド名と型名をを列挙する。
\verb+record+ の定義の例として Stack のデータを操作する際に必要なレコード型のデータ
\verb+Element+ (Code \ref{element-impl})を例とする。

\verb+Element+ は単方向のリスト構造になっており、 \verb+datum+ に格納する任意の
型のデータ、\verb+next+ に次のElement型のデータを持っている。

\begin{lstlisting}[caption=Element の定義,label=element-impl]
record Element {l : Level} (a : Set l) : Set l where
  inductive
  constructor cons
  field
    datum : a  -- `data` is reserved by Agda.
    next : Maybe (Element a)
\end{lstlisting}

%% element の定義、縦棒　| の定義
%% SingleLinkedStack の説明に必要なものだけ
% パターンマッチの説明、 | の定義、説明用のあれ。
%% push と pop だけ書いて必要なものだけ説明する
%% testStack08 を説明する。

引数は変数名で受けることもでき、具体的なコンストラクタを指定することでそのコンストラクタが渡された時の挙動を定義できる。
これはパターンマッチと呼ばれ、コンストラクタで case 文を行なっているようなものである。
例として、 popStack の実装である popSingleLinkedStack を使う。

popSingleLinkedStack では \verb+stack+、 \verb+cs+ の2つの引数を取り、
\verb+with+キーワードの後に\verb+Maybe+型の\verb+top+でパターンマッチしている。
\verb+Maybe+型は\verb+nothing+と\verb+Just+のどちらかを返す。そのため、両方のパ
ターンにマッチしている必要がある。
パターンマッチの記述では関数名、引数、を列挙して\verb+|+の後に \verb+パターン名 =+
で挙動を書く場合と、 Code \ref{pattern-match}のように、\verb+... |+で関数名、引数
を省略して\verb+パターン名 =+で挙動を書く方法がある。

また、Agda では特定の関数内のみで利用できる関数を \verb+where+ 句で記述できる。
スコープは \verb+where+ 句が存在する関数内部のみであるため、名前空間が汚染させる
ことも無い。
\verb+where+ 句は利用したい関数の末尾にインデント付きで \verb+where+ キーワード
を記述し、改行の後インデントをして関数内部で利用する関数を定義する。

\begin{lstlisting}[caption=パターンマッチの例,label=pattern-match]
popSingleLinkedStack stack cs with (top stack)
...                                | Nothing = cs stack  Nothing
...                                | Just d  = cs stack1 (Just data1)
  where
    data1  = datum d
    stack1 = record { top = (next d) }
\end{lstlisting}

pushStack と popStack を使った証明の例は Code\ref{push-pop}のようになる。
ここでは、stack に対し push を行なった直後に pop を行うと取れるデータは push し
たものと同じになるという論理式を型に書き、証明を行なった。

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

証明の関数部分に出てきた\verb+refl+は左右の項が等しいことを表す$x \equiv x$を生
成する項であり、$x \equiv x$を証明したい場合には\verb+refl+と書く事ができる。

\begin{lstlisting}[caption=reflectionの定義,label=refl]
data _≡_ {a} {A : Set a} (x : A) : A → Set a where
  refl : x ≡ x
\end{lstlisting}

また、Code \ref{test08}のように継続を用いて記述することで関数の中で計算途中のデー
タ内部を確認することができた。ここでは$\lambda$式のネストになり見づらいため、
\verb+()+をまとめる糖衣構文\verb+$+を使っている。\verb+$+を先頭に書くことで後ろ
の一行を\verb+()+でくくることができる。

Code \ref{test08} のように記述し、\verb+C-c C-n+(Compute nomal form)で関数を評価
すると最後に返している stack の top を確認することができる。top の中身は
Code\ref{test08} の中にコメントとして記述した。
\begin{lstlisting}[caption=継続によるテスト,label=test08]
testStack08 = pushSingleLinkedStack emptySingleLinkedStack 1 
   $ \s -> pushSingleLinkedStack s 2 
   $ \s -> pushSingleLinkedStack s 3 
   $ \s -> pushSingleLinkedStack s 4 
   $ \s -> pushSingleLinkedStack s 5 
   $ \s -> top s

-- Just (cons 5 (Just (cons 4 (Just (cons 3 (Just (cons 2 (Just (cons 1 Nothing)))))))))
\end{lstlisting}



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

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

Stack の実装を以下の Code \ref{stack-impl}で示す。
実装は SingleLinkedStack という名前の\verb+record+で定義されている。

\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 の実装(以下の Code \ref{tree-impl})は Tree という\verb+record+で定義されている。

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

\begin{lstlisting}[caption=Treeの実装,label=tree-impl]
record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where
  field
    putImpl : treeImpl -> a -> (treeImpl -> t) -> t
    getImpl  : treeImpl -> (treeImpl -> Maybe a -> t) -> t

record Tree  {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where
  field
    tree : treeImpl
    treeMethods : TreeMethods {n} {m} {a} {t} treeImpl
  putTree : a -> (Tree treeImpl -> t) -> t
  putTree d next = putImpl (treeMethods ) tree d (\t1 -> next (record {tree = t1 ; treeMethods = treeMethods} ))
  getTree : (Tree treeImpl -> Maybe a -> t) -> t
  getTree next = getImpl (treeMethods ) tree (\t1 d -> next (record {tree = t1 ; treeMethods = treeMethods} ) d )

record Node {n : Level } (a k : Set n) : Set n where
  inductive
  field
    key   : k
    value : a
    right : Maybe (Node a k)
    left  : Maybe (Node a k)
    color : Color {n}
\end{lstlisting}

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

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

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 で列挙し、Code~\ref{agda-interface}のように紐付けることができる。
Agda では型を明記する必要があるため record 内に型を記述している。

例として Agda で実装した Stack 上の interface ( Code \ref{agda-interface})
の一部を見る。
Stack の実装は SingleLinkedStack( Code \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 による Interface 部分を含めた Stack の部分的な証明}
\label{agda-interface-stack}

% Stack の仕様記述
Stack の 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 を定義する。 Code~\ref{agda-in-some-state}
の stackInSomeState 型は引数として \verb+SingleLinkedStack+ 型の \verb+s+を受け
取り新しいレコードを返す関数である。
この関数により、中身の分からない抽象的な Stack を表現している。ソースコー
ド~\ref{agda-in-some-state}の証明ではこの \verb+stackInSomeState+ に対して、
\verb+push+ 操作を2回行い、 \verb+pop+を2回行なって取れたデータは push したデー
タと同じものになることを証明している。

この証明では 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-in-some-state, caption=抽象的なStackの定義とpush$->$push$->$pop2 の証明]{src/AgdaStackSomeState.agda}

しかし、同様の証明を Tree 側で記述した際、 Agda 側で等しいことを認識できず記述が
複雑になっていったため、今後の証明は 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 の単位で考えると
PreCondition は CodeGear に入力として与えられる Input DataGear として、
 Command は処理の単位である CodeGear、 PostCondition を 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}