# HG changeset patch # User Yasutaka Higa # Date 1424152232 -32400 # Node ID 0cf12b73bb0271a98affd2ca68bb998dfa38b2ae # Parent b1271d62390cbdb7188c60260e7c2aa4ba3f3447 Update preprint diff -r b1271d62390c -r 0cf12b73bb02 prepaper/115763K.pdf Binary file prepaper/115763K.pdf has changed diff -r b1271d62390c -r 0cf12b73bb02 prepaper/115763K.tex --- a/prepaper/115763K.tex Tue Feb 17 14:32:40 2015 +0900 +++ b/prepaper/115763K.tex Tue Feb 17 14:50:32 2015 +0900 @@ -21,7 +21,6 @@ %% listings settings - \lstset{ frame=single, keepspaces=true, @@ -53,13 +52,14 @@ We define Delta Monad as meta computation that save behavior when modify program. Delta help to improve reliability. For example, debug method that compare traces of different versions is available. -Finally, We proved Delta Monad satisfy Monad-laws. +Finally, We proved Delta Monad satisfies Monad-laws. \end{abstract} \section{プログラムの変更の形式化} -信頼性とはプログラムが正しく動作する保証であり、プログラムのバグなど多くの原因により低下する。 -信頼性が変化する点としてプログラムの変更に注目し、プログラムの変更を Monad を用いたメタ計算として形式化する。 -加えて、定義した計算が Monad 則を満たすか証明する。 +信頼性とはプログラムが正しく動作する保証であり、バグといった原因により低下する。 +信頼性が変化する点としてプログラムの変更に注目し、プログラムの変更を形式化する。 +形式化には Monad を用い、メタ計算としてプログラムの変更を定義する。 +最後に、定義したメタ計算が Monad 則を満たすか証明する。 \section{メタ計算と Monad} プログラムを形式化するにあたり、プログラムを定義する。 @@ -88,9 +88,8 @@ \lstinputlisting[label=src:delta_instance_monad, caption= Delta に対するメタ計算の定義] {src/delta_instance_monad.hs} \end{table} -Delta Monad は全てのバージョンのプログラムを保存し、同時に実行できるメタ計算を行なう。 -プログラムはバージョンによって順序付けられているため、計算する際にバージョンが同じ関数と値を用いて関数を適用することで実現する。 -コンストラクタが Mono であった場合はバージョン1であるためバージョン1どうしの計算を行ない、バージョンが1より大きい Delta で構成される場合は、先頭のバージョンどうしを計算し、先頭を除いた形に変形してから再帰的にメタ計算を適用する。 +プログラムはバージョンによって順序付けられているため、バージョン毎に関数を適用することでメタ計算を実現する。 +コンストラクタが Mono であるバージョン1の場合はバージョン1どうしの計算を行ない、バージョンが1より大きい Delta で構成される場合は、先頭のバージョンどうしを計算し、先頭を除いた形に変形してから再帰的にメタ計算を適用する。 \section{Delta Monad を用いたプログラムの例} Delta Monad を用いて、異なるバージョンのプログラムを同時に実行した例を示す。 @@ -138,32 +137,23 @@ generator 関数と count 関数は変更が無いために Mono のままである。 変更された numberFilter 関数は、返り値の Delta のバージョンを2つにしている。 -Delta によって表現された numberCount プログラムを実行することで、2つのバージョンを同時に実行することができる。 -実行した結果がリスト\ref{src:numberCountResult}である。 +Delta によってプログラムの変更が表現できるため、2つのバージョンを含むプログラムを作成できた。 +このプログラムは全てのバージョンを同時に実行することが可能であり、実行した結果がリスト\ref{src:numberCountResult}である。 \begin{table}[html] \lstinputlisting[label=src:numberCountResult, caption= Delta によって表現されたnumberCountの実行例] {src/numberCountResult.txt} \end{table} -numberCount プログラムに対して 1000 を与えると、1 から 1000 までの中から素数の個数を数えた 168 と、偶数の個数を数えた500が得られる。 +numberCount プログラムに対して 1000 を与えると、1 から 1000 までの中から素数の個数を数えた 168 と、偶数の個数を数えた500が得られた。 このように Delta Monad によってプログラムの変更を表すことで全てのバージョンを同時に実行することが可能となる。 なお、 Delta が Monadであることを保証するMonad則を満することを証明支援言語Agda~\cite{agdawiki}によって証明した。 -\section{他の Monad との組み合せ} -Delta Monad によりプログラムの変更を表現することができた。 -ここで Delta Monad と他の Monad の組み合せを考える。 -プログラミング言語 Haskell において、入出力は Monad を介して行なわれる。 -よって入出力を行なうプログラムの変更を表現するには他の Monad と組み合わせが必須となる。 -加えて、Monad により提供される例外やロギングといったメタ計算を Delta に組込めるというメリットもある。 - -Delta Monad と他の Monad を組み合せるためにデータ型 DeltaM を定義した。 -データ型 DeltaM は内部にある Monad のメタ計算と同時にDelta Monad のメタ計算を行なう。 -例えば、DeltaM と Writer Monad を組み合せることにより、実行中の値のログ付きで全バージョン実行を行なうことができる。 -DeltaM も Monad 則を満たすことは Agda によって証明した。 - \section{まとめと課題} Delta Monad を用いてプログラムの変更を定義することができた。 -プログラムを同時に実行しながらトレースを比較することで変更を検出するなど、信頼性の向上に用いることができる。 +Delta Monad は他の Monad とも合成することが可能であり、データ型 DeltaM を定義することで Haskell における Monad 間の合成を確認できた。 +実行時のトレースや例外を表現する Monad と組み合せることで、プログラムの変更に対する解析が可能となる。 +例えば、プログラムを同時に実行しながらトレースを比較することでデバッグを支援することができる。 +他にも、全ての変更を保存する性質から、プログラムのバージョン管理システムに対して形式的な定義を与えられる。 今後の課題は大きく分けて3つある。 まず1つめはメタ計算の定義である。