Binary file paper/vmpcbc.pdf has changed

--- a/paper/vmpcbc.tex	Wed Jul 06 16:41:18 2016 +0900
+++ b/paper/vmpcbc.tex	Wed Jul 06 17:59:13 2016 +0900
@@ -7,10 +7,10 @@
 \usepackage{listings}
 \lstset{
   language={C},
-  basicstyle={\small},
-  commentstyle={\small\itshape},
-  keywordstyle={\small\bfseries},
-  stringstyle={\small},
+  basicstyle={\scriptsize},
+  commentstyle={\scriptsize\itshape},
+  keywordstyle={\scriptsize\bfseries},
+  stringstyle={\scriptsize},
   frame={trlb},
   breaklines=true,
   columns=[l]{fullflexible},
@@ -35,8 +35,6 @@
 %\再再受付{2015}{7}{20} %省略可能
 \採録{2015}{8}{1}
 
-% TODO lstlisting のcaptionの修正
-
 
 \begin{document}
 
@@ -389,11 +387,10 @@
 親の色が黒である場合は木が平衡であるために処理を終了し、ユーザ側のCode Segment へと \verb/goto/ する。
 親の色が赤である場合は経路情報を再現するためにスタックへと親を挿入し、次の条件判定へと \verb/goto/ する。
 
-% {{{ 赤黒木の赤が続かないという制約の判定
+% {{{ 赤黒木で赤のノードが続かないという制約の判定
 
 \begin{table}[ht]
 \begin{lstlisting}
-
 // Meta Code Segment
 __code insertCase2(struct Context* context, struct Node* current) {
     struct Node* parent;
@@ -411,7 +408,7 @@
     goto insertCase2(context, context->data[Traverse]->traverse.current);
 }
 \end{lstlisting}
-\caption{赤黒木の赤が続かないという制約の判定}
+\caption{赤黒木で赤のノードが続かないという制約の判定}
 \label{src:rbtree}
 \end{table}
 
@@ -421,15 +418,20 @@
 赤黒木を利用する Code Segment からは赤黒木の処理は意識する必要がないため、赤黒木の処理はMeta Code Segment のように見え、赤黒木のメモリ管理は Meta Meta Code Segment と考えられる。
 このようにメタ計算は階層構造を持つため、任意の Code Segment に対してメタ計算を適用することが可能である。
 
-\section{メタ計算を用いたデータ構造の性質の検証}
-CbC で記述された赤黒木と、それに対する処理の性質を実際に検証する。
-また、非破壊であるため木にデータを挿入、削除した際に過去の木は変更されない。
-非破壊赤黒木に求められる性質には、挿入したデータを参照できること、削除できること、値の更新ができること、操作を行なった後の木はバランスしていること、などが存在する。
-本論文では任意の順番で木に要素を挿入しても木がバランスしていることを検証する。
+\section{メタ計算を用いた赤黒木の検証}
+CbC で記述された赤黒木と、それに対する処理の性質を実際に検証していく。
+非破壊赤黒木に求められる性質には以下のようなものがある
+\begin{itemize}
+    \item 挿入したデータを参照できるこ
+    \item 挿入したデータを削除できること
+    \item 挿入したデータの値の更新ができること
+    \item 操作を行なった後の木はバランスしていること
+\end{itemize}
 
-まず、検証を行なうために満たすべき仕様を定義する。
-仕様はデータ構造が常に満たすべき論理式として表現し、CbC のコードで記述する。
-検証する仕様として、とを CbC で定義する(表\ref{src:specification})。
+本論文では操作を挿入に限定し、任意の順で木に要素を挿入しても木がバランスすることを検証する。
+検証には当研究室で開発している検証用メタ計算ライブラリ akasha を用いる。
+akasha では仕様を Meta Code Segment として記述するため、CbCで常に真となるべき式として定義する
+赤黒木の性質である、 木をルートから辿った際に最も長い経路は最も短い経路の高々2倍に収まることをCbCのコードで記述する(表\ref{src:specification})。
 
 % {{{ 木の高さの仕様記述
 
@@ -447,15 +449,125 @@
 % }}}
 
 表\ref{src:specification}で定義した仕様に対し、挿入する値と順番の全ての組み合わせに対して確認していく。
-また、仕様を満たさない反例が存在する場合はその具体的な組み合わせの値を出力する。
+無限回の挿入順番を数え上げることは状態の抽象化無しには不可能なので、限られた要素数の挿入を検証する。
+検証の対象である赤黒木を内包する Meta Data Segment を定義し、挿入順の検証に必要なデータを追加で定義する(表\ref{src:akashaDs})。
+必要なデータには挿入順の数え上げに使う環状リスト \verb/Iterator/ とその要素 \verb/IterElem/、検証に使う情報を保持する \verb/AkashaInfo/、木をなぞる際に使う \verb/AkashaNode/がある。
+
+% {{{ akasha の Data Segment
+\begin{table}[ht]
+\begin{lstlisting}
+// Data Segment
+union Data {
+    struct Tree { /* ... */ } tree;
+    struct Node { /* ... */ } node;
+
+    /* for verification */
+    struct IterElem {
+        unsigned int val;
+        struct IterElem* next;
+    } iterElem;
+    struct Iterator {
+        struct Tree* tree;
+        struct Iterator* previousDepth;
+        struct IterElem* head;
+        struct IterElem* last;
+        unsigned int  iteratedValue;
+        unsigned long iteratedPointDataNum;
+        void*         iteratedPointHeap;
+    } iterator;
+    struct AkashaInfo {
+        unsigned int minHeight;
+        unsigned int maxHeight;
+        struct AkashaNode* akashaNode;
+    } akashaInfo;
+    struct AkashaNode {
+        unsigned int       height;
+        struct Node*       node;
+        struct AkashaNode* nextAkashaNode;
+    } akashaNode;
+};
+\end{lstlisting}
+\caption{akasha の Data Segment}
+\label{src:akashaDs}
+\end{table}
+
+% }}}
+
+挿入順の数え上げには深さ優先探索を用いるが、CbCスタックフレームが無いために再帰では記述できず、データ構造に今の状態を保持させながら探索する必要がある。
+検証する要素を全て持つ環状リストを作成し、木に一度挿入する度に環状リストを複製する。
+複製を行なった際に挿入した要素を削除し、全ての要素が無くなることで1つの挿入順の探索を終了する。
+1つの挿入順を列挙後、前の深さの環状リストを再現し、環状リストの先頭を進めることで次の組み合わせを列挙していく。
+
+挿入順を列挙しつつ、木に要素を挿入する度に表\ref{src:specification}の仕様が満たされているか Code Segment を実行して確認する。
+仕様には木の高さが含まれるため、その値を取得する Meta Code Segment が必要である(表\ref{src:getMiHeight})。
+
+% {{{ 木の最も低い高さを取得する Code Segment
 
-当研究室で開発している検証用メタ計算ライブラリ akasha と、C言語の有限モデルチェッカ CBMC\cite{cite:cbmc} を用いてこの仕様を検証した。
--
+\begin{table}[ht]
+\begin{lstlisting}
+__code getMinHeight(struct Context* context,
+                    struct AkashaNode* left,
+                    struct AkashaNode* right,
+                    struct AkashaInfo* ai) {
+    const struct AkashaNode* an = ai->akashaNode;
+
+    if (an == NULL) {
+        ai->akashaNode->height = 1;
+        ai->akashaNode->node   = context->data[Tree]->tree.root;
+
+        goto getMaxHeight_stub(context);
+    }
+
+    const struct Node* n = ai->akashaNode->node;
+    if (n->left == NULL && n->right == NULL) {
+        if (ai->minHeight > an->height) {
+            ai->minHeight  = an->height;
+            ai->akashaNode = an->nextAkashaNode;
+            goto getMinHeight_stub(context);
+        }
+    }
+
+    ai->akashaNode = ai->akashaNode->nextAkashaNode;
+
+    if (n->left != NULL) {
+        left->height           = an->height+1;
+        left->node             = node->left;
+        left->nextAkashaNode   = ai->akashaNode;
+        ai->akashaNode = left;
+    }
+
+    if (n->right != NULL) {
+        right->height            = an->height+1;
+        right->node              = node->right;
+        right->nextAkashaNode    = ai->akashaNode;
+        ai->akashaNode   = right;
+    }
+
+    goto getMinHeight_stub(context);
+}
+\end{lstlisting}
+\caption{木の最も低い高さを取得する Code Segment}
+\label{src:getMinHeight}
+\end{table}
+
+% }}}
+
+木をなぞるためのスタックに相当する \verb/AkashaNode/ を用いてノードを保持しつつ、高さを確認している。
+スタックが空であれば全てのノードをなぞったので最も高い高さを取得するために \verb/goto/する。
+空でなければ今なぞっているノードが葉であるか確認し、葉ならば高さを更新し、スタックからノードを1つ破棄して自身に \verb/goto/する。
+葉でなければ高さを1つ増やしながらスタックに左右の子供を積み、自身に \verb/goto/ する。
+
+このように、Code Segment の検証に必要な仕様や処理は Code Segment で記述することができる。
+akasha におけるメタ計算を用いて、要素数13個まで任意の順で挿入を行なっても仕様が満たされることを検証した。
+
+% writing...
+\section{CBMC を用いた赤黒木の検証}
+C言語の有限モデルチェッカ CBMC\cite{cite:cbmc} を用いてこの仕様を検証した。
+
 akasha では検証用の仕様と検証用の処理をMeta Code Segmentに定義する。
 挿入順の数え上げには深さ優先探索を用いる。
 CbCには関数呼び出しが存在しないため、深さ優先探索を行なう際にスタックフレームに相当するMeta Data Segmentを自ら用意する。
 各深さ毎の木を保存しておくことで、ある深さまでの探索が終了した際に木を再現ことができ、高速に探索を行なうことができる。
-要素数13個までは任意の順で挿入を行なっても仕様が満たされることをakasha を用いて検証した。
 また、赤黒木の処理内部にバグを追加した際にはakashaは反例を返した。
 
 同じ仕様をC言語の有限モデルチェッカCBMCで検証する。