# HG changeset patch # User Yasutaka Higa # Date 1424157100 -32400 # Node ID ac56c2f84dfba5d89a5d8eb838bc6a445644ac76 # Parent f44cabf175b33f0b2d3679044615aa5f9aec4f49 Mini fixes diff -r f44cabf175b3 -r ac56c2f84dfb paper/delta.tex --- a/paper/delta.tex Tue Feb 17 15:33:22 2015 +0900 +++ b/paper/delta.tex Tue Feb 17 16:11:40 2015 +0900 @@ -1,7 +1,7 @@ \chapter{プログラムの変更を表現する Delta Monad} \label{chapter:delta} -本研究では Monad によりプログラムの変更を定義する。 +Monad を用いてプログラムの変更を形式化していく。 第\ref{chapter:delta}章ではプログラムの変更を表す Delta Monad を定義し、その使用例とメタ計算の例を示す。 なお、Monad についての定義と解説は第\ref{chapter:category}章と第\ref{chapter:functional_programming}章にて行なう。 diff -r f44cabf175b3 -r ac56c2f84dfb paper/introduction.tex --- a/paper/introduction.tex Tue Feb 17 15:33:22 2015 +0900 +++ b/paper/introduction.tex Tue Feb 17 16:11:40 2015 +0900 @@ -4,16 +4,15 @@ 本研究ではプログラムの信頼性の向上を目標とする。 プログラムの信頼性とはプログラムが正しく動く保証性であり、信頼性は多くの原因により損なわれる。 -例えば仕様が未定義の挙動によってプログラムが停止することやプログラム内の誤った条件式による誤った計算結果、実行環境やパラメタの変化による誤動作などがある。 -信頼性を低下させるタイミングの一つにプログラムの変更がある。 -プログラムの変更を形式化することにより、プログラムの信頼性が損なわれる変更を定義する。 +例えば未定義の挙動によりプログラムが停止することやプログラム内の誤った条件式による誤った計算結果、実行環境やパラメタの変化による誤動作などがある。 +プログラムの変更は信頼性を低下させるきっかけとなる。 +変更を形式化することでプログラムの信頼性の変化を指摘し、プログラムの信頼性を向上させる。 -本研究ではプログラムの変更を Monad を用いて形式化する。 +プログラムの変更の形式化には Monad を用いる。 プログラムにおけるMonad とはデータ構造とメタ計算の対応である~\cite{Moggi:1991:NCM:116981.116984}。 -メタ計算とは計算を実現するための計算であり、プログラムの変更をメタ計算として定義することで、プログラムの変更そのものを計算として実行することができる。 +プログラムの変更をメタ計算として定義することで、プログラムの変更そのものを計算として実行する。 変更を計算可能にすることで、信頼性の解析に利用可能な機構を計算として定義できる。 例えば、プログラムが変更された際に変更前と変更後のプログラムの挙動を比較する機構を提供できる。 もし挙動の変化が望ましくない場合、信頼性が損なわれる変更だと変更時に判定できる。 このように、プログラムの変更に対するメタ計算を定義することで信頼性を保ちながら開発することが可能となる。 -本研究ではプログラムの変更をメタ計算として定義し、Monad則を満たすことを証明する。 -%加えて、形式化した論理の観点からプログラムの変更が持つ性質などを解析し、ソフトウェア開発手法の指針を提案する。 +本研究ではプログラムの変更をメタ計算として定義し、それがMonad則を満たすことを証明する。 diff -r f44cabf175b3 -r ac56c2f84dfb paper/main.pdf Binary file paper/main.pdf has changed diff -r f44cabf175b3 -r ac56c2f84dfb paper/main.tex --- a/paper/main.tex Tue Feb 17 15:33:22 2015 +0900 +++ b/paper/main.tex Tue Feb 17 16:11:40 2015 +0900 @@ -18,6 +18,18 @@ \belongto{琉球大学工学部情報工学科} \author{115763K 比嘉健太 \\ 指導教員 {河野真治} } +% TODO +% 卒論の修正点 +% T Aの A の解説 +% A が未定義 +% 式2.1 が未定義式っぽい +% 実行例で Delta を使わないのも出す +% 可能な変更の一覧 +% bibliograph +% agda, hg, git +% ソフトウェアのバージョンにする +% where の解説が欲しい + %% %% プリアンブルに記述 diff -r f44cabf175b3 -r ac56c2f84dfb prepaper/115763K.pdf Binary file prepaper/115763K.pdf has changed diff -r f44cabf175b3 -r ac56c2f84dfb prepaper/115763K.tex --- a/prepaper/115763K.tex Tue Feb 17 15:33:22 2015 +0900 +++ b/prepaper/115763K.tex Tue Feb 17 16:11:40 2015 +0900 @@ -78,9 +78,9 @@ \lstinputlisting[label=src:delta_data, caption= Delta のデータ定義] {src/delta_data.hs} \end{table} -バージョンが1である値はコンストラクタ Mono によって構成され、複数のバージョンを持つ場合はコンストラクタ Delta により構成される。 -よって、最初のプログラムにおける値は Mono で構成され、値の変更を行なう時は Delta を追加することで表現する。 -そのためバージョンによって順序付けられたリストが構成される。 +バージョンが1である値はコンストラクタ Mono によって構成し、複数のバージョンを持つ場合はコンストラクタ Delta により構成する。 +よって、最初のプログラムにおける値は Mono で、値の変更は Delta を追加することで表現する。 +このようにプログラムの変更を記述することで、バージョンによって順序付けられたリストが構成される。 リスト\ref{src:delta_instance_monad}に Delta 型と関連付けるメタ計算を示す。 @@ -110,7 +110,7 @@ {\tt numberFilter} : 整数のリストを取り、特定の性質を持つ数のみを残す。 -バージョン1では素数の数のみを残す。 +バージョン1では素数のみを残す。 {\tt count} : 整数のリストを取り、その個数を数える。