Binary file paper/vmpcbc.pdf has changed

--- a/paper/vmpcbc.tex	Fri Jul 08 13:01:16 2016 +0900
+++ b/paper/vmpcbc.tex	Fri Jul 08 15:31:10 2016 +0900
@@ -63,7 +63,7 @@
 CbC を用いることによりメタ計算は CbC の Code Segment 間に Meta Code Segment を挟むという単純な方法で実現できる。
 そして、通常計算との切り替えも簡単に行うことができる。
 ここでは、赤黒木を実際の例題として検証した。
-比較対象としてANSI-Cの記号実行を行うCBMC\cite{cite:cmbc}でも検証する。
+比較対象としてANSI-Cの記号実行を行うCBMCでも検証する。
 CBMCよりも広い範囲の検査が行えることを確認した。
 \end{abstract}
 
@@ -141,13 +141,13 @@
 Code SegmentとData Segmentを用いたプログラミングスタイルで記述する言語として Continuation based C\cite{cite:cbc-clang} を作成した。
 Continuation based C (以下 CbC)はOSや組込みシステムなどの記述を行なうことを目標に作られた、アセンブラとC言語の中間のような言語である。
 CbC におけるCode SegmentはC言語における関数に、関数呼び出しが末尾のみである制約を加えたものである。
-Code Segmentどうしの接続は goto による軽量継続で表される(表\ref{src:simpleCs})。
+Code Segmentどうしの接続は goto による軽量継続で表される(図\ref{src:simpleCs})。
 軽量継続とは呼び出し元の環境を持たずに次の処理へと移動することであり、呼び出し元のスタックフレームを破棄しながら関数呼び出しを行なうようなものである。
 なお、C言語の資産を利用するために関数呼び出しを行なうことも可能である。
 また、Code Segment のみが導入されたCbCで検証を行った例として Dining Philosophers Problem のデッドロック検知\cite{cite:dpp}がある。
 
 % {{{ Code Segment の接続(10加算して2倍する)
-\begin{table}
+\begin{figure}[ht]
 \begin{lstlisting}
 __code addTen(int a) {
     int b = a+10;
@@ -158,24 +158,24 @@
     int y = 2*x;
     goto showValue(y);
 }
+\end{lstlisting}
 
-\end{lstlisting}
 \caption{Code Segment の接続(10加算して2倍する)}
 \label{src:simpleCs}
-\end{table}
+\end{figure}
 % }}}
 
 CbCにおけるCode Segmentは、C言語の関数宣言の返り値の型の部分に \verb/__code/ を記述して定義する。
 Code Segment内部には変数の宣言やif文による分岐といったC言語の文法を用いて処理を記述する。
-表\ref{src:simpleCs}の例では、\verb/addTen/ と \verb/twice/という2つのCode Segmentを定義している。
+図\ref{src:simpleCs}の例では、\verb/addTen/ と \verb/twice/という2つのCode Segmentを定義している。
 \verb/addTen/では int の値を受けとり、10加算して \verb/twice/ を実行する。
 \verb/twice/ では受けとったintの値を2倍して \verb/showValue/ を実行する。
 
 また、CbCにおけるData SegmentはC言語における構造体と共用体を用いたデータ構造である。
-各Code Segmentで必要な値を構造体で定義し、それらの共用体としてData Segmentを定義する(表\ref{src:simpleDs})。
+各Code Segmentで必要な値を構造体で定義し、それらの共用体としてData Segmentを定義する(図\ref{src:simpleDs})。
 
 % {{{ Data Segment の例
-\begin{table}[ht]
+\begin{figure}[ht]
 \begin{lstlisting}
 union Data {
     struct Count {
@@ -188,18 +188,18 @@
 \end{lstlisting}
 \caption{Data Segmentの例}
 \label{src:simpleDs}
-\end{table}
+\end{figure}
 % }}}
 
-表\ref{src:simpleDs}ではData Segmentとして int を持つ count と unsigned int を持つ port の2つを定義している。
+図\ref{src:simpleDs}ではData Segmentとして int を持つ count と unsigned int を持つ port の2つを定義している。
 
 Code Segment 内部ではポインタ演算は行なわず、メタ計算でポインタへの演算を行なう。
 これにはメモリ管理をメタ計算部分に分離することで、プログラムを検証しやすくするねらいがある。
-Code Segment がどの Data Segment にアクセスするかといった指定も Meta Code Segment で行なう(表\ref{src:stub} における \verb/twice_stub/)。
+Code Segment がどの Data Segment にアクセスするかといった指定も Meta Code Segment で行なう(図\ref{src:stub} における \verb/twice_stub/)。
 CbC における Meta Code Segment は Code Segment と Code Segment 間に存在する Code Segment である。
 
 % {{{ Data Segment を指定する Meta Code Segment
-\begin{table}[ht]
+\begin{figure}[ht]
 \begin{lstlisting}
 // Code Segment
 __code addTen(union Data* ds, int a) {
@@ -220,17 +220,17 @@
 \end{lstlisting}
 \caption{Data Segment を指定する Meta Code Segment}
 \label{src:stub}
-\end{table}
+\end{figure}
 
 % }}}
 
-CbC における Meta Data Segment は Data Segment を内包する構造体として定義できる(表\ref{src:meta} の Context)。
-また、goto する際に必ず通る Meta Code Segment を定義することで、 Code Segment どうしの接続もメタ計算として定義できる(表\ref{src:meta} の \verb/meta/)。
+CbC における Meta Data Segment は Data Segment を内包する構造体として定義できる(図\ref{src:meta} の Context)。
+また、goto する際に必ず通る Meta Code Segment を定義することで、 Code Segment どうしの接続もメタ計算として定義できる(図\ref{src:meta} の \verb/meta/)。
 \verb/meta/ を切り替えることで Code Segment を変更することなくメタ計算のみを変更することができる。
 
 % {{{ メタ計算を用いてCode Segment を接続する例
 
-\begin{table}[ht]
+\begin{figure}[ht]
 \begin{lstlisting}
 // Meta Data Segment
 struct Context {
@@ -269,7 +269,7 @@
 \end{lstlisting}
 \caption{メタ計算を用いてCode Segment を接続する例}
 \label{src:meta}
-\end{table}
+\end{figure}
 
 % }}}
 
@@ -305,13 +305,13 @@
 
 関数呼び出しが可能な言語では再起呼び出しで木を辿ることか可能だが、CbC は \verb/goto/による軽量継続のみで記述する必要があるため、経路を辿るにはノードに親への参照を持たせるか挿入・削除時に辿った経路を記憶するしかない。
 ノードが親への参照を持つ非破壊木構造は構築出来ないため、辿った経路を記憶する方法を用いる。
-辿った経路を記憶するため Meta Data Segment にスタックを持たせる(表\ref{src:stack}における Context 内部の \verb/node_stack/)。
-赤黒木で利用する Data Segment を表\ref{src:stack}に表す。
+辿った経路を記憶するため Meta Data Segment にスタックを持たせる(図\ref{src:stack}における Context 内部の \verb/node_stack/)。
+赤黒木で利用する Data Segment を図\ref{src:stack}に表す。
 Data Segment は各ノードの情報を持つ \verb/Node/ と赤黒木を格納する \verb/Tree/と、挿入などの操作中の一時的な木を持つ\verb/Traverse/の共用体で表される。
 
 % {{{ 赤黒木の Data Segment
 
-\begin{table}[ht]
+\begin{figure}[ht]
 \begin{lstlisting}
 // Data Segment for Red-Black Tree
 union Data {
@@ -342,18 +342,18 @@
 \end{lstlisting}
 \caption{赤黒木の Data Segment}
 \label{src:stack}
-\end{table}
+\end{figure}
 
 % }}}
 
-CbCによる赤黒木実装の例として、赤が続かないという制約をチェックする Code Segment を表\ref{src:rbtree}に示す。
+CbCによる赤黒木実装の例として、赤が続かないという制約をチェックする Code Segment を図\ref{src:rbtree}に示す。
 まず、赤が連続するか判定するために親の情報が必須なため、経路を記憶しているスタックから親の情報を取得する。
 親の色が黒である場合は木が平衡であるために処理を終了し、ユーザ側のCode Segment へと \verb/goto/ する。
 親の色が赤である場合は次の条件判定へと \verb/goto/ するが、経路情報を再現するためにスタックへと親を再度挿入しつつ \verb/goto/ する。
 
 % {{{ 赤黒木で赤のノードが続かないという制約の判定
 
-\begin{table}[ht]
+\begin{figure}[ht]
 \begin{lstlisting}
 // Meta Code Segment
 __code insertCase2(struct Context* context, struct Node* current) {
@@ -374,7 +374,7 @@
 \end{lstlisting}
 \caption{赤黒木で赤のノードが続かないという制約の判定}
 \label{src:rbtree}
-\end{table}
+\end{figure}
 
 % }}}
 
@@ -396,11 +396,11 @@
 本論文では操作を挿入に限定し、任意の順で木に要素を挿入しても木がバランスすることを検証する。
 検証には当研究室で開発している検証用メタ計算ライブラリ akasha を用いる。
 akasha では仕様を Meta Code Segment に記述するため、CbCで常に真となる式として定義する
-赤黒木の性質である、 木をルートから辿った際に最も長い経路は最も短い経路の高々2倍に収まることをCbCのコードで記述する(表\ref{src:specification})。
+赤黒木の性質である、 木をルートから辿った際に最も長い経路は最も短い経路の高々2倍に収まることをCbCのコードで記述する(図\ref{src:specification})。
 
 % {{{ 木の高さの仕様記述
 
-\begin{table}[ht]
+\begin{figure}[ht]
 \begin{lstlisting}
 if (akashaInfo.maxHeight >
     2*akashaInfo.minHeight) {
@@ -409,17 +409,17 @@
 \end{lstlisting}
 \caption{木の高さの仕様記述}
 \label{src:specification}
-\end{table}
+\end{figure}
 
 % }}}
 
-表\ref{src:specification}で定義した仕様が常に成り立つか、全ての挿入順の組み合わせを列挙しながら確認していく。
+図\ref{src:specification}で定義した仕様が常に成り立つか、全ての挿入順の組み合わせを列挙しながら確認していく。
 無限回の挿入順番を数え上げることは状態の抽象化無しには不可能なので、限られた要素数の挿入を検証する。
-検証の対象である赤黒木を内包する Meta Data Segment を定義し、挿入順の列挙に必要なデータを追加で定義する(表\ref{src:akashaDs})。
+検証の対象である赤黒木を内包する Meta Data Segment を定義し、挿入順の列挙に必要なデータを追加で定義する(図\ref{src:akashaDs})。
 検証に必要なデータには挿入順の数え上げに使う環状リスト \verb/Iterator/ とその要素 \verb/IterElem/、検証に使う情報を保持する \verb/AkashaInfo/、木をなぞる際に使う \verb/AkashaNode/がある。
 
 % {{{ akasha の Data Segment
-\begin{table}[ht]
+\begin{figure}[ht]
 \begin{lstlisting}
 // Data Segment
 union Data {
@@ -454,7 +454,7 @@
 \end{lstlisting}
 \caption{akasha の Data Segment}
 \label{src:akashaDs}
-\end{table}
+\end{figure}
 
 % }}}
 
@@ -463,12 +463,12 @@
 環状リストに全ての要素が無くなった時、1つの組み合わせを列挙したことになる。
 1つの挿入順を列挙後、前の深さの環状リストを再現し、環状リストの先頭を進めることで組み合わせの列挙を続ける。
 
-挿入順を列挙しつつ、木に要素を挿入する度に表\ref{src:specification}の仕様が成り立つか Code Segment を実行して確認する。
-仕様には木の高さが含まれるため、その値を取得する Meta Code Segment が必要である(表\ref{src:getMinHeight})。
+挿入順を列挙しつつ、木に要素を挿入する度に図\ref{src:specification}の仕様が成り立つか Code Segment を実行して確認する。
+仕様には木の高さが含まれるため、その値を取得する Meta Code Segment が必要である(図\ref{src:getMinHeight})。
 
 % {{{ 木の最も低い高さを取得する Code Segment
 
-\begin{table}[ht]
+\begin{figure}[ht]
 \begin{lstlisting}
 __code getMinHeight(struct Context* context,
                     struct AkashaNode* left,
@@ -513,7 +513,7 @@
 \end{lstlisting}
 \caption{木の最も低い高さを取得する Code Segment}
 \label{src:getMinHeight}
-\end{table}
+\end{figure}
 
 % }}}
 
@@ -534,13 +534,13 @@
 比較のために全く同じ赤黒木のソースコードを用いたいが、CbCの構文はCとは異なるために変換が必要である。
 CbCはCと似た構文を持つため、\verb/__code/ を \verb/void/ に、 \verb/goto/ を \verb/return/ に置換することで機械的にC言語に変換できる。
 
-CBMC における仕様は bool を返す式として記述するため、akashaと同様の仕様定義が利用できる(表\ref{src:specificationCBMC}。
+CBMC における仕様は bool を返す式として記述するため、akashaと同様の仕様定義が利用できる(図\ref{src:specificationCBMC}。
 C では再帰呼び出しができるため、木の高さは再帰関数で確認している。
 assert が true になるような実行パターンを CBMC が見付けると、その実行パターンが反例として出力される。
 
 % {{{ CBMCにおける仕様記述
 
-\begin{table}[ht]
+\begin{figure}[ht]
 \begin{lstlisting}
 void verifySpecification(struct Context* context,
                          struct Tree* tree) {
@@ -551,16 +551,16 @@
 \end{lstlisting}
 \caption{CBMCにおける仕様記述}
 \label{src:specificationCBMC}
-\end{table}
+\end{figure}
 
 % }}}
 
-挿入順の数え上げにはCBMCの機能に存在する非決定的な値 \verb/nondet_int()/ を用いた(表\ref{src:enumerateInputs})。
+挿入順の数え上げにはCBMCの機能に存在する非決定的な値 \verb/nondet_int()/ を用いた(図\ref{src:enumerateInputs})。
 検証する有限の要素数回分、ランダムな値を入力させることで挿入順の数え上げとする。
 
 % {{{ CBMCによる挿入順の数え上げ
 
-\begin{table}[ht]
+\begin{figure}[ht]
 \begin{lstlisting}
 void enumerateInputs(struct Context* context,
                      struct Node* node) {
@@ -578,7 +578,7 @@
 \end{lstlisting}
 \caption{CBMCによる挿入順の数え上げ}
 \label{src:enumerateInputs}
-\end{table}
+\end{figure}
 
 % }}}