Binary file paper/fig/nondestructive_tree_modification.pdf has changed

Binary file paper/vmpcbc.pdf has changed

--- a/paper/vmpcbc.tex	Wed Jul 06 16:16:36 2016 +0900
+++ b/paper/vmpcbc.tex	Wed Jul 06 16:41:18 2016 +0900
@@ -171,7 +171,7 @@
 
 \begin{figure}[htbp]
     \begin{center}
-        \includegraphics[scale=0.5]{fig/meta_code_segment_and_meta_data_segment.pdf}
+        \includegraphics[scale=0.45]{fig/meta_code_segment_and_meta_data_segment.pdf}
         \caption{Meta Code Segment と Meta Data Segment}
         \label{fig:metaCSDS}
     \end{center}
@@ -186,6 +186,7 @@
 CbC におけるCode SegmentはC言語における関数に、関数呼び出しが末尾のみである制約を加えようなものである。
 Code Segmentどうしの接続は goto による軽量継続で表される(表\ref{src:simpleCs})。
 軽量継続とは呼び出し元の環境を持たずに次の処理へと移動することであり、呼び出し元のスタックフレームを破棄しながら関数呼び出しを行なうようなものである。
+なお、C言語の資産を利用するために通常の関数呼び出しを行なうことも可能である。
 
 % {{{ Code Segment の接続(10加算して2倍する)
 \begin{table}
@@ -272,7 +273,6 @@
 
 \begin{table}[ht]
 \begin{lstlisting}
-
 // Meta Data Segment
 struct Context {
     union Data *data;  // Data Segment
@@ -330,14 +330,59 @@
 
 赤黒木の実装として、当研究室で CbC を用いて開発している Gears OS \cite{cite:gears-os} における非破壊赤黒木がある。
 非破壊赤黒木とは木への挿入や削除を行なった際に一度構築した木構造を破壊することなく新しく木構造を生成する赤黒木である。
-非破壊赤黒木の実装の基本的な戦略は、変更したいノードへのルートノードからの経路を全て複製し、上に存在しないノードは変更前元の木構造と共有することで実現できる。
+非破壊赤黒木の実装の基本的な戦略は、変更したいノードへのルートノードからの経路を全て複製し、上に存在しないノードは変更前元の木構造と共有することで実現できる(図\ref{fig:tree})。
 
-%TODO figure
+\begin{figure}[ht]
+    \begin{center}
+        \includegraphics[scale=0.4]{fig/nondestructive_tree_modification.pdf}
+        \caption{非破壊赤黒木の編集}
+        \label{fig:tree}
+    \end{center}
+\end{figure}
 
 関数呼び出しが可能な言語では戻り値で経路を辿ることか可能だが、CbC はgotoによる軽量継続のみで記述する必要があるため、経路を辿るにはノードに親への参照を持たせるか挿入・削除時に辿った経路を記憶するしかない。
 ノードが親への参照を持つ非破壊木構造は構築出来ないため、辿った経路を記憶する方法を用いる。
-辿った経路を記憶するため Meta Data Segment にスタックを持たせる。
-このスタックは軽量継続ではなく関数呼び出しで利用する。
+辿った経路を記憶するため Meta Data Segment にスタックを持たせる(表\ref{src:stack}における Context)。
+なお、このスタックは軽量継続ではなく関数呼び出しで利用している。
+赤黒木で利用する Data Segment を表\ref{src:stack}に表す。
+Data Segment は各ノードの情報を持つ \verb/Node/ と赤黒木を格納する \verb/Tree/と、挿入などの操作中の一時的な木を持つ\verb/Traverse/の共用体で表される。
+
+% {{{ 赤黒木の Data Segment
+
+\begin{table}[ht]
+\begin{lstlisting}
+// Data Segment for Red-Black Tree
+union Data {
+    struct Tree {
+        struct Node* root;
+    } tree;
+    struct Traverse {
+        struct Node* current;
+        int result;
+    } traverse;
+    struct Node {
+        int key;
+        union Data* value;
+        struct Node* left;
+        struct Node* right;
+        enum Color {
+            Red,
+            Black,
+        } color;
+    } node;
+};
+
+// Meta Data Segment
+struct Context {
+    stack_ptr node_stack;
+    union Data **data;
+};
+\end{lstlisting}
+\caption{赤黒木の Data Segment}
+\label{src:stack}
+\end{table}
+
+% }}}
 
 赤黒木の赤が続かないという制約をチェックする Code Segment は表\ref{src:rbtree}のようになる。
 まず、親の情報が必須なために経路を記憶しているスタックから親の情報を取得する。
@@ -374,8 +419,7 @@
 
 ここで、赤黒木に対する処理を Code Segment とした場合、赤黒木のメモリ管理などは Meta Code Segment である。
 赤黒木を利用する Code Segment からは赤黒木の処理は意識する必要がないため、赤黒木の処理はMeta Code Segment のように見え、赤黒木のメモリ管理は Meta Meta Code Segment と考えられる。
-このようにメタ計算は階層構造を持つため、任意の Code Segment に対してメタ計算を適用することが可能であり、検証機構の検証なども行なうことができる。
-
+このようにメタ計算は階層構造を持つため、任意の Code Segment に対してメタ計算を適用することが可能である。
 
 \section{メタ計算を用いたデータ構造の性質の検証}
 CbC で記述された赤黒木と、それに対する処理の性質を実際に検証する。
@@ -445,6 +489,7 @@
 \bibitem{cite:cbmc} Clarke, Edmund and Kroening, Daniel and Lerda, Flavio: A Tool for Checking {ANSI-C} Programs, Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004)
 \bibitem{cite:agda} \verb/The Agda Wiki - Agda/ \urlj{http://wiki.portal.chalmers.se/agda/pmwiki.php} \refdatej{2016-07-05}.
 \bibitem{cite:monad} Moggi, Eugenio: Notions of Computation and Monads, Inf. Comput (1991).
+% kkb さん
 
 \end{thebibliography}