--- a/paper/akasha.tex	Wed Feb 08 13:50:52 2017 +0900
+++ b/paper/akasha.tex	Wed Feb 08 14:27:06 2017 +0900
@@ -203,4 +203,38 @@
 
 % }}}
 
+% {{{ モデル検査器 CBMC との比較
+
 \section{モデル検査器 CBMC との比較}
+akasha の比較対象として、 C言語の有限モデルチェッカ CBMC\cite{cite:cbmc} を用いて赤黒木を検証した。
+CBMC は ANSI-C を記号実行し、仕様の否定となるような実行パターンが無いかを検証するツールである。
+
+比較のために全く同じ赤黒木のソースコードを用いたいが、CbCの構文は厳密にはCとは異なるために変換が必要である。
+具体的には、\verb/__code/ を \verb/void/ に、 \verb/goto/ を \verb/return/ に置換することで機械的にC言語に変換できる。
+
+CBMC における仕様は bool を返す式として記述するため、akashaと同様の仕様定義が利用できる(リスト\ref{src:cbmc-assert}。
+assert が true になるような実行パターンを CBMC が見付けると、その実行パターンが反例として出力される。
+
+\lstinputlisting[label=src:cbmc-assert, caption=CBMC における仕様記述] {src/cbmc-assert.c}
+
+挿入順の数え上げにはCBMCの機能に存在する非決定的な値 \verb/nondet_int()/ を用いた(リスト\ref{src:enumerate-inputs})。
+この \verb/nondet_int()/ 関数は int の持ちうる値の内から非決定的に値を取得する関数である。
+akasha では有限の要素個分の組み合わせを用いて挿入順の数え上げとしたが、CBMC では要素数回分だけランダムな値を入力させることで数え上げとする。
+
+\lstinputlisting[label=src:enumerate-inputs, caption= CBMC における挿入順の数え上げ] {src/enumerate-inputs.c}
+
+CBMCでは有限のステップ数だけC言語を記号実行し、その範囲内で仕様が満たされるかを確認する。
+条件分岐や繰り返しなどは展開されて実行される。
+基本的にはメモリの許す限り展開を行なうことができるが、今回の赤黒木の検証では411回まで展開することができた。
+この411回のうちの実行パスでは赤黒木の仕様は常に満たされる。
+しかし、この展開された回数は挿入された回数とは無関係であり、実際どの程度検証することができたか確認できない。
+実際、赤黒木に恣意的なバグを追加した際にも仕様の反例は得られず、CBMC で扱える範囲内では赤黒木の性質は検証できなかった。
+
+よって、CBMCでは検証できない範囲の検証を akasha で行なえることが確認できた。
+しかし、要素数13個分の挿入を検証しても赤黒木の挿入が必ずバランスするとは言いづらい。
+より大きな数を扱っても現実的な速度で検証が行なえる必要がある。
+そのためには記号化なので状態の抽象化や、何らかの機構により状態の削減を行なう必要がある。
+CbC における状態の抽象化の内部表現や、状態を削減するための制約として、型に注目した。
+特に、型を値として利用できる
+
+% }}}

Binary file paper/atton-master.pdf has changed

--- a/paper/introduction.tex	Wed Feb 08 13:50:52 2017 +0900
+++ b/paper/introduction.tex	Wed Feb 08 14:27:06 2017 +0900
@@ -9,26 +9,28 @@
 モデル検査とはソフトウェアの全ての状態を数え上げ、その状態について仕様が常に真となることを確認する。
 モデル検査器には Promela と呼ばれる言語でモデルを記述する Spin\cite{spin} や、モデルを状態遷移系で記述する NuSMV\cite{nusmv}、C言語/C++ を記号実行する CBMC\cite{cbmc} などが存在する。
 定理証明はソフトウェアが満たすべき仕様を論理式で記述し、その論理式が恒真であることを証明する。
-定理証明を行なうことができる言語には、依存型証明を行なう Agda\cite{agda} や Coq\cite{coq} 、 ATS2\cite{ats2} などが存在する。
+定理証明を行なうことができる言語には、依存型で証明を行なう Agda\cite{agda} や Coq\cite{coq} 、 ATS2\cite{ats2} などが存在する。
 
 モデル検査器や証明でソフトウェアを検証する際、検証を行なう言語と実装に使われる言語が異なるという問題がある。
 言語が異なれば二重で同じソフトウェアを記述する必要がある上、検証に用いるソースコードは状態遷移系でプログラムを記述するなど実装コードに比べて記述が困難である。
-検証されたコードから実行可能なコードを生成可能な検証系もあるが、既存の実装に対する検証は行なえない。
+検証されたコードから実行可能なコードを生成可能な検証系もあるが、生成されたコードは検証のコードとは別の言語であったり、既存の実装に対する検証は行なえないなどの問題がある。
 そこで、当研究室では検証と実装が同一の言語で行なえる Continuation based C\cite{utah-master} 言語を開発している。
 
 Continuation based C (CbC)はC言語と似た構文を持つ言語である。
 CbC では処理の単位は関数ではなく CodeSegment という単位で行なわれる。
 CodeSegment は値を入力として受け取り出力を行なう処理単位であり、CodeSegment を接続していくことによりソフトウェアを構築していく。
 CodeSegment の接続処理はメタ計算として定義されており、実装や環境によって切り替えを行なうことができる。
-検証を行なうメタ計算を定義することにより、CodeSegment の定義を検証用に変更することなくソフトウェアの検証を行なうことができる。
+検証を行なうメタ計算を定義することにより、CodeSegment の定義を検証用に変更せずソフトウェアの検証を行なう。
 
 本論文では CbC のメタ計算として検証手法の提案と CbC の型システムの定義を行なう。
 モデル検査的な検証として、状態の数え上げを行なう有限のモデル検査と仕様の定義を CbC 自身で行なう。
-また、証明的な検証として CbC における型システムを部分型として定義する。
-部分型を利用して CbC のプログラムが証明支援系言語 Agda 上で正しく証明可能な形で定義できることを示す。
+CbC で記述された GearsOS の非破壊赤黒木に対して、メタ計算ライブラリ akasha を用いて仕様を検査する。
+また、定理証明的な検証として、 CbC のプログラムが証明支援系言語 Agda 上に証明可能な形で定義できることを示す。
+Agda 上で CbC のプログラムを記述するために、CbC の型システムを部分型を利用して定義する。
 
 
 \section{本論文の構成}
+% TODO: もう一回構成しなおし
 本論文ではまず第\ref{chapter:cbc}章で Continuation based C の解説を行なう。
 CbC を記述するプログラミングスタイルである CodeSegment と DataSegment の解説、メタ計算と状態を数え上げるメタ計算ライブラリ akasha の解説を行なう。
 次に第\ref{chapter:type}章で型システムについて取り上げる。

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/cbmc-assert.c	Wed Feb 08 14:27:06 2017 +0900
@@ -0,0 +1,7 @@
+void verifySpecification(struct Context* context,
+                         struct Tree* tree) {
+    assert(!(maxHeight(tree->root, 1) >
+             2*minHeight(tree->root, 1)));
+    return meta(context, EnumerateInputs);
+}
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/enumerate-inputs.c	Wed Feb 08 14:27:06 2017 +0900
@@ -0,0 +1,13 @@
+void enumerateInputs(struct Context* context,
+                     struct Node* node) {
+    if (context->loopCount > LIMIT_OF_VERIFICATION_SIZE) {
+        return meta(context, Exit);
+    }
+
+    node->key     = nondet_int();
+    node->value   = node->key;
+    context->next = VerifySpecification;
+    context->loopCount++;
+
+    return meta(context, Put);
+}

--- a/paper/type.tex	Wed Feb 08 13:50:52 2017 +0900
+++ b/paper/type.tex	Wed Feb 08 14:27:06 2017 +0900
@@ -1,11 +1,19 @@
 \chapter{ラムダ計算と型システム}
 \label{chapter:type}
-\ref{chapter:cbc} では CbC のモデル検査的検証アプローチとして、akasha を用いた有限の要素数の挿入時の仕様の検証を行なった。
+\ref{chapter:akasha} 章では CbC のモデル検査的検証アプローチとして、akasha を用いた有限の要素数の挿入時の仕様の検証を行なった。
+しかし、要素数13個分の挿入を検証しても赤黒木の挿入が必ずバランスするとは断言しづらい。
+
+そこで、 CbC の性質をより厳密に定義し、その上で証明を行なうことを考えた。
+CbC のプログラムを証明できる形に変換し、任意の回数の挿入に対しても性質が保証できるよう証明するのである。
+証明を行なう機構として注目したのが型システムである。
+
+\ref{chapter:type} 章ではCbC の項の形式的な定義の一つとして、部分型を用いて CbC の CodeSegment と DataSegment を定義する。
+また、型システムの別の利用方法として命題が型で表現できる Curry-Howard 対応を利用した証明が存在するが、その利用方法については\ref{chapter:agda}章で述べる。
+
+
 しかし、さらに多くの要素を検証したり無限回の挿入を検証するには状態の抽象化や CbC 側に記号実行の機構を組み込んだり証明を行なう必要がある。
 CbC は直接自身を証明する機構が存在しない。
 プログラムの性質を証明するには CbC の形式的な定義が必須となる。
-\ref{chapter:type} 章ではCbC の項の形式的な定義の一つとして、部分型を用いて CbC の CodeSegment と DataSegment が定義できることを示していく。
-また、型システムの別の利用方法として命題が型で表現できる Curry-Howard 対応を利用した証明が存在するが、その利用方法については\ref{chapter:agda}章で述べる。
 
 % {{{ 型システムとは
 \section{型システムとは}