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