--- a/paper/cbc.tex	Mon Jan 23 17:19:30 2017 +0900
+++ b/paper/cbc.tex	Mon Jan 23 18:41:23 2017 +0900
@@ -260,6 +260,8 @@
 
 % }}}
 
+% {{{ メタ計算ライブラリ akasha を用いた赤黒木の実装の検証
+
 \section{メタ計算ライブラリ akasha を用いた赤黒木の実装の検証}
 GearsOS の赤黒木の仕様の定義とその確認を CbC で行なっていく。
 赤黒木には以下の性質が求められる。
@@ -303,7 +305,20 @@
 \lstinputlisting[label=src:get-min-height, caption=木の最も短かい経路の長さを確認する Meta CodeSegment] {src/getMinHeight.c}
 
 同様に最も高い高さを取得し、仕様であるリスト\ref{src:assert}の assert を挿入の度に実行する。
+assert は CodeSegment の結合を行なうメタ計算である \verb/meta/ を上書きすることにより実現する。
+\verb/meta/ はリスト\ref{src:rbtree-insert-case-2}の \verb/insertCase2/ のように軽量継続を行なう際に CodeSegment 名と DataSegment を指定するものである。
+検証を行なわない通常の \verb/meta/ の実装は CodeSegment 名から対応する実体への軽量継続である(リスト\ref{src:meta})。
 
+\lstinputlisting[label=src:meta, caption=通常の CodeSegment の軽量継続] {src/meta.c}
 
-% TODO: meta の定義
-% TODO: akasha の結果
+これを、検証を行なうように変更することで \verb/insertCase2/ といった赤黒木の実装のコードを修正することなく検証を行なうことができる。
+検証を行ないながら軽量継続する \verb/meta/ はリスト\ref{src:akasha-meta}のように定義される。
+実際の検証部分は \verb/PutAndGoToNextDepth/ の後に行なわれるため、直接は記述されていない。
+この \verb/meta/ が行なうのは検証用にメモリの管理である。
+状態の数え上げを行なう際に状態を保存したり、元の状態に戻す処理が行なわれる。
+このメタ計算を用いた検証では、要素数13個までの任意の順で挿入の際に仕様が満たされることを確認できた。
+また、赤黒木の処理内部に恣意的なバグを追加した際には反例を返した。
+
+\lstinputlisting[label=src:akasha-meta, caption=検証を行なう CodeSegment の軽量継続] {src/akashaMeta.c}
+
+% }}}