--- a/paper/vmpcbc.tex	Tue Jul 05 13:34:52 2016 +0900
+++ b/paper/vmpcbc.tex	Tue Jul 05 17:34:31 2016 +0900
@@ -95,12 +95,13 @@
 プログラムの信頼性とは、定められた環境下においてプログラムの動作が必ず仕様を満たすことである。
 プログラムが仕様を満たすことを保証する手法として、プログラムの性質を証明する手法\cite{cite:agda}やプログラムの状態を全て数えあげるモデルチェッカ\cite{cite:cbmc}などが存在する。
 しかし、証明では実際に動作するコードでなく証明用にコードを書き直したり、モデルチェッカでは高速化のために抽象化した記号実行によって性質が検証されるなど、実際に動作するコードとの乖離が発生してしまう。
+よって、検証した環境では仕様が満たされていても、実装にバグが入り込み信頼性を保証できない可能性がある。
+仕様とその実装コードの信頼性を保証するため、実際に動作するコードの検証を行なう。
 
-実際に動作するコードを検証しやすいよう、本研究室ではコードセグメントとデータセグメントを用いるプログラミングスタイルを提案している。 % TODO ref?
+動作するコードを検証しやすいよう、本研究室ではコードセグメントとデータセグメントを用いるプログラミングスタイルを提案している。
 コードセグメントとは処理の単位であり、ループを含まない単純な処理のみを行なう。
-プログラムはコードセグメントどうしを組み合わせることにより構築される(図\ref{fig:csds})。
-組み合わせる際のコードセグメント間における値の受け渡しにはデータセグメントを用いる。
-データセグメントとはデータの単位である。
+プログラムはコードセグメントどうしを組み合わせることで構築される(図\ref{fig:csds})。
+コードセグメント間における値の受け渡しには、データセグメントというデータの単位で行なう。
 なお、接続されたコードセグメントには依存関係が発生するが、依存関係が無いコードセグメントは並列に実行することが可能である。
 
 \begin{figure}
@@ -115,17 +116,17 @@
 処理を表すコードセグメントどうしの接続も処理であるため、コードセグメントで表現できる。
 このような計算を実現するための計算をメタ計算と呼び、メタ計算を行なうコードセグメントをメタコードセグメントと呼ぶ。
 メタコードセグメントはコードセグメント間に存在する処理と考えることもできる。
-また、メタ計算に必要なデータはメタデータセグメントに格納する。
-メタデータセグメントは通常の処理に必要なデータセグメントの拡張である。
+また、メタ計算に必要なデータはメタデータセグメントに格納し、通常の処理に必要なデータセグメントも内包する。
 プログラムの性質を検証する機能をメタ計算として提供することで、ユーザが書いたコードセグメントを変更することなく、メタ計算を追加するだけでプログラムの信頼性を上げる。
 
 \section{Continuation based C}
 コードセグメントとデータセグメントを用いたプログラミングスタイルで記述言語に Continuation based C\cite{cite:cbc-clang} 言語が存在する。
 Continuation based C (以下 CbC)はOSや組込みシステムなどの記述を行なうことを目標に作られた、アセンブラとC言語の中間のような言語である。
 CbC におけるコードセグメントはC言語における関数に、関数呼び出しが末尾のみである制約を加えようなものである。
-コードセグメントどうしの接続は goto によって表される(Code\ref{src:simpleCs})。
+コードセグメントどうしの接続は goto による軽量継続で表される(Code\ref{src:simpleCs})。
 
 \begin{lstlisting}[label=src:simpleCs, caption=code]%コードセグメントの接続例 (10加算して2倍する)]
+
 __code addTen(int a) {
     int b = a+10;
     goto twice(b);
@@ -139,10 +140,9 @@
 
 CbCにおけるコードセグメントは、C言語の関数宣言の返り値の型の部分に \verb/__code/ を記述して定義する。
 コードセグメント内部には変数の宣言やif文による分岐といったC言語の文法を用いて処理を記述する。
-次のコードセグメントへ接続する場合は \verb/goto/ を用いて接続先を指定する。
 Code\ref{src:simpleCs}の例では、2つのコードセグメント \verb/addTen/ と \verb/twice/を定義している。
 \verb/addTen/では int の値を受けとり、10加算して \verb/twice/ を実行する。
-\verb/twice/では受けとったintの値を2倍して \verb/showValue/ を実行する。
+\verb/twice/ では受けとったintの値を2倍して \verb/showValue/ を実行する。
 
 また、CbCにおけるデータセグメントはC言語における構造体と共用体を用いたデータ構造である。
 各コードセグメントで必要な値を構造体で定義し、それらの共用体としてデータセグメントを定義する(Code\ref{src:simpleDs})。
@@ -160,7 +160,7 @@
 \end{lstlisting}
 
 Code\ref{src:simpleDs}ではデータセグメントとして int を持つ count と unsigned int を持つ port の2つを定義している。
-コードセグメントに\verb/goto/する際に利用するデータセグメントを指定することで、データセグメント内部の値で処理が行なえる。
+コードセグメントに\verb/goto/する際に利用するデータセグメントを指定することで、データセグメント内部の値で処理が行なえる(Code\ref{src:stub})。
 
 \begin{lstlisting}[label=src:stub, caption=stub]%データセグメントの利用例 (countの値を2倍する)]
 
@@ -179,8 +179,8 @@
 }
 \end{lstlisting}
 
-Code\ref{src:stub}では \verb/twice/ の際に2倍する値は count の値であることを \verb/twice_stub/ で指定している。
-CbC におけるメタコードセグメントはCode\ref{src:stub}や goto する際に必ず通るコードセグメント(Code\ref{src:meta}の \verb/meta/)のように表現される。
+Code\ref{src:stub}では \verb/twice/ の処理で2倍する値が count の値であることを \verb/twice_stub/ 内で指定している。
+CbC におけるメタコードセグメントはCode\ref{src:stub} における \verb/twice_stub/ や goto する際に必ず通るコードセグメント(Code\ref{src:meta}の \verb/meta/)のように表現される。
 
 \begin{lstlisting}[label=src:meta, caption=meta ] %メタ計算として接続した例]
 
@@ -214,12 +214,12 @@
 \end{lstlisting}
 
 メタ計算の切り替えは \verb/meta/ を変更することで実現できる。
-また、メタデータセグメントに相当する \verb/Context/ はデータセグメントをフィールドに持つ構造体として表現できる。
+また、メタデータセグメントに相当する \verb/Context/ はデータセグメントをフィールドに持つ構造体として表現し、メタ計算に必要な処理は構造体にフィールドを追加することで表現できる.
 
 CbC におけるメタ計算の例にメモリ管理がある。
 メモリの確保やポインタ演算をメタコードセグメントのみで行なうことで、コードセグメント側ではメモリに由来するエラーを排除することができる。
 加えて、メタ計算を切り替えることでメモリの管理方法も切り替えることができるため、不要な領域の開放するよう拡張することも容易である。
-また、通常の計算を保存するようにメタ計算を定義することにより、例外処理といった処理を含む計算に拡張することができる\ref{cite:monad}。
+また、通常の計算を保存するようメタ計算を定義することで、例外処理などを含む計算に拡張することができる\cite{cite:monad}。
 
 \section{メタ計算を用いたデータ構造の性質の検証}
 CbC で記述されたデータ構造と、データ構造に対する処理の性質を実際に検証する。
@@ -242,26 +242,31 @@
 
 \end{lstlisting}
 
-定義した仕様に対し、挿入する値と順番の全ての組み合わせに対して確認していく。
+Code\ref{src:specification}で定義した仕様に対し、挿入する値と順番の全ての組み合わせに対して確認していく。
 また、仕様を満たさない反例が存在する場合はその具体的な組み合わせの値を出力する。
 
 当研究室で開発している検証用メタ計算ライブラリ akasha と、C言語の有限モデルチェッカ cbmc\cite{cite:cbmc} を用いてこの仕様を検証した。
-akasha では検証用の仕様をメタコードセグメントに定義する。
-検証に必要な木の状態の保持や挿入順番の数え上げといった状態の保持はメタデータセグメントが行なう。
+akasha では検証用の仕様と検証用の処理をメタコードセグメントに定義する。
+挿入順の数え上げには深さ優先探索を用いる。
+CbCには関数呼び出しが存在しないため、深さ優先探索を行なう際にスタックフレームに相当するメタデータセグメントを自ら用意する。
+各深さ毎の木を保存しておくことで、ある深さまでの探索が終了した際に木を再現ことができ、高速に探索を行なうことができる。
 要素数13個までは任意の順で挿入を行なっても仕様が満たされることをakasha を用いて検証した。
-また、赤黒木の処理に恣意的にバグを追加した際にはakashaは反例を返した。
+また、赤黒木の処理内部にバグを追加した際にはakashaは反例を返した。
 
+同じ仕様をC言語の有限モデルチェッカcbmcで検証する。
 CbCは C とほぼ同様の構文を持つため、単純な置換でC言語に変換することができる。
-CbCで記述された赤黒木のコードを置換でC言語に変換し、cbmcで検証する。
-cbmc における仕様は bool を返すコードとして記述するため、akashaと同じ仕様定義を用いることができる。
-任意の順番での挿入の検証にはcbmcの機能に存在する非決定的な入力を用いた。
-しかし、cbmcで検証できる範囲内では赤黒木の仕様を検証することはできなかった。
-有限モデルチェッカでは探索する状態空間を有限の数で指定し、それを越える範囲は探索しない。
+CbCで記述された赤黒木のコードを置換でC言語に変換し、cbmcで検証を行なった。
+cbmc における仕様は bool を返すコードとして記述するため、akashaと同じ仕様定義を用いることが可能である。
+挿入順の数え上げにはcbmcの機能に存在する非決定的な入力を用いた。
+しかし、cbmcで検証できる範囲内ではGearsの赤黒木の仕様を検証することはできなかった。
+有限モデルチェッカでは探索する状態空間を指定し、それを越える範囲は探索しない。
 cbmcで実行可能な最大の状態空間まで探索しても、バグを含んだ赤黒木に対する反例を得ることはできなかった。
 
+よって、cbmcでは検証できない範囲の検証をakashaで行なうことが確認できた。
+
 \section{まとめと今後の課題}
-コードセグメントとデータセグメントを用いたプログラミング手法を用いる言語CbCで記述したプログラムに対する仕様の検証を行なうことができた。
-メタ計算として検証を行なうことで、実際に動作するプログラムを全く変更することなくプログラムを検証した。
+CbC で記述したプログラムに対する仕様の検証を行なうことができた。
+CbC はコードセグメントとデータセグメントを用いてプログラミングするため、検証用にコードを変更することなくメタ計算の切り替えで検証を行なうことができた。
 
 今後の課題として、検証できる範囲の拡大や効率化、値の抽象化などがある。
 本論文では入力の組み合わせを全探索するため、過去に探索した形状の木に対しても探索を行なっていた。