--- a/paper/introduction.tex	Wed Feb 18 11:10:19 2015 +0900
+++ b/paper/introduction.tex	Wed Feb 18 12:26:17 2015 +0900
@@ -1,18 +1,15 @@
 \chapter{プログラムの変更の形式化}
 \label{chapter:introduction}
-
-本研究ではプログラムの信頼性の向上を目標とする。
-
 プログラムの信頼性とはプログラムが正しく動く保証性であり、信頼性は多くの原因により損なわれる。
-例えば未定義の挙動によりプログラムが停止することやプログラム内の誤った条件式による誤った計算結果、実行環境やパラメタの変化による誤動作などがある。
+例えば未定義の挙動によりプログラムが停止すること、プログラム内の誤った条件式による誤った計算結果、実行環境やパラメタの変化による誤動作などがある。
 プログラムの変更は信頼性を低下させるきっかけとなる。
-変更を形式化することでプログラムの信頼性の変化を指摘し、プログラムの信頼性を向上させる。
+変更を形式化することでプログラムの信頼性の変化を指摘する。
 
 プログラムの変更の形式化には Monad を用いる。
 プログラムにおけるMonad とはデータ構造とメタ計算の対応である~\cite{Moggi:1991:NCM:116981.116984}。
-プログラムの変更をメタ計算として定義することで、プログラムの変更そのものを計算として実行する。
-変更を計算可能にすることで、信頼性の解析に利用可能な機構を計算として定義できる。
+プログラムの変更をメタ計算として定義することで、プログラムの変更そのものを計算可能にする。
+メタ計算として信頼性の解析に利用可能な機構を定義することで、信頼性を保ちながらソフトウェアを開発できることを示す。
 例えば、プログラムが変更された際に変更前と変更後のプログラムの挙動を比較する機構を提供できる。
-もし挙動の変化が望ましくない場合、信頼性が損なわれる変更だと変更時に判定できる。
-このように、プログラムの変更に対するメタ計算を定義することで信頼性を保ちながら開発することが可能となる。
-本研究ではプログラムの変更をメタ計算として定義し、それがMonad則を満たすこと証明支援系Agda~\cite{agda}により証明する。
+また、定義したメタ計算の Monad と対応を保証するために、メタ計算が Monad則を満たすこと証明支援系Agda~\cite{agda}により証明する。
+加えて他の Monad との組み合せが可能であることも証明する。
+