\chapter{プログラムの変更の形式化}
\label{chapter:introduction}

本研究ではプログラムの信頼性の向上を目標とする。

プログラムの信頼性とはプログラムが正しく動く保証性であり、信頼性は多くの原因により損なわれる。
例えば仕様が未定義の挙動によってプログラムが停止したり、プログラム内の誤った条件式により計算結果が仕様と異なったり、実行環境やパラメタが変化した際に望まない動作が発生することなどがある。
信頼性を低下させる原因が増えるタイミングの多くはプログラムを変更した時である。
よって、プログラムの変更を形式化することにより、プログラムの信頼性が損なわれる変更を定義する。

本研究ではプログラムの変更を Monad を用いて形式化する。
プログラムにおけるMonad とはデータ構造とメタ計算の対応である。
メタ計算とは計算を実現するための計算であり、プログラムの変更をメタ計算として定義することで、プログラムの変更そのものを計算として実行することができる。
例えば、プログラムが変更された際に変更前と変更後のプログラムの挙動を比較する機構を考える。
もし挙動の変化が望ましくない場合、信頼性が損なわれる変更だと判定できる。
このように、プログラムの変更に対するメタ計算を定義することで信頼性を保ちながら開発するための手法を提案する。
加えて、形式化した論理の観点からプログラムの変更が持つ性質などを解析し、ソフトウェア開発手法の指針を提案する。