\chapter{Agda による CbC の証明}

前章では Agda で CodeGear や DataGear の定義を示した。また、 CbC のコード
を Agda にマッピングし等価なコードを生成できることを示した。
本章では前章で生成した Interface の Stack や Tree のコードを使い Agda で
Interface を経由したコードでの証明が可能であることを示す。

% Hoare Logic ベースで証明をすすめる〜みたいなとこをどっかにいれたい。
% ↑ 上は Tree のコードが証明できないことを示して、その次の章に Hoare Logic でこ
% んな感じにするとできるのでは？っていう感じにしよ

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

% Stack の仕様記述
ここでの証明とは 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 に2回 push したあと2回 pop すると push したものと同じ
% ものが受け取れることを 証明している。

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

 \lstinputlisting[label=src:agda-in-some-state, caption=抽象的なStackの定義とpush$->$push$->$pop2 の証明]{src/AgdaStackSomeState.agda.replaced}
 
% Agda でも継続を使った書き方で Interface 部分の実装を示した。

この証明では 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=src:agda-Test, caption=]{src/AgdaStackTest.agda.replaced}

\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=src:agda-tree-proof, caption=Tree Interface の証
明]{src/AgdaTreeProof.agda.replaced}

この 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.6}[0.6]{\includegraphics{fig/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.8}[0.8]{\includegraphics{fig/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 として当てはめることができると考えて
いる。

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

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