\documentclass[twocolumn,twoside,9.5pt]{jarticle}
\usepackage[dvips]{graphicx}
\usepackage{picins}
\usepackage{fancyhdr}
\usepackage{listings}
\usepackage{url}
\pagestyle{fancy}
\lhead{\parpic{\includegraphics[height=1zw,keepaspectratio,bb=0 0 251 246]{pic/emblem-bitmap.pdf}}琉球大学主催 工学部情報工学科 卒業研究発表会}
\rhead{}
\cfoot{}

\setlength{\topmargin}{-1in \addtolength{\topmargin}{15mm}}
\setlength{\headheight}{0mm}
\setlength{\headsep}{5mm}
\setlength{\oddsidemargin}{-1in \addtolength{\oddsidemargin}{11mm}}
\setlength{\evensidemargin}{-1in \addtolength{\evensidemargin}{21mm}}
\setlength{\textwidth}{181mm}
\setlength{\textheight}{261mm}
\setlength{\footskip}{0mm}
\pagestyle{empty}


%% listings settings
\lstset{
  frame=single,
  keepspaces=true,
  basicstyle={\ttfamily},
  breaklines=true,
  xleftmargin=0zw,
  xrightmargin=0zw,
  framerule=.2pt,
  columns=[l]{fullflexible},
  language={},
  tabsize=4,
  lineskip=-0.5zw,
  escapechar={@},
}
\def\lstlistingname{リスト}


\begin{document}
\title{Categorical Formalization of Program Modification}
\author{115763K 氏名 {比嘉}{健太} 指導教員 : 河野真治}
\date{}
\maketitle
\thispagestyle{fancy}

\begin{abstract}
Formalization of program modification is proposed.
Series of source code version are represented as List like structured Monad as meta computation.
Using this Delta Monad, we can make reliable program development possible.
For example, comparing traces of different versions is performed in Haskell.
\end{abstract}

\section{プログラムの変更の形式化}
プログラムの変更そのものを計算に対するプログラミング、つまり、メタ計算として形式化する手法を提案する。
メタ計算の形式化としては、Monad を使う手法がMoggi~\cite{Moggi:1991:NCM:116981.116984}などにより提案されている。
ここではプログラムの複数のバージョンを持つデータ構造Deltaを使用する。
Delta がMonadであることを証明支援系 Agda~\cite{agdawiki}を用いて証明した。

ここではプログラムは関数の集合であり、プログラムの変更は関数の定義の変更となる。
それぞれの変更はMonadに格納されるために型が整合している必要がある。
Delta Monad により、信頼性が変化する点としてのプログラムの変更を形式化することができた。
例えば、プログラムの異なるバージョンを同時に実行し、そのトレースをMonadを用いて比較することが可能である。

\section{変更を表す Delta Monad}
Delta Monad では変更単位をバージョンとし、全てのバージョンを保存する。
Delta Monad をプログラミング言語 Haskell において実装し、異なるバージョンのプログラムを同時に実行する。

まずは、Delta Monad と対応するデータ型 Delta を定義する(リスト\ref{src:delta_data})。

\begin{table}[html]
    \lstinputlisting[label=src:delta_data, caption= Delta のデータ定義] {src/delta_data.hs}
\end{table}

バージョンが1である値はコンストラクタ Mono によって構成し、複数のバージョンを持つ場合はコンストラクタ Delta により構成する。
このようにプログラムの変更を記述することで、バージョンによって順序付けられたリストが構成される。

リスト\ref{src:delta_instance_monad}に Delta 型と関連付けるメタ計算を示す。

\begin{table}[html]
    \lstinputlisting[label=src:delta_instance_monad, caption= Delta に対するメタ計算の定義] {src/delta_instance_monad.hs}
\end{table}

プログラムはバージョンによって順序付けられているため、バージョン毎に関数を適用することでメタ計算を実現する。
コンストラクタが Mono であるバージョン1の場合はバージョン1どうしの計算を行ない、バージョンが1より大きい Delta である場合は、再帰的にバージョンを下げながら計算を行なう。

\section{Delta Monad を用いたプログラムの例}
Delta Monad を用いて、異なるバージョンのプログラムを同時に実行する例を示す。

まずは変更の対象となる numberCount プログラムのバージョン1を示す(リスト\ref{src:numberCountV1})。

\begin{table}[html]
    \lstinputlisting[label=src:numberCountV1,
                     caption= numberCount プログラムバージョン1,
                     basicstyle={\small}] {src/numberCount1.hs}
\end{table}

numberCount プログラムは、1 から n の整数において特定の数の個数を数えるプログラムである。
プログラムは3つの関数によって表現される。

{\tt generator} :
n を取り、1からnまでの整数のリストを返す

{\tt numberFilter} :
整数のリストを取り、特定の性質を持つ数のみを残す。
バージョン1では素数のみを残す。

{\tt count} :
整数のリストを取り、その個数を数える。

次に、numberCount プログラムを変更する。
変更点は numberFilter 関数の抽出条件とし、素数判定による抽出から偶数判定による抽出に変更する。
変更した結果をリスト\ref{src:numberCountV2}に示す。
なお、変更部分は下線の部分である。

\begin{table}[html]
    \lstinputlisting[label=src:numberCountV2,
                     caption= numberCount プログラムバージョン2,
                     basicstyle={\small}] {src/numberCount2.hs}
\end{table}

numberCount プログラムとその変更を Delta Monad によって記述する(リスト\ref{src:numberCountDelta})。
Delta Monad によって変更を記述したプログラムは全ての値が Delta 型であり、全ての関数はDelta型の値を返す。

\begin{table}[html]
    \lstinputlisting[label=src:numberCountDelta, caption= Delta を用いて記述した numberCount プログラム,
                     basicstyle={\footnotesize}] {src/numberCountDelta.hs}
\end{table}

generator 関数と count 関数は変更が無いために Mono のままである。
変更された numberFilter 関数は、返り値の Delta のバージョンを2つにしている。

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が得られた。
このように Delta Monad によってプログラムの変更を表すことで全てのバージョンを同時に実行可能となる。

\section{まとめと課題}
Delta Monad を用いてプログラムの変更を定義し、異なるバージョンのプログラムを同時に実行することができた。

また、Delta Monad は他の Monad とも合成が可能であることも証明した。
実行時のトレースや例外を表現する Monad と組み合せることで、プログラムの変更に対する解析が可能となる。
Monad と合成することにより、プログラムを同時に実行しながらトレースを比較することが可能となり、デバッグを支援できる。
なお、 Haskell においてデータ型 DeltaM を定義することで Monad を合成し、トレースを得ながら異なるバージョンのプログラムを同時に実行することができた。

今後の課題は Delta Monad におけるプログラムの変更範囲の定義である。
Delta Monad において表現可能な変更の範囲が全ての変更を含むか証明する。
もしくは、Delta Monad により表現できる変更の範囲を定義する。
次に、 Monad を通した圏における解釈がある。
バージョンの組み合せは product に、全てのバージョンを保存している Delta は colimit に対応すると考えている。
また、全ての変更を保存する性質から、プログラムのバージョン管理システムに対して形式的な定義を与えられると考えている。

\nocite{Girard:1989:PT:64805, opac-b1092711, BarrM:cattcs, JonesDuponcheel93}
\thispagestyle{fancy}

\bibliographystyle{jplain}
\bibliography{reference}

\end{document}