Mercurial > hg > Papers > 2015 > atton-thesis

comparison prepaper/115763K.tex @ 68:b1271d62390c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Mini fixes
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 17 Feb 2015 14:32:40 +0900
parents 4f7137c0ea15
children 0cf12b73bb02
comparison
equal deleted inserted replaced
67:b5c04cca699b 68:b1271d62390c
47 \thispagestyle{fancy} 47 \thispagestyle{fancy}
48 48
49 \begin{abstract} 49 \begin{abstract}
50 Reliability of program reduced by many factors. 50 Reliability of program reduced by many factors.
51 Generally, reliability changes due to modification. 51 Generally, reliability changes due to modification.
52 We formalize modification of program through Monad. 52 We formalize modification of program using Monad.
53 We define Delta Monad as meta computation that save behavior when modify program. 53 We define Delta Monad as meta computation that save behavior when modify program.
54 Delta help to improve reliability. 54 Delta help to improve reliability.
55 For example, debug method that compare traces of different versions is available. 55 For example, debug method that compare traces of different versions is available.
56 Finally, We proved Delta Monad satisfy Monad-laws. 56 Finally, We proved Delta Monad satisfy Monad-laws.
57 \end{abstract} 57 \end{abstract}
58 58
59 \section{プログラムの変更の形式化} 59 \section{プログラムの変更の形式化}
60 本研究はプログラムの信頼性を向上させることを目的とする。
61 信頼性とはプログラムが正しく動作する保証であり、プログラムのバグなど多くの原因により低下する。 60 信頼性とはプログラムが正しく動作する保証であり、プログラムのバグなど多くの原因により低下する。
62 信頼性が変化する点としてプログラムの変更に注目し、プログラムの変更を Monad を用いたメタ計算として形式化する。 61 信頼性が変化する点としてプログラムの変更に注目し、プログラムの変更を Monad を用いたメタ計算として形式化する。
63 加えて、定義した計算が Monad 則を満たすか証明する。 62 加えて、定義した計算が Monad 則を満たすか証明する。
64 63
65 \section{メタ計算と Monad} 64 \section{メタ計算と Monad}
66 プログラムを形式化するにあたり、プログラムを定義する。 65 プログラムを形式化するにあたり、プログラムを定義する。
67 プログラムの要素は型付けされた値と関数により定義され、関数は値から値への写像を行なう。 66 プログラムの要素は型付けされた値と関数により定義され、関数は値から値への写像を行なう。
68 プログラムの実行は関数の適用として表される。 67 プログラムの実行は関数の適用として表わされる。
69 この時、入出力といった値の写像のみで表現できない計算を表現するために Monad を用いる。 68 この時、入出力といった値の写像で表現できない計算は Monad を用いいたメタ計算とすることで解決できる~\cite{Moggi:1991:NCM:116981.116984}。
70 プログラムにおける Monad とはデータ構造とメタ計算の関連付けであり、メタ計算とは計算を行なう計算である ~\cite{Moggi:1991:NCM:116981.116984}。
71 メタ計算として入出力機構をプログラムの計算とは別に定義し、入出力を利用したい関数は値をメタ計算と関連付けられたデータ型へと写像することで実現する。
72 Monad を用いることでプログラムの内部ではメタ計算を扱わずにメタ計算を実現できる。
73 69
74 \section{変更を表す Delta Monad} 70 \section{変更を表す Delta Monad}
75 本研究ではプログラムの変更を表すメタ計算として、変更時に過去のプログラムも保存するメタ計算を提案する。 71 プログラムの変更を表すメタ計算として、変更時に過去のプログラムも保存する Delta Monad を提案する。
76 このメタ計算に対応する Monad として Delta Monad を定義し、プログラミング言語 Haskell にて実装する。
77 Delta Monad では変更単位をバージョンとし、全てのバージョンを保存しつつ実行することができる。 72 Delta Monad では変更単位をバージョンとし、全てのバージョンを保存しつつ実行することができる。
73 Delta Monad をプログラミング言語 Haskell において実装し、異なるバージョンのプログラムを同時に実行する。
74
78 まずは、Delta Monad と対応するデータ型 Delta を定義する(リスト\ref{src:delta_data})。 75 まずは、Delta Monad と対応するデータ型 Delta を定義する(リスト\ref{src:delta_data})。
79 76
80 \begin{table}[html] 77 \begin{table}[html]
81 \lstinputlisting[label=src:delta_data, caption= Delta のデータ定義] {src/delta_data.hs} 78 \lstinputlisting[label=src:delta_data, caption= Delta のデータ定義] {src/delta_data.hs}
82 \end{table} 79 \end{table}
94 Delta Monad は全てのバージョンのプログラムを保存し、同時に実行できるメタ計算を行なう。 91 Delta Monad は全てのバージョンのプログラムを保存し、同時に実行できるメタ計算を行なう。
95 プログラムはバージョンによって順序付けられているため、計算する際にバージョンが同じ関数と値を用いて関数を適用することで実現する。 92 プログラムはバージョンによって順序付けられているため、計算する際にバージョンが同じ関数と値を用いて関数を適用することで実現する。
96 コンストラクタが Mono であった場合はバージョン1であるためバージョン1どうしの計算を行ない、バージョンが1より大きい Delta で構成される場合は、先頭のバージョンどうしを計算し、先頭を除いた形に変形してから再帰的にメタ計算を適用する。 93 コンストラクタが Mono であった場合はバージョン1であるためバージョン1どうしの計算を行ない、バージョンが1より大きい Delta で構成される場合は、先頭のバージョンどうしを計算し、先頭を除いた形に変形してから再帰的にメタ計算を適用する。
97 94
98 \section{Delta Monad を用いたプログラムの例} 95 \section{Delta Monad を用いたプログラムの例}
99 Delta Monad を用いてプログラムの変更を記述する。 96 Delta Monad を用いて、異なるバージョンのプログラムを同時に実行した例を示す。
100 97
101 まずは変更の対象となるプログラム numberCount を示す(リスト\ref{src:numberCountV1})。 98 まずは変更の対象となる numberCount プログラムのバージョン1を示す(リスト\ref{src:numberCountV1})。
102 99
103 \begin{table}[html] 100 \begin{table}[html]
104 \lstinputlisting[label=src:numberCountV1, 101 \lstinputlisting[label=src:numberCountV1,
105 caption= numberCount プログラムバージョン1, 102 caption= numberCount プログラムバージョン1,
106 basicstyle={\small}] {src/numberCount1.hs} 103 basicstyle={\small}] {src/numberCount1.hs}
107 \end{table} 104 \end{table}
108 105
109 numberCount プログラムは、1 から n の整数において特定の数の個数を数えるプログラムである。 106 numberCount プログラムは、1 から n の整数において特定の数の個数を数えるプログラムである。
110 プログラムは3つの関数によって表現される。 107 プログラムは3つの関数によって表現される。
111 \begin{itemize}
112 \item generator
113 108
114 n を取り、1からnまでの整数のリストを返す 109 {\tt generator} :
110 n を取り、1からnまでの整数のリストを返す
115 111
116 \item numberFilter 112 {\tt numberFilter} :
113 整数のリストを取り、特定の性質を持つ数のみを残す。
114 バージョン1では素数の数のみを残す。
117 115
118 整数のリストを取り、特定の性質を持つ数のみを残す。 116 {\tt count} :
119 バージョン1では素数の数のみを残す。 117 整数のリストを取り、その個数を数える。
120
121 \item count
122
123 整数のリストを取り、その個数を数える。
124
125 \end{itemize}
126
127 118
128 次に、numberCount プログラムを変更する。 119 次に、numberCount プログラムを変更する。
129 変更点は numberFilter 関数の抽出条件とし、素数判定による抽出から偶数判定による抽出に変更する。 120 変更点は numberFilter 関数の抽出条件とし、素数判定による抽出から偶数判定による抽出に変更する。
130 変更した結果をリスト\ref{src:numberCountV2}に示す。 121 変更した結果をリスト\ref{src:numberCountV2}に示す。
131 なお、変更部分は下線の部分である。 122 なお、変更部分は下線の部分である。
154 \lstinputlisting[label=src:numberCountResult, caption= Delta によって表現されたnumberCountの実行例] {src/numberCountResult.txt} 145 \lstinputlisting[label=src:numberCountResult, caption= Delta によって表現されたnumberCountの実行例] {src/numberCountResult.txt}
155 \end{table} 146 \end{table}
156 147
157 numberCount プログラムに対して 1000 を与えると、1 から 1000 までの中から素数の個数を数えた 168 と、偶数の個数を数えた500が得られる。 148 numberCount プログラムに対して 1000 を与えると、1 から 1000 までの中から素数の個数を数えた 168 と、偶数の個数を数えた500が得られる。
158 このように Delta Monad によってプログラムの変更を表すことで全てのバージョンを同時に実行することが可能となる。 149 このように Delta Monad によってプログラムの変更を表すことで全てのバージョンを同時に実行することが可能となる。
159 なお、 Delta が Monadであることを保証するMonad則を満たすることは証明支援言語Agda~\cite{agdawiki}によって証明した。 150 なお、 Delta が Monadであることを保証するMonad則を満することを証明支援言語Agda~\cite{agdawiki}によって証明した。
160 151
161 \section{他の Monad との組み合せ} 152 \section{他の Monad との組み合せ}
162 Delta Monad によりプログラムの変更を表現することができた。 153 Delta Monad によりプログラムの変更を表現することができた。
163 ここで Delta Monad と他の Monad の組み合せを考える。 154 ここで Delta Monad と他の Monad の組み合せを考える。
164 プログラミング言語 Haskell において、入出力は Monad を介して行なわれる。 155 プログラミング言語 Haskell において、入出力は Monad を介して行なわれる。