\chapter{プログラムの変更の形式化}
\label{chapter:introduction}
プログラムの信頼性とはプログラムが正しく動く保証性であり、信頼性は多くの原因により損なわれる。
例えば未定義の挙動によりプログラムが停止すること、プログラム内の誤った条件式による誤った計算結果、実行環境やパラメタの変化による誤動作などがある。
プログラムの変更は信頼性を低下させるきっかけとなる。
変更を形式化することでプログラムの信頼性の変化を指摘する。

プログラムの変更の形式化には Monad を用いる。
プログラムにおけるMonad とはデータ構造とメタ計算の対応である~\cite{Moggi:1991:NCM:116981.116984}。
プログラムの変更をメタ計算として定義することで、プログラムの変更そのものを計算可能にする。
メタ計算として信頼性の解析に利用可能な機構を定義することで、信頼性を保ちながらソフトウェアを開発できることを示す。
例えば、プログラムが変更された際に変更前と変更後のプログラムの挙動を比較する機構を提供できる。
また、定義したメタ計算の Monad と対応を保証するために、メタ計算が Monad則を満たすこと証明支援系Agda~\cite{agda}により証明する。
加えて他の Monad との組み合せが可能であることも証明する。