\chapter{Continuation based C と Agda} 
\label{c:cbc_agda}
現在 CbC では検証用の上位言語として Agda を利用しており、
Agda では CbC のプログラムをメタ計算を含む形で記述することができる。

先行研究\cite{atton-master} では CbC と Agda を対応させるための型付けが行われているが、
ここでは、その型付けは使わず、前段階である Agda での記述のみで説明を行う。

本章では当研究室で推奨している単位での検証を行うために、
Agda で DataGear、 CodeGear を表現し、
これらの単位を用いた検証を行う事ができることを示す。

\section{DataGear、 CodeGear と Agdaの対応}
Agda での DataGear は Agda で使うことのできるすべてのデータに対応する。
また、Agda での記述はメタ計算として扱われるので、
Context を通すことなくそのまま扱う。

CodeGear は DataGear を受け取って処理を行い DataGear を返す。
また、CodeGear 間の移動は継続を用いて行われる。
継続は関数呼び出しとは異なり、呼び出した後に元のコードに戻らず、
次の CodeGear へ継続を行うものであった。

これは、関数型プログラミングでは末尾関数呼び出しを行うことに相当し、
継続渡し(Continuation Passing Style) で書かれた Agda の関数と対応する。
継続は不定の型 (\verb/t/) を返す関数で表される。
継続先は次に実行する関数の型を引数として受け取り不定の型\verb/t/を返す関数として記述され、
CodeGear 自体も同じ型 \verb/t/ を返す関数となる。

\coderef{agda-cg} は Agda で記述した加算を行う CodeGear の例である。

\lstinputlisting[caption= Agdaでの CodeGear の例, label=agda-cg]{src/cbc-agda.agda.replaced}

\verb/plus 10 20/ を評価すると \verb/next/ に 30 が入力されていることがわかる。


\section{Meta Gears の表現}
\label{s:meta-gears}
通常の Meta Gears はノーマルレベルの CodeGear、 DataGear では扱えないメタレベルの計算を扱う単位である。
Meta DataGear はメタ計算で使われる DataGear で、実行するメタ計算によって異なる。
検証での Meta DataGear は、 DataGear が持つ同値関係や、大小関係などの関係を表す DataGear がそれに当たると考えられる。
Agda 上では Meta DataGear を持つことでデータ構造自体が関係を持つデータを作ることができる。
\coderef{agda-mdg} は While Program での制約条件をまとめたものである。

\lstinputlisting[label=agda-mdg, caption= Agda における Meta DataGear] {src/agda-mdg.agda.replaced}

ここでは \verb/whileTestState/ で Meta DataGear を識別するためのデータを分け、
\verb/whileTestStateP/ でそれぞれの Meta DataGear を返している。
ここでは \verb/(vari env ≡ 0) /\ (varn env ≡ c10 env)/ などのデータを Meta DataGear として扱う。

%% \coderef{agda-mdg} は大小関係を持った Tree 型データ構造の例である。

%% \lstinputlisting[label=agda-mdg, caption= Agda における Meta DataGear] {src/tree.agda.replaced}

%% \verb/nomal-tree/ データ型では leaf か node で別れていて、 node には左右として\verb/nomal-tree/型を再帰的に保持している。この \verb/nomal-tree/ でデータの順序等を考える場合はデータを構築する関数側で成約を考えたプログラムを記述する必要がある。

%% \verb/meta-tree/では node が左右の \verb/meta-tree/ を持っているところまでは同じだが、
%% node の場合に暗黙的な変数として \verb/l/ \verb/r/ という自然数を持っており、
%% 成約として \verb/l/ $\leq$ \verb/key/、\verb/key/ $\leq$ \verb/r/ のデータの関係を受け取る。

%% 付帯した制約が守られなければエラーとなるため、より信頼性の高いデータとなる。


Meta CodeGear は 通常の CodeGear では扱えないメタレベルの計算を扱う CodeGear である。
Agda での Meta CodeGear は Meta DataGear を引数に取りそれらの関係を返す CodeGear である。

メタ計算で検証を行う際の Meta CodeGear は Agda で記述した CodeGear の検証そのものである。
例として \coderef{agda-mcg} を示す。

\lstinputlisting[label=agda-mcg, caption= Agda における Meta CodeGear] {src/agda-mcg.agda.replaced}

\verb/whileTestPwP/ は Meta CodeGear の例である。
ここでは Meta DataGear に \verb/mdg/ という名前をつけてある。
この Meta CodeGear では次の CodeGear に mdg を渡しており、
CodeGear 内で Meta DataGear の性質が正しいことを検証して次の CodeGear に遷移することがわかる。

Meta CodeGear はこのような形で記述される。


%% \section{CbC 上での HoareLogic の実現}
%% CbC 上の Hoare Logic は引数として事前条件、次の CodeGear に渡す値に事後条件を含めることで記述する。
%% その際に事前条件が CodeGear で変更され、事後条件を導く形になる。
%% CbC 上でも While Program を実装し、Hoare Logic ベースの検証を行う。
%% まずは、Condition について確認する。
%% \coderef{cbc-condition} は While Program の Condition を記述したものである。
%% \lstinputlisting[label=cbc-condition, caption= CbC ベースの Hoare Logic] {src/cbc-condition.agda.replaced}

%% \verb/whileTestStateP/ では \verb/s1/ が初期状態、 \verb/s2/ がループ内不変条件、　\verb/fs/ が最終状態に対応している。

%% これらの Condition を用いて While Program の CbC 記述を行う。

%% \coderef{cbc-hoare} は while Program の CbC 記述である。

%% \lstinputlisting[label=cbc-hoare, caption= CbC ベースの Hoare Logic] {src/cbc-hoare.agda.replaced}

%% \verb/whileTestPCallwP'/ が \coderef{}

%%  Hoare Logic の記述を行い、部分的な整合性を示すことができている。
%% 全体の検証を行うためには接続されているすべての CodeGear が実行されたときの健全性(Soundness)が担保される必要がある。
%% そのため、検証用の Meta CodeGear を記述する。
%% 例として while プログラムの健全性を担保するプログラムをみる。
%% %% コード
%% このコードでは CodeGear をつなげて終了状態まで実行したとき最後の事後条件が成り立っているため、これらの実行が正しく終了することを示すことができる。