--- a/paper/vmpcbc.tex	Wed Jul 06 19:40:01 2016 +0900
+++ b/paper/vmpcbc.tex	Thu Jul 07 17:22:35 2016 +0900
@@ -116,13 +116,14 @@
 ソフトウェアの検証手法には、定理証明とモデル検査がある。
 定理証明はソフトウェアが満たすべき仕様を論理式で記述し、その式が常に真であることを証明する。
 定理証明を行なう言語には依存型で証明を行なう Agda\cite{cite:agda} や Coq\cite{cite:coq} などが存在する。
-モデル検査はソフトウェアのモデルの全ての状態において仕様が満たされるかを確認するものである。
-モデル検査を行なうモデル検査器には、 promela と呼ばれる言語でモデルを記述する spin\cite{cite:spin} やモデルを状態遷移系で記述する NuSMV\cite{cite:nusmv} 、ANSI-Cを記号実行することができる CBMC\cite{cite:cbmc} などが存在する。
+モデル検査はソフトウェアの全ての状態において仕様が満たされるかを確認するものである。
+モデル検査器には、 Promela と呼ばれる言語でモデルを記述する Spin\cite{cite:spin} やモデルを状態遷移系で記述する NuSMV\cite{cite:nusmv} 、ANSI-Cを記号実行することができる CBMC\cite{cite:cbmc} などが存在する。
 証明やモデル検査器で検証を行なう際、実際に動作するコードでなく検証用にコードを書き直す必要があるなど、実際の実装との乖離が存在する。
-よって、検証した環境では仕様が満たされていても、実装にバグが入り込み信頼性を保証できない可能性がある。
+よって、書き直した記述では仕様が満たされていても、実装にバグが入り込み信頼性を保証できない可能性がある。
 本研究は実際に動作するプログラムの信頼性を保証することを目的とする。
 
 \section{Code SegmentとData Segment}
+% どうしてcs/dsなのかのストーリ＝とか
 動作するコードを検証しやすいよう、本研究室ではCode SegmentとData Segmentを用いるプログラミングスタイルを提案している。
 Code Segmentとは処理の単位であり、ループを含まない単純な処理のみを行なう。
 プログラムはCode Segmentどうしを組み合わせることで構築される(図\ref{fig:csds})。
@@ -138,8 +139,9 @@
 \end{figure}
 
 ここで、Code Segmentどうしの接続処理について考える。
-処理を表すCode Segmentどうしの接続も処理であるため、Code Segmentで表現できる。
-このような、計算を実現するための計算をメタ計算と呼び、メタ計算を行なうCode SegmentをMeta Code Segmentと呼ぶ。
+処理を表すCode Segmentどうしの接続も処理である。
+このような、計算を実現するための計算をメタ計算と呼ぶ。
+メタ計算は Code Segment で記述することが可能であり、メタ計算を記述したCode SegmentをMeta Code Segmentと呼ぶ。
 Meta Code SegmentはCode Segment間に存在する上位の処理と考えることもできる(図\ref{fig:metaCSDS})。
 
 \begin{figure}[htbp]
@@ -154,9 +156,9 @@
 プログラムの性質を検証する機能をメタ計算として提供することで、ユーザが書いたCode Segmentを変更することなく、メタ計算を追加するだけでプログラムの信頼性を上げる。
 
 \section{Continuation based C}
-Code SegmentとData Segmentを用いたプログラミングスタイルで記述する言語に 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 におけるCode SegmentはC言語における関数に、関数呼び出しが末尾のみである制約を加えようなものである。
+CbC におけるCode SegmentはC言語における関数に、関数呼び出しが末尾のみである制約を加えたものである。
 Code Segmentどうしの接続は goto による軽量継続で表される(表\ref{src:simpleCs})。
 軽量継続とは呼び出し元の環境を持たずに次の処理へと移動することであり、呼び出し元のスタックフレームを破棄しながら関数呼び出しを行なうようなものである。
 なお、C言語の資産を利用するために通常の関数呼び出しを行なうことも可能である。
@@ -208,7 +210,7 @@
 
 表\ref{src:simpleDs}ではData Segmentとして int を持つ count と unsigned int を持つ port の2つを定義している。
 
-Code Segment 内部では演算やポインタ演算は行なわず、メタ計算でポインタへの演算を行なう。
+Code Segment 内部ではポインタ演算は行なわず、メタ計算でポインタへの演算を行なう。
 これにはメモリ管理をメタ計算部分に分離することで、プログラムを検証しやすくするねらいがある。
 Code Segment がどの Data Segment にアクセスするかといった指定も Meta Code Segment で行なう(表\ref{src:stub} における \verb/twice_stub/)。
 CbC における Meta Code Segment は Code Segment と Code Segment 間に存在する Code Segment である。
@@ -250,17 +252,20 @@
 // Meta Data Segment
 struct Context {
     union Data *data;  // Data Segment
-    unsigned int a;    /* メタ計算に必要なデータ */
+    unsigned int gotoCount; /* メタ計算に必要なデータ */
+    unsigned int stepOfAddTen;
 };
 
 // Meta Code Segment
 __code meta(struct Context* context,
             enum Code next) {
+    countext.gotoCount++;
 
     /* 接続時に行なうメタ計算を記述 */
     switch (next) {
         case AddTen:
             /* 特定のCode Segmentへのメタ計算 */
+            context.stepOfAddTen++;
             goto addTen_stub(context);
         case Twice:
             goto twice_stub(context);
@@ -314,13 +319,14 @@
     \end{center}
 \end{figure}
 
-関数呼び出しが可能な言語では戻り値で経路を辿ることか可能だが、CbC は \verb/goto/による軽量継続のみで記述する必要があるため、経路を辿るにはノードに親への参照を持たせるか挿入・削除時に辿った経路を記憶するしかない。
+関数呼び出しが可能な言語では再起呼び出しで木を辿ることか可能だが、CbC は \verb/goto/による軽量継続のみで記述する必要があるため、経路を辿るにはノードに親への参照を持たせるか挿入・削除時に辿った経路を記憶するしかない。
 ノードが親への参照を持つ非破壊木構造は構築出来ないため、辿った経路を記憶する方法を用いる。
 辿った経路を記憶するため Meta Data Segment にスタックを持たせる(表\ref{src:stack}における Context 内部の \verb/node_stack/)。
-なお、このスタックは軽量継続ではなく関数呼び出しで利用している。
 赤黒木で利用する Data Segment を表\ref{src:stack}に表す。
 Data Segment は各ノードの情報を持つ \verb/Node/ と赤黒木を格納する \verb/Tree/と、挿入などの操作中の一時的な木を持つ\verb/Traverse/の共用体で表される。
 
+% TODO: Appendix でrbtreeのコード
+
 % {{{ 赤黒木の Data Segment
 
 \begin{table}[ht]
@@ -399,9 +405,9 @@
 赤黒木に求められる性質には以下のようなものがある
 
 \begin{itemize}
-    \item 挿入したデータを参照できるこ
-    \item 挿入したデータを削除できること
-    \item 挿入したデータの値の更新ができること
+    \item 挿入したデータを参照できること
+    \item 削除したデータは参照できないこと
+    \item 値を更新した後は更新された値が参照されること
     \item 操作を行なった後の木はバランスしていること
 \end{itemize}
 
@@ -410,6 +416,8 @@
 akasha では仕様を Meta Code Segment に記述するため、CbCで常に真となる式として定義する
 赤黒木の性質である、 木をルートから辿った際に最も長い経路は最も短い経路の高々2倍に収まることをCbCのコードで記述する(表\ref{src:specification})。
 
+%TODO akasha info はめた
+
 % {{{ 木の高さの仕様記述
 
 \begin{table}[ht]
@@ -535,7 +543,7 @@
 葉ならば高さを更新し、スタックからノードを1つ破棄して自身に \verb/goto/する。
 葉でなければ高さを1つ増やしながらスタックに左右の子供を積み、自身に \verb/goto/ する。
 
-このように、Code Segment の検証に必要な仕様や処理は Code Segment で記述することができる。
+このように、Code Segment の検証に必要な仕様や処理は Meta Code Segment で記述することができる。
 akasha におけるメタ計算を用いて、要素数13個まで任意の順で挿入を行なっても仕様が満たされることを検証した。
 また、赤黒木の処理内部にバグを追加した際にはakashaは反例を返した。
 
@@ -605,6 +613,11 @@
 CbC で記述したプログラムに対する仕様の検証を行なうことができた。
 CbC はCode SegmentとData Segmentを用いてプログラミングすることで、検証用にコードを変更することなく検証を行なうことができた。
 
+% 考察
+
+% やってる範囲は今は小さい
+% どうすれば拡張できるか
+
 今後の課題として、検証できる範囲の拡大や効率化、値の抽象化などがある。
 CBMCではポインタへの不正アクセスを行なう実行例を検出する機能が組込みで存在している。
 akashaでも一般的なエラーに対するメタ計算などを定義したい。
@@ -628,15 +641,10 @@
 \end{thebibliography}
 
 \begin{biography}
-\profile{n}{比嘉健太}{2015年琉球大学工学部情報工学科卒業。2015年琉球大学大学院理工学研究科情報工学専攻入学。}
-% TODO: update
-\profile{n}{河野真治}{1960年生．1982年情報処理大学理学部情報科学科卒業．
-1984年同大学大学院修士課程修了．1987年同博士課程修了．理学博士．1987年情報処
-理大学助手．1992年架空大学助教授．1997年同大教授．オンライン出版の研究
-に従事．2010年情報処理記念賞受賞．電子情報通信学会，IEEE，IEEE-CS，ACM
-各会員．}
+\profile{n}{比嘉健太}{1992年生。2015年琉球大学工学部情報工学科卒業。2015年琉球大学大学院理工学研究科情報工学専攻入学。}
+\profile{n}{河野真治}{1959年生。1984年3月東京工業大学理学部化学科卒業。1986年3月東京大学大学院情報工学課程修了。1989年5月工学博士。 1989-1996年 Sony Computer Science Laboratry, Inc. 1996年 琉球大学准教授。
+情報処理学会, ACM , 日本ソフトウェア科学会各会員。
+}
 \end{biography}
 
-
-
 \end{document}