Mercurial > hg > Papers > 2015 > atton-thesis

annotate 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
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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}
4
cc74def322a8 Add introduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 プログラムの信頼性とはプログラムが正しく動く保証性であり、信頼性は多くの原因により損なわれる。
78
6f699b37dc55 Add original number count
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
4 例えば未定義の挙動によりプログラムが停止すること、プログラム内の誤った条件式による誤った計算結果、実行環境やパラメタの変化による誤動作などがある。
71
ac56c2f84dfb Mini fixes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
5 プログラムの変更は信頼性を低下させるきっかけとなる。
78
6f699b37dc55 Add original number count
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
6 変更を形式化することでプログラムの信頼性の変化を指摘する。
4
cc74def322a8 Add introduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7
71
ac56c2f84dfb Mini fixes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
8 プログラムの変更の形式化には Monad を用いる。
54
bf136bd59e7a Add thebibliography
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 30
diff changeset
9 プログラムにおけるMonad とはデータ構造とメタ計算の対応である~\cite{Moggi:1991:NCM:116981.116984}。
78
6f699b37dc55 Add original number count
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
10 プログラムの変更をメタ計算として定義することで、プログラムの変更そのものを計算可能にする。
6f699b37dc55 Add original number count
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
11 メタ計算として信頼性の解析に利用可能な機構を定義することで、信頼性を保ちながらソフトウェアを開発できることを示す。
57
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 54
diff changeset
12 例えば、プログラムが変更された際に変更前と変更後のプログラムの挙動を比較する機構を提供できる。
78
6f699b37dc55 Add original number count
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
13 また、定義したメタ計算の Monad と対応を保証するために、メタ計算が Monad則を満たすこと証明支援系Agda~\cite{agda}により証明する。
6f699b37dc55 Add original number count
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
14 加えて他の Monad との組み合せが可能であることも証明する。
6f699b37dc55 Add original number count
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
15