Mercurial > hg > Papers > 2015 > atton-thesis
annotate paper/introduction.tex @ 71:ac56c2f84dfb
Mini fixes
| author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 17 Feb 2015 16:11:40 +0900 |
| parents | 1181b4facaf9 |
| children | 0286bbcb59af |
| rev | line source |
|---|---|
|
30
67d79c18a276
Update description and delta definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
11
diff
changeset
|
1 \chapter{プログラムの変更の形式化} |
|
11
76ce5bb18092
Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
4
diff
changeset
|
2 \label{chapter:introduction} |
|
76ce5bb18092
Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
4
diff
changeset
|
3 |
| 4 | 4 本研究ではプログラムの信頼性の向上を目標とする。 |
| 5 | |
| 6 プログラムの信頼性とはプログラムが正しく動く保証性であり、信頼性は多くの原因により損なわれる。 | |
| 71 | 7 例えば未定義の挙動によりプログラムが停止することやプログラム内の誤った条件式による誤った計算結果、実行環境やパラメタの変化による誤動作などがある。 |
| 8 プログラムの変更は信頼性を低下させるきっかけとなる。 | |
| 9 変更を形式化することでプログラムの信頼性の変化を指摘し、プログラムの信頼性を向上させる。 | |
| 4 | 10 |
| 71 | 11 プログラムの変更の形式化には Monad を用いる。 |
|
54
bf136bd59e7a
Add thebibliography
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
30
diff
changeset
|
12 プログラムにおけるMonad とはデータ構造とメタ計算の対応である~\cite{Moggi:1991:NCM:116981.116984}。 |
| 71 | 13 プログラムの変更をメタ計算として定義することで、プログラムの変更そのものを計算として実行する。 |
| 57 | 14 変更を計算可能にすることで、信頼性の解析に利用可能な機構を計算として定義できる。 |
| 15 例えば、プログラムが変更された際に変更前と変更後のプログラムの挙動を比較する機構を提供できる。 | |
| 16 もし挙動の変化が望ましくない場合、信頼性が損なわれる変更だと変更時に判定できる。 | |
| 17 このように、プログラムの変更に対するメタ計算を定義することで信頼性を保ちながら開発することが可能となる。 | |
| 71 | 18 本研究ではプログラムの変更をメタ計算として定義し、それがMonad則を満たすことを証明する。 |