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

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

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

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

% Stack の仕様記述

Stack 

この証明では任意の Stack に2回 push したあと2回 pop すると push したものと同じものが受け取れる
ことを証明している。

stackInSomeState 型は中身の分からない抽象的な Stack を作成している。リスト
\ref{src:agda-in-some-state}の証明ではこのstackInSomeState に対して、 push を2回
行い、 pop2 をして取れたデータは push したデータと同じものになることを証明してい
る。
% Agda でも継続を使った書き方で Interface 部分の実装を示した。

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

この証明では 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 部分を含めた Tree の部分的な証明}



\section{Hoare Logic}

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

このとき、後状態から前状態を推論することが〜...

Hoare Logic ではプログラムの動作が部分的に正しいことが証明できる。
最終的な Stack、Tree の証明は Hoare Logic ベースで行う。

%%
% 部分正当性がプログラムに関する構造機能法によって合成的に証明できるという考えを導
% 入した。
%%