\chapter{Continuation based C と Agda} 
\label{c:cbc_agda}
現在 Agda は CbC の上位言語として使用されており、
Agda で記述された CbC のプログラムはメタ計算を含む形で記述される。
しかし、


本章では当研究室で推奨している単位を用いての検証を行うため、
Agda 上で DataGear、 CodeGear の表現を示す。
また、Gear の単位と Hoare Logic を対応させ、
CbC 上での Hoare Logic について示す。



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

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

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

\lstinputlisting[caption= whileTest の型, label=agda-while]{src/while-test.agda.replaced}
%% Agda のとこで Level の話を…！
ここでは \verb/c10/ と名付けた自然数を受け取った後、
\verb/Env/ を受け取って不定の型\verb/t/を返す関数を受け取り、
\verb/t/を返す CodeGear を定義している。


\section{Meta CodeGear の表現と Meta DataGear}
Meta CodeGear は 通常の CodeGear では扱えないメタレベルの計算を扱う CodeGear である。
Agda での Meta CodeGear は通常の CodeGear を引数に取りそれらの関係などの上位概念を返す CodeGear である。
これは(図を入れる)のような Code Gear となる。

% \lstinputlisting[label=src:agda-mcg, caption= Agda における Meta CodeGear 型の定義] {src/MetaCodeGear.agda.replaced}

Meta DataGear については不確かであるが、 DataGear が持つ同値関係や、大小関係などの関係を表す DataGear がそれに当たると考えている。
Agda 上では Meta DataGear を持つことで性質を持ったデータ構造を作ることができる。

% \lstinputlisting[label=src:agda-cs, caption= Agda における CodeGear 型の定義] {src/CodeSegment.agda.replaced}

\section{CbC 上での HoareLogic の実現}
CbC 上の Hoare Logic は引数として事前条件、次の CodeGear に渡す値に事後条件を含めることで記述する。
その際に事前条件が CodeGear で変更され、事後条件を導く形になる。
例として while プログラムの CbC 記述についてみる。


%% コード
ここでは~

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