--- a/paper/vmpcbc.tex	Tue Jul 05 17:34:31 2016 +0900
+++ b/paper/vmpcbc.tex	Tue Jul 05 17:51:28 2016 +0900
@@ -30,7 +30,7 @@
 \setcounter{号数}{1}
 \setcounter{page}{1}
 
-% TODO: コードセグメント, Code Segment の統一
+% TODO: Code Segment, Code Segment の統一
 
 
 \受付{2015}{3}{4}
@@ -90,7 +90,7 @@
 
 \maketitle
 
-\section{コードセグメントとデータセグメント}
+\section{Code SegmentとData Segment}
 本研究は実際に動作するプログラムの信頼性を保証することを目的とする。
 プログラムの信頼性とは、定められた環境下においてプログラムの動作が必ず仕様を満たすことである。
 プログラムが仕様を満たすことを保証する手法として、プログラムの性質を証明する手法\cite{cite:agda}やプログラムの状態を全て数えあげるモデルチェッカ\cite{cite:cbmc}などが存在する。
@@ -98,34 +98,43 @@
 よって、検証した環境では仕様が満たされていても、実装にバグが入り込み信頼性を保証できない可能性がある。
 仕様とその実装コードの信頼性を保証するため、実際に動作するコードの検証を行なう。
 
-動作するコードを検証しやすいよう、本研究室ではコードセグメントとデータセグメントを用いるプログラミングスタイルを提案している。
-コードセグメントとは処理の単位であり、ループを含まない単純な処理のみを行なう。
-プログラムはコードセグメントどうしを組み合わせることで構築される(図\ref{fig:csds})。
-コードセグメント間における値の受け渡しには、データセグメントというデータの単位で行なう。
-なお、接続されたコードセグメントには依存関係が発生するが、依存関係が無いコードセグメントは並列に実行することが可能である。
+動作するコードを検証しやすいよう、本研究室ではCode SegmentとData Segmentを用いるプログラミングスタイルを提案している。
+Code Segmentとは処理の単位であり、ループを含まない単純な処理のみを行なう。
+プログラムはCode Segmentどうしを組み合わせることで構築される(図\ref{fig:csds})。
+Code Segment間における値の受け渡しには、Data Segmentというデータの単位で行なう。
+なお、接続されたCode Segmentには依存関係が発生するが、依存関係が無いCode Segmentは並列に実行することが可能である。
 
 \begin{figure}
     \begin{center}
         \includegraphics[scale=0.5]{fig/code_segment_data_segment.pdf}
-        \caption{コードセグメントどうしの組み合わせ}
+        \caption{Code Segmentどうしの組み合わせ}
         \label{fig:csds}
     \end{center}
 \end{figure}
 
-ここで、コードセグメントどうしの接続処理について考える。
-処理を表すコードセグメントどうしの接続も処理であるため、コードセグメントで表現できる。
-このような計算を実現するための計算をメタ計算と呼び、メタ計算を行なうコードセグメントをメタコードセグメントと呼ぶ。
-メタコードセグメントはコードセグメント間に存在する処理と考えることもできる。
-また、メタ計算に必要なデータはメタデータセグメントに格納し、通常の処理に必要なデータセグメントも内包する。
-プログラムの性質を検証する機能をメタ計算として提供することで、ユーザが書いたコードセグメントを変更することなく、メタ計算を追加するだけでプログラムの信頼性を上げる。
+ここで、Code Segmentどうしの接続処理について考える。
+処理を表すCode Segmentどうしの接続も処理であるため、Code Segmentで表現できる。
+このような計算を実現するための計算をメタ計算と呼び、メタ計算を行なうCode SegmentをMeta Code Segmentと呼ぶ。
+Meta Code SegmentはCode Segment間に存在する処理と考えることもできる(図\ref{fig:metaCSDS})。
+
+\begin{figure}[htbp]
+    \begin{center}
+        \includegraphics[scale=0.5]{fig/meta_code_segment_and_meta_data_segment.pdf}
+        \caption{Meta Code Segment と Meta Data Segment}
+        \label{fig:metaCSDS}
+    \end{center}
+\end{figure}
+
+また、メタ計算に必要なデータはMeta Data Segmentに格納し、通常の処理に必要なData Segmentも内包する。
+プログラムの性質を検証する機能をメタ計算として提供することで、ユーザが書いたCode Segmentを変更することなく、メタ計算を追加するだけでプログラムの信頼性を上げる。
 
 \section{Continuation based C}
-コードセグメントとデータセグメントを用いたプログラミングスタイルで記述言語に Continuation based C\cite{cite:cbc-clang} 言語が存在する。
+Code SegmentとData Segmentを用いたプログラミングスタイルで記述言語に Continuation based C\cite{cite:cbc-clang} 言語が存在する。
 Continuation based C (以下 CbC)はOSや組込みシステムなどの記述を行なうことを目標に作られた、アセンブラとC言語の中間のような言語である。
-CbC におけるコードセグメントはC言語における関数に、関数呼び出しが末尾のみである制約を加えようなものである。
-コードセグメントどうしの接続は goto による軽量継続で表される(Code\ref{src:simpleCs})。
+CbC におけるCode SegmentはC言語における関数に、関数呼び出しが末尾のみである制約を加えようなものである。
+Code Segmentどうしの接続は goto による軽量継続で表される(Code\ref{src:simpleCs})。
 
-\begin{lstlisting}[label=src:simpleCs, caption=code]%コードセグメントの接続例 (10加算して2倍する)]
+\begin{lstlisting}[label=src:simpleCs, caption=code]%Code Segmentの接続例 (10加算して2倍する)]
 
 __code addTen(int a) {
     int b = a+10;
@@ -138,16 +147,16 @@
 }
 \end{lstlisting}
 
-CbCにおけるコードセグメントは、C言語の関数宣言の返り値の型の部分に \verb/__code/ を記述して定義する。
-コードセグメント内部には変数の宣言やif文による分岐といったC言語の文法を用いて処理を記述する。
-Code\ref{src:simpleCs}の例では、2つのコードセグメント \verb/addTen/ と \verb/twice/を定義している。
+CbCにおけるCode Segmentは、C言語の関数宣言の返り値の型の部分に \verb/__code/ を記述して定義する。
+Code Segment内部には変数の宣言やif文による分岐といったC言語の文法を用いて処理を記述する。
+Code\ref{src:simpleCs}の例では、2つのCode Segment \verb/addTen/ と \verb/twice/を定義している。
 \verb/addTen/では int の値を受けとり、10加算して \verb/twice/ を実行する。
 \verb/twice/ では受けとったintの値を2倍して \verb/showValue/ を実行する。
 
-また、CbCにおけるデータセグメントはC言語における構造体と共用体を用いたデータ構造である。
-各コードセグメントで必要な値を構造体で定義し、それらの共用体としてデータセグメントを定義する(Code\ref{src:simpleDs})。
+また、CbCにおけるData SegmentはC言語における構造体と共用体を用いたデータ構造である。
+各Code Segmentで必要な値を構造体で定義し、それらの共用体としてData Segmentを定義する(Code\ref{src:simpleDs})。
 
-\begin{lstlisting}[label=src:simpleDs, caption=data]%データセグメントの例 (10加算して2倍する)]
+\begin{lstlisting}[label=src:simpleDs, caption=data]%Data Segmentの例 (10加算して2倍する)]
 
 union Data {
     struct Count {
@@ -159,10 +168,10 @@
 };
 \end{lstlisting}
 
-Code\ref{src:simpleDs}ではデータセグメントとして int を持つ count と unsigned int を持つ port の2つを定義している。
-コードセグメントに\verb/goto/する際に利用するデータセグメントを指定することで、データセグメント内部の値で処理が行なえる(Code\ref{src:stub})。
+Code\ref{src:simpleDs}ではData Segmentとして int を持つ count と unsigned int を持つ port の2つを定義している。
+Code Segmentに\verb/goto/する際に利用するData Segmentを指定することで、Data Segment内部の値で処理が行なえる(Code\ref{src:stub})。
 
-\begin{lstlisting}[label=src:stub, caption=stub]%データセグメントの利用例 (countの値を2倍する)]
+\begin{lstlisting}[label=src:stub, caption=stub]%Data Segmentの利用例 (countの値を2倍する)]
 
 __code addTen(union Data* ds, int a) {
     int b = a+10;
@@ -180,7 +189,7 @@
 \end{lstlisting}
 
 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/)のように表現される。
+CbC におけるMeta Code SegmentはCode\ref{src:stub} における \verb/twice_stub/ や goto する際に必ず通るCode Segment(Code\ref{src:meta}の \verb/meta/)のように表現される。
 
 \begin{lstlisting}[label=src:meta, caption=meta ] %メタ計算として接続した例]
 
@@ -195,7 +204,7 @@
     /* 接続時に行なうメタ計算を記述 */
     switch (next) {
         case AddTen:
-            /* 特定のコードセグメントへのメタ計算 */
+            /* 特定のCode Segmentへのメタ計算 */
             goto addTen_stub(context);
         case Twice:
             goto twice_stub(context);
@@ -214,10 +223,10 @@
 \end{lstlisting}
 
 メタ計算の切り替えは \verb/meta/ を変更することで実現できる。
-また、メタデータセグメントに相当する \verb/Context/ はデータセグメントをフィールドに持つ構造体として表現し、メタ計算に必要な処理は構造体にフィールドを追加することで表現できる.
+また、Meta Data Segmentに相当する \verb/Context/ はData Segmentをフィールドに持つ構造体として表現し、メタ計算に必要な処理は構造体にフィールドを追加することで表現できる.
 
 CbC におけるメタ計算の例にメモリ管理がある。
-メモリの確保やポインタ演算をメタコードセグメントのみで行なうことで、コードセグメント側ではメモリに由来するエラーを排除することができる。
+メモリの確保やポインタ演算をMeta Code Segmentのみで行なうことで、Code Segment側ではメモリに由来するエラーを排除することができる。
 加えて、メタ計算を切り替えることでメモリの管理方法も切り替えることができるため、不要な領域の開放するよう拡張することも容易である。
 また、通常の計算を保存するようメタ計算を定義することで、例外処理などを含む計算に拡張することができる\cite{cite:monad}。
 
@@ -246,9 +255,9 @@
 また、仕様を満たさない反例が存在する場合はその具体的な組み合わせの値を出力する。
 
 当研究室で開発している検証用メタ計算ライブラリ akasha と、C言語の有限モデルチェッカ cbmc\cite{cite:cbmc} を用いてこの仕様を検証した。
-akasha では検証用の仕様と検証用の処理をメタコードセグメントに定義する。
+akasha では検証用の仕様と検証用の処理をMeta Code Segmentに定義する。
 挿入順の数え上げには深さ優先探索を用いる。
-CbCには関数呼び出しが存在しないため、深さ優先探索を行なう際にスタックフレームに相当するメタデータセグメントを自ら用意する。
+CbCには関数呼び出しが存在しないため、深さ優先探索を行なう際にスタックフレームに相当するMeta Data Segmentを自ら用意する。
 各深さ毎の木を保存しておくことで、ある深さまでの探索が終了した際に木を再現ことができ、高速に探索を行なうことができる。
 要素数13個までは任意の順で挿入を行なっても仕様が満たされることをakasha を用いて検証した。
 また、赤黒木の処理内部にバグを追加した際にはakashaは反例を返した。
@@ -257,6 +266,7 @@
 CbCは C とほぼ同様の構文を持つため、単純な置換でC言語に変換することができる。
 CbCで記述された赤黒木のコードを置換でC言語に変換し、cbmcで検証を行なった。
 cbmc における仕様は bool を返すコードとして記述するため、akashaと同じ仕様定義を用いることが可能である。
+また、ポインタへの不正アクセスといった一般的なバグへの検証コードが機能として存在する。
 挿入順の数え上げにはcbmcの機能に存在する非決定的な入力を用いた。
 しかし、cbmcで検証できる範囲内ではGearsの赤黒木の仕様を検証することはできなかった。
 有限モデルチェッカでは探索する状態空間を指定し、それを越える範囲は探索しない。
@@ -266,9 +276,11 @@
 
 \section{まとめと今後の課題}
 CbC で記述したプログラムに対する仕様の検証を行なうことができた。
-CbC はコードセグメントとデータセグメントを用いてプログラミングするため、検証用にコードを変更することなくメタ計算の切り替えで検証を行なうことができた。
+CbC はCode SegmentとData Segmentを用いてプログラミングするため、検証用にコードを変更することなくメタ計算の切り替えで検証を行なうことができた。
 
 今後の課題として、検証できる範囲の拡大や効率化、値の抽象化などがある。
+cbmcではポインタへの不正アクセスを行なう実行例を検出することができる。
+akashaでも一般的なエラーに対するメタ計算などを定義したい。
 本論文では入力の組み合わせを全探索するため、過去に探索した形状の木に対しても探索を行なっていた。
 木の形状を抽象化することで探索範囲を抑えて高速に検証ができると思われる。
 また、抽象度を上げることで有限回でなく無限回の操作も扱いたい。