--- a/paper/chapter/introduction.tex	Sat Jan 30 16:22:52 2021 +0900
+++ b/paper/chapter/introduction.tex	Sat Jan 30 18:59:04 2021 +0900
@@ -39,6 +39,7 @@
 OSのソースコードそのものをモデル検査すると、実際に検証されたOSが動作可能となる。
 しかしOSの処理は膨大であり、 様々な関数呼び出しや非決定的な処理、 並行処理などが発生する。
 モデル検査を行う場合でも、やみくもにOSのすべての処理を検査するのは難しい。
+モデル検査自体が巨大な状態の検証を行うため、 状態を有限に制限したり抽象化を行う必要がある。
 
 
 OSのシステムコールは、ユーザーからAPI経由で呼び出され、 いくつかの処理を行う。
@@ -48,6 +49,19 @@
 この為にはOSの処理を状態遷移系で表現し、 証明しやすくする必要がある。
 
 
-OSを状態遷移系で実装する場合、通常のC言語では状態ごとに分離するのは困難である。
-関数呼び出しを利用して状態を切り分けても、 関数呼び出し時に伴うスタックフレームの操作などでパフォーマンスにも問題がある。
-この問題を解決するには、 C言語よりも細かく記述できる言語で実装する必要がある。
\ No newline at end of file
+証明を行う対象の計算は、 その意味が大きく別けられる。
+OSやプログラムの動作においては本来したい計算がまず存在する。
+これはプログラマが通常プログラミングするものである。
+それ以外にデータをメモリに保存するためにメモリのアロケーションをする処理や、メモリから値を持ってくる処理が入る。
+メモリのほかにCPUの資源管理なども必要となる。
+さらにオブジェクト型の整合性の為にキャストなどの型変換が必要となる場合もある。
+これらユーザーが本来やりたい計算以外に、しなければならない計算が存在する。
+前者の計算をノーマルレベルの計算と呼び、後者をメタレベルの計算と呼ぶ。
+プログラムの整合性の検証はメタレベルの計算と考えられる。
+ユーザーが実装したノーマルレベルの計算に対応するメタレベルの計算を、自由にメタレベルの計算で証明したい。
+またメタレベルで検証ががすでにされたプログラムがあった場合、都度実行ユーザーの環境で検証が行われるとパフォーマンスに問題が発生する。
+この場合はメタレベルの計算を検証をするもの、しないものと切り替えられる柔軟なAPIが必要となる。
+メタレベルの計算をノーマルレベルの計算と同等にプログラミングできると、動作するコードに対して様々なアプローチが掛けられる。
+この為にはノーマルレベル、メタレベル共にプログラミングできる言語と環境が必要となる。
+
+プログラムのノーマルレベルの計算とメタレベルの計算を一貫して行う言語として、 Continuation Based C(CbC)を用いる。
\ No newline at end of file

Binary file paper/master_paper.pdf has changed