# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1467615538 -32400
# Node ID c957fb73860f2a53e307f2d3284b3f26a1659951
# Parent  7d776d6abf67d7bdf4aef5ce479e1aaed6d8810d
Add CbC sources

diff -r 7d776d6abf67 -r c957fb73860f paper/vmpcbc.tex
--- a/paper/vmpcbc.tex	Mon Jul 04 15:02:26 2016 +0900
+++ b/paper/vmpcbc.tex	Mon Jul 04 15:58:58 2016 +0900
@@ -4,6 +4,23 @@
 
 \usepackage[dvipdfmx]{graphicx}
 \usepackage{latexsym}
+\usepackage{listings}
+\lstset{
+  language={C},
+  basicstyle={\small},
+  commentstyle={\small\itshape},
+  keywordstyle={\small\bfseries},
+  stringstyle={\small},
+  frame={trlb},
+  breaklines=true,
+  columns=[l]{fullflexible},
+  xrightmargin=0zw,
+  xleftmargin=3zw,
+  lineskip=-0.5ex,
+  captionpos=b,
+  moredelim=**[s][\color{red}]{\"compressed}{\"},
+}
+\renewcommand{\lstlistingname}{Code}
 
 \def\Underline{\setbox0\hbox\bgroup\let\\\endUnderline}
 \def\endUnderline{\vphantom{y}\egroup\smash{\underline{\box0}}\\}
@@ -103,15 +120,50 @@
 コードセグメントとデータセグメントを用いたプログラミングスタイルで記述言語に Continuation based C\cite{cbc-clang} 言語が存在する。
 Continuation based C (以下 CbC)はOSや組込みシステムなどの記述を行なうことを目標に作られた、アセンブラとC言語の中間のような言語である。
 CbC におけるコードセグメントはC言語における関数に、関数呼び出しが末尾のみである制約を加えようなものである。
-コードセグメントどうしの接続は goto によって表される。
+コードセグメントどうしの接続は goto によって表される(Code\ref{src:simpleCs})。
 
-% TODO: かんたんな goto program
+\begin{lstlisting}[label=src:simpleCs, caption=code]%コードセグメントの接続例 (10加算して2倍する)]
+__code addTen(unsigned int x) {
+    int y = x+10;
+    goto twice(y);
+}
+
+__code twice(int x) {
+    int y = 2*x;
+    goto showValue(y);
+}
+\end{lstlisting}
 
 また、データセグメントは構造体と共用体を用いたデータ構造を用いる。
 
-CbC におけるメタコードセグメントは goto する際に必ず通るコードセグメント(以下の例では \verb/meta/ がそれにあたる)として表現される。
+CbC におけるメタコードセグメントは goto する際に必ず通るコードセグメント(以下のCode\ref{src:meta}では \verb/meta/ がそれにあたる)のように表現される。
+
+\begin{lstlisting}[label=src:meta, caption=meta ] %メタコードセグメントを用いて接続した例]
+
+__code meta(struct Context* context,
+            enum Code next) {
 
-% TODO: meta を使った program
+    /* 接続時に行なうメタ計算を記述 */
+    switch (next) {
+        case AddTen:
+            /* 特定のコードセグメントへのメタ計算 */
+            goto addTen(context);
+        case Twice:
+            goto twice(context);
+    }
+}
+
+__code addTen(struct Context* context) {
+    context->x = context->x+10;
+    goto meta(context, Twice);
+}
+
+__code twice(struct Context* context) {
+    context->x = context->x*2;
+    goto meta(context, ShowValue);
+
+\end{lstlisting}
+
 メタコードセグメントの切り替えは \verb/meta/ の切り替えで表現できる。
 メタデータセグメントはデータセグメントをフィールドに持つ構造体として表現できる。
 
@@ -129,8 +181,17 @@
 
 まず、検証を行なうために満たすべき仕様を定義する。
 仕様はデータ構造が常に満たすべき論理式として表現し、CbC のコードで記述する。
-検証する仕様として、木を根から辿った際に最も長い経路は最も短い経路の高々2倍に収まることを CbC で定義する。
-% TODO code
+検証する仕様として、木を根から辿った際に最も長い経路は最も短い経路の高々2倍に収まることを CbC で定義する(Code\ref{src:specification}。
+
+\begin{lstlisting}[label=src:specification, caption=s]% 木の高さの仕様記述]
+
+if (akashaInfo.maxHeight >
+    2*akashaInfo.minHeight) {
+   goto meta(context, ShowTrace);
+}
+
+\end{lstlisting}
+
 定義した仕様に対し、挿入する値と順番の全ての組み合わせに対して確認していく。
 また、仕様を満たさない反例が存在する場合はその具体的な組み合わせの値を出力する。