--- a/paper/introduction.tex	Tue Feb 17 15:33:22 2015 +0900
+++ b/paper/introduction.tex	Tue Feb 17 16:11:40 2015 +0900
@@ -4,16 +4,15 @@
 本研究ではプログラムの信頼性の向上を目標とする。
 
 プログラムの信頼性とはプログラムが正しく動く保証性であり、信頼性は多くの原因により損なわれる。
-例えば仕様が未定義の挙動によってプログラムが停止することやプログラム内の誤った条件式による誤った計算結果、実行環境やパラメタの変化による誤動作などがある。
-信頼性を低下させるタイミングの一つにプログラムの変更がある。
-プログラムの変更を形式化することにより、プログラムの信頼性が損なわれる変更を定義する。
+例えば未定義の挙動によりプログラムが停止することやプログラム内の誤った条件式による誤った計算結果、実行環境やパラメタの変化による誤動作などがある。
+プログラムの変更は信頼性を低下させるきっかけとなる。
+変更を形式化することでプログラムの信頼性の変化を指摘し、プログラムの信頼性を向上させる。
 
-本研究ではプログラムの変更を Monad を用いて形式化する。
+プログラムの変更の形式化には Monad を用いる。
 プログラムにおけるMonad とはデータ構造とメタ計算の対応である~\cite{Moggi:1991:NCM:116981.116984}。
-メタ計算とは計算を実現するための計算であり、プログラムの変更をメタ計算として定義することで、プログラムの変更そのものを計算として実行することができる。
+プログラムの変更をメタ計算として定義することで、プログラムの変更そのものを計算として実行する。
 変更を計算可能にすることで、信頼性の解析に利用可能な機構を計算として定義できる。
 例えば、プログラムが変更された際に変更前と変更後のプログラムの挙動を比較する機構を提供できる。
 もし挙動の変化が望ましくない場合、信頼性が損なわれる変更だと変更時に判定できる。
 このように、プログラムの変更に対するメタ計算を定義することで信頼性を保ちながら開発することが可能となる。
-本研究ではプログラムの変更をメタ計算として定義し、Monad則を満たすことを証明する。
-%加えて、形式化した論理の観点からプログラムの変更が持つ性質などを解析し、ソフトウェア開発手法の指針を提案する。
+本研究ではプログラムの変更をメタ計算として定義し、それがMonad則を満たすことを証明する。