# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1467367553 -32400
# Node ID aeb1ce0e33c8a1586e97dc6f1099f231fa243bec
# Parent  a9e93aee0af1554d235c73ecc49020174014ba3a
Wrote section 1

diff -r a9e93aee0af1 -r aeb1ce0e33c8 paper/vmpcbc.tex
--- a/paper/vmpcbc.tex	Fri Jul 01 18:31:36 2016 +0900
+++ b/paper/vmpcbc.tex	Fri Jul 01 19:05:53 2016 +0900
@@ -70,6 +70,27 @@
 \maketitle
 
 \section{コードセグメントとデータセグメント}
+本研究は実際に動作するプログラムの信頼性を保証することを目的とする。
+プログラムの信頼性とは、定められた環境下においてプログラムの動作が必ず仕様を満たすことである。
+プログラムが仕様を満たすことを保証する手法として、プログラムの性質を証明する手法やプログラムの状態を全て数えあげるモデルチェッカなどが存在する。 % TODO ref
+しかし、証明では実際に動作するコードでなく証明用にコードを書き直したり、モデルチェッカでは高速化のために抽象化した記号実行によって性質が検証されるなど、実際に動作するコードとの乖離が発生してしまう。
+
+実際に動作するコードを検証しやすいよう、本研究室ではコードセグメントとデータセグメントを用いるプログラミングスタイルを提案している。 % TODO ref?
+コードセグメントとは処理の単位であり、ループを含まない単純な処理のみを行なう。
+プログラムはコードセグメントどうしを組み合わせることにより構築される。
+組み合わせる際のコードセグメント間における値の受け渡しにはデータセグメントを用いる。
+データセグメントとはデータの単位である。
+なお、接続されたコードセグメントには依存関係が発生するが、依存関係が無いコードセグメントは並列に実行することが可能である。
+
+% TODO cs/ds の図
+
+ここで、コードセグメントどうしの接続処理について考える。
+処理を表すコードセグメントの接続も処理であるため、コードセグメントで表現できる。
+このように、計算を実現するための計算をメタ計算と呼び、メタ計算を行なうコードセグメントをメタコードセグメントと呼ぶ。
+メタコードセグメントはコードセグメント間に存在する処理と考えることもできる。
+また、メタ計算に必要なデータはメタデータセグメントに格納する。
+プログラムの性質を検証する機能をメタ計算として提供することで、ユーザが書いたコードセグメントを変更することなく、メタコードセグメントを切り替えるだけでプログラムの信頼性を上げることができる。
+
 \section{Continuation based C}
 \section{メタ計算を用いたデータ構造の性質の検証}
 \section{まとめと今後の課題}