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

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

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

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