Mercurial > hg > Papers > 2015 > atton-thesis

comparison paper/introduction.tex @ 78:6f699b37dc55

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add original number count
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Wed, 18 Feb 2015 12:26:17 +0900
parents 0286bbcb59af
children
comparison
equal deleted inserted replaced
77:ce7701e4a308 78:6f699b37dc55
1 \chapter{プログラムの変更の形式化} 1 \chapter{プログラムの変更の形式化}
2 \label{chapter:introduction} 2 \label{chapter:introduction}
3
4 本研究ではプログラムの信頼性の向上を目標とする。
5
6 プログラムの信頼性とはプログラムが正しく動く保証性であり、信頼性は多くの原因により損なわれる。 3 プログラムの信頼性とはプログラムが正しく動く保証性であり、信頼性は多くの原因により損なわれる。
7 例えば未定義の挙動によりプログラムが停止することやプログラム内の誤った条件式による誤った計算結果、実行環境やパラメタの変化による誤動作などがある。 4 例えば未定義の挙動によりプログラムが停止すること、プログラム内の誤った条件式による誤った計算結果、実行環境やパラメタの変化による誤動作などがある。
8 プログラムの変更は信頼性を低下させるきっかけとなる。 5 プログラムの変更は信頼性を低下させるきっかけとなる。
9 変更を形式化することでプログラムの信頼性の変化を指摘し、プログラムの信頼性を向上させる。 6 変更を形式化することでプログラムの信頼性の変化を指摘する。
10 7
11 プログラムの変更の形式化には Monad を用いる。 8 プログラムの変更の形式化には Monad を用いる。
12 プログラムにおけるMonad とはデータ構造とメタ計算の対応である~\cite{Moggi:1991:NCM:116981.116984}。 9 プログラムにおけるMonad とはデータ構造とメタ計算の対応である~\cite{Moggi:1991:NCM:116981.116984}。
13 プログラムの変更をメタ計算として定義することで、プログラムの変更そのものを計算として実行する。 10 プログラムの変更をメタ計算として定義することで、プログラムの変更そのものを計算可能にする。
14 変更を計算可能にすることで、信頼性の解析に利用可能な機構を計算として定義できる。 11 メタ計算として信頼性の解析に利用可能な機構を定義することで、信頼性を保ちながらソフトウェアを開発できることを示す。
15 例えば、プログラムが変更された際に変更前と変更後のプログラムの挙動を比較する機構を提供できる。 12 例えば、プログラムが変更された際に変更前と変更後のプログラムの挙動を比較する機構を提供できる。
16 もし挙動の変化が望ましくない場合、信頼性が損なわれる変更だと変更時に判定できる。 13 また、定義したメタ計算の Monad と対応を保証するために、メタ計算が Monad則を満たすこと証明支援系Agda~\cite{agda}により証明する。
17 このように、プログラムの変更に対するメタ計算を定義することで信頼性を保ちながら開発することが可能となる。 14 加えて他の Monad との組み合せが可能であることも証明する。
18 本研究ではプログラムの変更をメタ計算として定義し、それがMonad則を満たすこと証明支援系Agda~\cite{agda}により証明する。 15