--- a/paper/introduction.tex	Wed Feb 08 13:50:52 2017 +0900
+++ b/paper/introduction.tex	Wed Feb 08 14:27:06 2017 +0900
@@ -9,26 +9,28 @@
 モデル検査とはソフトウェアの全ての状態を数え上げ、その状態について仕様が常に真となることを確認する。
 モデル検査器には Promela と呼ばれる言語でモデルを記述する Spin\cite{spin} や、モデルを状態遷移系で記述する NuSMV\cite{nusmv}、C言語/C++ を記号実行する CBMC\cite{cbmc} などが存在する。
 定理証明はソフトウェアが満たすべき仕様を論理式で記述し、その論理式が恒真であることを証明する。
-定理証明を行なうことができる言語には、依存型証明を行なう Agda\cite{agda} や Coq\cite{coq} 、 ATS2\cite{ats2} などが存在する。
+定理証明を行なうことができる言語には、依存型で証明を行なう Agda\cite{agda} や Coq\cite{coq} 、 ATS2\cite{ats2} などが存在する。
 
 モデル検査器や証明でソフトウェアを検証する際、検証を行なう言語と実装に使われる言語が異なるという問題がある。
 言語が異なれば二重で同じソフトウェアを記述する必要がある上、検証に用いるソースコードは状態遷移系でプログラムを記述するなど実装コードに比べて記述が困難である。
-検証されたコードから実行可能なコードを生成可能な検証系もあるが、既存の実装に対する検証は行なえない。
+検証されたコードから実行可能なコードを生成可能な検証系もあるが、生成されたコードは検証のコードとは別の言語であったり、既存の実装に対する検証は行なえないなどの問題がある。
 そこで、当研究室では検証と実装が同一の言語で行なえる Continuation based C\cite{utah-master} 言語を開発している。
 
 Continuation based C (CbC)はC言語と似た構文を持つ言語である。
 CbC では処理の単位は関数ではなく CodeSegment という単位で行なわれる。
 CodeSegment は値を入力として受け取り出力を行なう処理単位であり、CodeSegment を接続していくことによりソフトウェアを構築していく。
 CodeSegment の接続処理はメタ計算として定義されており、実装や環境によって切り替えを行なうことができる。
-検証を行なうメタ計算を定義することにより、CodeSegment の定義を検証用に変更することなくソフトウェアの検証を行なうことができる。
+検証を行なうメタ計算を定義することにより、CodeSegment の定義を検証用に変更せずソフトウェアの検証を行なう。
 
 本論文では CbC のメタ計算として検証手法の提案と CbC の型システムの定義を行なう。
 モデル検査的な検証として、状態の数え上げを行なう有限のモデル検査と仕様の定義を CbC 自身で行なう。
-また、証明的な検証として CbC における型システムを部分型として定義する。
-部分型を利用して CbC のプログラムが証明支援系言語 Agda 上で正しく証明可能な形で定義できることを示す。
+CbC で記述された GearsOS の非破壊赤黒木に対して、メタ計算ライブラリ akasha を用いて仕様を検査する。
+また、定理証明的な検証として、 CbC のプログラムが証明支援系言語 Agda 上に証明可能な形で定義できることを示す。
+Agda 上で CbC のプログラムを記述するために、CbC の型システムを部分型を利用して定義する。
 
 
 \section{本論文の構成}
+% TODO: もう一回構成しなおし
 本論文ではまず第\ref{chapter:cbc}章で Continuation based C の解説を行なう。
 CbC を記述するプログラミングスタイルである CodeSegment と DataSegment の解説、メタ計算と状態を数え上げるメタ計算ライブラリ akasha の解説を行なう。
 次に第\ref{chapter:type}章で型システムについて取り上げる。