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

先行研究\ref{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/ を返す関数となる。
コード \ref{agda-while} は Agda で記述した CodeGear の例である。

\lstinputlisting[caption= whileTest の型, label=agda-while]{src/while-test.agda.replaced}

型では \verb/c10/ と名付けた自然数を受け取った後、
\verb/Env/ を受け取り不定の型\verb/t/を返す関数を受け取り、
最終的に \verb/t/を返す CodeGear を定義しており、

実装では、自然数 \verb/c10/ と継続先の関数 \verb/next/ を受け取り、\verb/next/ に値を代入した Env を引数として渡している。

\section{Meta Gears の表現}
通常の Meta Gears はノーマルレベルの CodeGear、 DataGear では扱えないメタレベルの計算を扱う CodeGear である。
検証での Meta DataGear は、 DataGear が持つ同値関係や、大小関係などの関係を表す DataGear がそれに当たると考えている。
Agda 上では Meta DataGear を持つことで性質を持ったデータ構造を作ることができる。

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

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

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


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


%% コード
ここでは~

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