--- a/paper/vmpcbc.tex	Tue Jul 05 12:00:31 2016 +0900
+++ b/paper/vmpcbc.tex	Tue Jul 05 13:34:52 2016 +0900
@@ -93,7 +93,7 @@
 \section{コードセグメントとデータセグメント}
 本研究は実際に動作するプログラムの信頼性を保証することを目的とする。
 プログラムの信頼性とは、定められた環境下においてプログラムの動作が必ず仕様を満たすことである。
-プログラムが仕様を満たすことを保証する手法として、プログラムの性質を証明する手法やプログラムの状態を全て数えあげるモデルチェッカなどが存在する。 % TODO ref
+プログラムが仕様を満たすことを保証する手法として、プログラムの性質を証明する手法\cite{cite:agda}やプログラムの状態を全て数えあげるモデルチェッカ\cite{cite:cbmc}などが存在する。
 しかし、証明では実際に動作するコードでなく証明用にコードを書き直したり、モデルチェッカでは高速化のために抽象化した記号実行によって性質が検証されるなど、実際に動作するコードとの乖離が発生してしまう。
 
 実際に動作するコードを検証しやすいよう、本研究室ではコードセグメントとデータセグメントを用いるプログラミングスタイルを提案している。 % TODO ref?
@@ -120,7 +120,7 @@
 プログラムの性質を検証する機能をメタ計算として提供することで、ユーザが書いたコードセグメントを変更することなく、メタ計算を追加するだけでプログラムの信頼性を上げる。
 
 \section{Continuation based C}
-コードセグメントとデータセグメントを用いたプログラミングスタイルで記述言語に Continuation based C\cite{cbc-clang} 言語が存在する。
+コードセグメントとデータセグメントを用いたプログラミングスタイルで記述言語に Continuation based C\cite{cite:cbc-clang} 言語が存在する。
 Continuation based C (以下 CbC)はOSや組込みシステムなどの記述を行なうことを目標に作られた、アセンブラとC言語の中間のような言語である。
 CbC におけるコードセグメントはC言語における関数に、関数呼び出しが末尾のみである制約を加えようなものである。
 コードセグメントどうしの接続は goto によって表される(Code\ref{src:simpleCs})。
@@ -182,7 +182,7 @@
 Code\ref{src:stub}では \verb/twice/ の際に2倍する値は count の値であることを \verb/twice_stub/ で指定している。
 CbC におけるメタコードセグメントはCode\ref{src:stub}や goto する際に必ず通るコードセグメント(Code\ref{src:meta}の \verb/meta/)のように表現される。
 
-\begin{lstlisting}[label=src:meta, caption=meta ] %メタコードセグメントを用いて接続した例]
+\begin{lstlisting}[label=src:meta, caption=meta ] %メタ計算として接続した例]
 
 struct Context {
     union Data *data;
@@ -213,16 +213,17 @@
 }
 \end{lstlisting}
 
-メタコードセグメントの切り替えは \verb/meta/ を変更することで実現できる。
+メタ計算の切り替えは \verb/meta/ を変更することで実現できる。
 また、メタデータセグメントに相当する \verb/Context/ はデータセグメントをフィールドに持つ構造体として表現できる。
 
 CbC におけるメタ計算の例にメモリ管理がある。
 メモリの確保やポインタ演算をメタコードセグメントのみで行なうことで、コードセグメント側ではメモリに由来するエラーを排除することができる。
-また、メタ計算を切り替えることでメモリの管理方法も切り替えることができるため、不要な領域の開放するよう拡張することも容易である。
+加えて、メタ計算を切り替えることでメモリの管理方法も切り替えることができるため、不要な領域の開放するよう拡張することも容易である。
+また、通常の計算を保存するようにメタ計算を定義することにより、例外処理といった処理を含む計算に拡張することができる\ref{cite:monad}。
 
 \section{メタ計算を用いたデータ構造の性質の検証}
-CbC で記述されさデータ構造と、データ構造に対する処理の性質を実際に検証する。
-検証の対象として、当研究室で CbC を用いて開発している Gears OS \cite{gears-os}における非破壊赤黒木を用いる。
+CbC で記述されたデータ構造と、データ構造に対する処理の性質を実際に検証する。
+検証の対象として、当研究室で CbC を用いて開発している Gears OS \cite{cite:gears-os}における非破壊赤黒木を用いる。
 赤黒木とは木構造を持ったデータ構造であり、各ノードに赤と黒の色を割り当て、その色を用いて木の高さのバランスを取る。
 また、非破壊であるため木にデータを挿入、削除した際に過去の木は変更されない。
 非破壊赤黒木に求められる性質には、挿入したデータを参照できること、削除できること、値の更新ができること、操作を行なった後の木はバランスしていること、などが存在する。
@@ -244,11 +245,11 @@
 定義した仕様に対し、挿入する値と順番の全ての組み合わせに対して確認していく。
 また、仕様を満たさない反例が存在する場合はその具体的な組み合わせの値を出力する。
 
-当研究室で開発している検証用メタ計算ライブラリ akasha と、C言語の有限モデルチェッカ cbmc を用いてこの仕様を検証した。
+当研究室で開発している検証用メタ計算ライブラリ akasha と、C言語の有限モデルチェッカ cbmc\cite{cite:cbmc} を用いてこの仕様を検証した。
 akasha では検証用の仕様をメタコードセグメントに定義する。
 検証に必要な木の状態の保持や挿入順番の数え上げといった状態の保持はメタデータセグメントが行なう。
-akasha を用いて要素数13個までは任意の順で挿入を行なっても仕様が満たされることを検証した。
-また、赤黒木の処理に恣意的にバグを追加した際には反例をきちんとと返した。
+要素数13個までは任意の順で挿入を行なっても仕様が満たされることをakasha を用いて検証した。
+また、赤黒木の処理に恣意的にバグを追加した際にはakashaは反例を返した。
 
 CbCは C とほぼ同様の構文を持つため、単純な置換でC言語に変換することができる。
 CbCで記述された赤黒木のコードを置換でC言語に変換し、cbmcで検証する。
@@ -270,8 +271,11 @@
 
 \begin{thebibliography}{9}
 
-\bibitem{cbc-clang} 徳森海斗, 河野真治: Continuation based CのLLVM/clang 3.5上の実装について, 情報処理学会システムソフトウェアとオペレーティング・システム研究会 (OS) (2014)
-\bibitem{gears-os} 伊波立樹, 東恩納琢偉, 河野真治: Code Gear、 Data Gear に基づく OS のプロトタイプ, 情報処理学会システムソフトウェアとオペレーティング・システム研究会 (OS) (2016)
+\bibitem{cite:cbc-clang} 徳森海斗, 河野真治: Continuation based CのLLVM/clang 3.5上の実装について, 情報処理学会システムソフトウェアとオペレーティング・システム研究会 (OS) (2014)
+\bibitem{cite:gears-os} 伊波立樹, 東恩納琢偉, 河野真治: Code Gear、 Data Gear に基づく OS のプロトタイプ, 情報処理学会システムソフトウェアとオペレーティング・システム研究会 (OS) (2016)
+\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).
 
 \end{thebibliography}