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