# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1467687631 -32400
# Node ID 879272af0acd566c453f61c689043ca1a06adbed
# Parent  ea7b331f263ae6e26f692a435eb4b611bf59f0ff
Add sample codes

diff -r ea7b331f263a -r 879272af0acd paper/vmpcbc.tex
--- a/paper/vmpcbc.tex	Mon Jul 04 16:03:53 2016 +0900
+++ b/paper/vmpcbc.tex	Tue Jul 05 12:00:31 2016 +0900
@@ -30,6 +30,8 @@
 \setcounter{号数}{1}
 \setcounter{page}{1}
 
+% TODO: コードセグメント, Code Segment の統一
+
 
 \受付{2015}{3}{4}
 %\再受付{2015}{7}{16}   %省略可能
@@ -110,11 +112,12 @@
 \end{figure}
 
 ここで、コードセグメントどうしの接続処理について考える。
-処理を表すコードセグメントの接続も処理であるため、コードセグメントで表現できる。
-このように、計算を実現するための計算をメタ計算と呼び、メタ計算を行なうコードセグメントをメタコードセグメントと呼ぶ。
+処理を表すコードセグメントどうしの接続も処理であるため、コードセグメントで表現できる。
+このような計算を実現するための計算をメタ計算と呼び、メタ計算を行なうコードセグメントをメタコードセグメントと呼ぶ。
 メタコードセグメントはコードセグメント間に存在する処理と考えることもできる。
 また、メタ計算に必要なデータはメタデータセグメントに格納する。
-プログラムの性質を検証する機能をメタ計算として提供することで、ユーザが書いたコードセグメントを変更することなく、メタコードセグメントを切り替えるだけでプログラムの信頼性を上げることができる。
+メタデータセグメントは通常の処理に必要なデータセグメントの拡張である。
+プログラムの性質を検証する機能をメタ計算として提供することで、ユーザが書いたコードセグメントを変更することなく、メタ計算を追加するだけでプログラムの信頼性を上げる。
 
 \section{Continuation based C}
 コードセグメントとデータセグメントを用いたプログラミングスタイルで記述言語に Continuation based C\cite{cbc-clang} 言語が存在する。
@@ -123,9 +126,9 @@
 コードセグメントどうしの接続は goto によって表される(Code\ref{src:simpleCs})。
 
 \begin{lstlisting}[label=src:simpleCs, caption=code]%コードセグメントの接続例 (10加算して2倍する)]
-__code addTen(unsigned int x) {
-    int y = x+10;
-    goto twice(y);
+__code addTen(int a) {
+    int b = a+10;
+    goto twice(b);
 }
 
 __code twice(int x) {
@@ -134,12 +137,58 @@
 }
 \end{lstlisting}
 
-また、データセグメントは構造体と共用体を用いたデータ構造を用いる。
+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/ を実行する。
+
+また、CbCにおけるデータセグメントはC言語における構造体と共用体を用いたデータ構造である。
+各コードセグメントで必要な値を構造体で定義し、それらの共用体としてデータセグメントを定義する(Code\ref{src:simpleDs})。
+
+\begin{lstlisting}[label=src:simpleDs, caption=data]%データセグメントの例 (10加算して2倍する)]
+
+union Data {
+    struct Count {
+        int x;
+    } count;
+    struct Port {
+        unsigned int port;
+    } port;
+};
+\end{lstlisting}
 
-CbC におけるメタコードセグメントは goto する際に必ず通るコードセグメント(以下のCode\ref{src:meta}では \verb/meta/ がそれにあたる)のように表現される。
+Code\ref{src:simpleDs}ではデータセグメントとして int を持つ count と unsigned int を持つ port の2つを定義している。
+コードセグメントに\verb/goto/する際に利用するデータセグメントを指定することで、データセグメント内部の値で処理が行なえる。
+
+\begin{lstlisting}[label=src:stub, caption=stub]%データセグメントの利用例 (countの値を2倍する)]
+
+__code addTen(union Data* ds, int a) {
+    int b = a+10;
+    goto twice_stub(ds);
+}
+
+__code twice_stub(union Data* ds) {
+    goto twice(ds->count.x);
+}
+
+__code twice(int x) {
+    int y = 2*x;
+    goto showValue(y);
+}
+\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/)のように表現される。
 
 \begin{lstlisting}[label=src:meta, caption=meta ] %メタコードセグメントを用いて接続した例]
 
+struct Context {
+    union Data *data;
+    /* メタ計算に必要なデータ */
+};
+
 __code meta(struct Context* context,
             enum Code next) {
 
@@ -147,25 +196,25 @@
     switch (next) {
         case AddTen:
             /* 特定のコードセグメントへのメタ計算 */
-            goto addTen(context);
+            goto addTen_stub(context);
         case Twice:
-            goto twice(context);
+            goto twice_stub(context);
     }
 }
 
-__code addTen(struct Context* context) {
-    context->x = context->x+10;
+__code addTen(struct Context* context, int a) {
+    x = x+10;
     goto meta(context, Twice);
 }
 
-__code twice(struct Context* context) {
-    context->x = context->x*2;
+__code twice(struct Context* context, int x) {
+    x = x*2;
     goto meta(context, ShowValue);
-
+}
 \end{lstlisting}
 
-メタコードセグメントの切り替えは \verb/meta/ の切り替えで表現できる。
-メタデータセグメントはデータセグメントをフィールドに持つ構造体として表現できる。
+メタコードセグメントの切り替えは \verb/meta/ を変更することで実現できる。
+また、メタデータセグメントに相当する \verb/Context/ はデータセグメントをフィールドに持つ構造体として表現できる。
 
 CbC におけるメタ計算の例にメモリ管理がある。
 メモリの確保やポインタ演算をメタコードセグメントのみで行なうことで、コードセグメント側ではメモリに由来するエラーを排除することができる。
@@ -201,7 +250,7 @@
 akasha を用いて要素数13個までは任意の順で挿入を行なっても仕様が満たされることを検証した。
 また、赤黒木の処理に恣意的にバグを追加した際には反例をきちんとと返した。
 
-CbCは C とほぼ同じ構文を持つため、単純な置換でC言語に変換することができる。
+CbCは C とほぼ同様の構文を持つため、単純な置換でC言語に変換することができる。
 CbCで記述された赤黒木のコードを置換でC言語に変換し、cbmcで検証する。
 cbmc における仕様は bool を返すコードとして記述するため、akashaと同じ仕様定義を用いることができる。
 任意の順番での挿入の検証にはcbmcの機能に存在する非決定的な入力を用いた。