# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1418192277 -32400
# Node ID 7ec73a287b63c87e3f8d2ff0261e02aa7398db32
# Parent  c86aa006497bc24a2ba670319b3272f97fcd2504
Writing position paper ...

diff -r c86aa006497b -r 7ec73a287b63 sigse.pdf
Binary file sigse.pdf has changed
diff -r c86aa006497b -r 7ec73a287b63 sigse.tex
--- a/sigse.tex	Wed Dec 10 12:53:10 2014 +0900
+++ b/sigse.tex	Wed Dec 10 15:17:57 2014 +0900
@@ -27,13 +27,13 @@
 %\checklines    % 行送りを確認する時に使用
 \begin{document}%{
 % 和文表題
-\title{圏によるプログラムの変更の形式化}
+\title{形式化手法とプログラミング言語の型}
 % 英文表題
-\etitle{Categorical Formalization of Program Modification}
+\etitle{Formal Methods and Types of Programming Languages}
 % 所属ラベルの定義
 \affilabel{ie-ryukyu}{琉球大学工学部情報工学科 \\ Department of Information Engineering, University of the Ryukyus.}
 % 和文著者名
-\author{比嘉 健太\affiref{ie-ryukyu}\and
+\author{比嘉 健太\affiref{ie-ryukyu} \and
         河野 真治\affiref{ie-ryukyu}}
 % 英文著者名
 \eauthor{Yasutaka Higa\affiref{ie-ryukyu}\and
@@ -41,22 +41,10 @@
 
 % 和文概要
 \begin{abstract}
-本研究ではプログラムの信頼性を保ちながら開発するための手法を提案することを目的とする．
-
-プログラムの信頼性が変化するのはプログラムの変更時である．
-プログラムの変更を表現するデータ構造 Delta を定義し，異なるバージョンのプログラムを同時に実行可能にする．
-異なるバージョン間のプログラムのトレースを比較し，信頼性の変化の指摘とデバッグの支援を行なう手法を提案する．
 
 \end{abstract}
 % 英文概要
 \begin{eabstract}
-We will propose software development method with improve reliability of program.
-
-If program modified, reliability change with relation.
-We define Delta that data structure for expression of program modification.
-Delta be able to execute program has multiple version at the same time.
-
-We propose method to visualising reliability and support debug by compare traces between different version programs.
 
 \end{eabstract}
 
@@ -67,96 +55,43 @@
 
 % 本文はここから始まる
 \section{はじめに}
-プログラムの信頼性を保ちながら開発するための手法を提案する．
-プログラムの変更時に信頼性が変化すると仮定し，圏を用いてプログラムの変更を形式化する．
-
-本研究ではプログラムの変更を Monad として表現する．
-Monad とはデータ構造とメタ計算を対応させる手法である．
-Monad として任意の異なるバージョンのプログラムを同時に実行するデータ構造 Delta を定義した．
-プログラムの変更は特定バージョンの Delta から次のバージョンの Delta への変換として記述する．
-
-ここで，任意の2つのバージョンのプログラムを同時に実行する．
-実行した際に振舞いが変化する点がバージョン間における変更点である．
-変更点を自動で検出することにより，バージョンが変わることによって信頼性の変化する部分を指摘する．
-
-\section{プログラムの変更を表す Delta}
-プログラミング言語 Haskell においてデータ構造 Delta を定義した．
-Delta は全てのバージョンの実行結果の値を保持するデータ構造である．
-値の変更は値から Delta を返す関数として定義する．
-返す Delta に内包する値を複数個持たせることにより，複数のバージョンを表現する．
+形式手法によるチェックはプログラム実装言語の処理系とユーザ間で対話的に行なわれるべきだと考える．
+特に，実装言語で記述されたプログラムから仕様との対応を処理系が判断すべきだと考える．
+なぜなら，仕様の定義に関わらず実行してはいけない処理などが存在するからである．
 
-ここで，異なるバージョン数を持つ Delta や関数の組み合せを考える．
-その際，前のバージョンの組み合せを保存しつつ新たな変更も取り入れるように組み合せる必要がある．
-バージョンの組み合せの例を図\ref{fig:versions}に示す．
-変数 variable と関数 function が存在するとする．
-variable はバージョンが2つ存在し，関数はバージョンが3つ存在する．
-これらの組み合せの中から，variableのバージョン2つを保存しつつ関数のバージョン3も含むように組み合せから値を選ぶ．
+例えば，0による除算や配列外へのアクセスはどのようなプログラムにおいても実行してはいけない．
+全てのプログラムに対して共通に持つべき仕様として定義し，処理系が自動でチェックするべきである．
+そうすることにより，仕様が全く記述されていないプログラムにおいても仕様をチェックすることができる．
 
-\begin{figure}[htpb]
-    \begin{center}
-        \scalebox{0.35}{\includegraphics{figure/versions.pdf}}
-    \end{center}
-    \caption{バージョンの組み合せの例}
-    \label{fig:versions}
-\end{figure}
+仕様は処理系におけるユーザ定義の満たすべき条件として定義する．
+基本的な満たすべき条件の拡張として記述することにより，仕様が存在するプログラムにも対応することができる．
 
-バージョンの組み合せを一意に定義するために Delta を Monad とする．
-Monad によってデータ構造とメタ計算を対応付けることができる\cite{moggi}．
-Delta におけるメタ計算とはバージョン間の組み合せを一意に決めるルールである．
-関数の実行時にメタ計算も含めて実行することにより，異なるバージョンに存在する独立した計算も全て実行することができる．
-なお，データ構造を Monad として定義する際に満たすべき Monad則が存在するが，Monad則を満たしていることは証明支援系言語Agda\cite{agda}によって証明した．
-
-プログラムをデータ構造 Delta と Delta を返す関数として記述することにより，全てのバージョンを同時に実行できるプログラムが得られる．
-ここで，バージョンとはある一意な Delta の組み合せの列として表現される．
-組み合せの列を比較することにより異なるバージョン間の比較ができると考えた．
+ここで，プログラム実装言語が自動で仕様をチェックするために必要な情報を考えたい．
+どれだけの情報をプログラムに記述すれば自動でチェックできるかは私の中ではまだはっきりしていない．
+仕様をチェックするに足る情報の量と，その情報から仕様をチェックする手法に興味がある．
 
 
-\section{任意の2つのバージョンを実行する Parallel Debugger}
-任意の2つのバージョンを同時に実行することによりデバッグを支援する手法 Parallel Debugger を提案する．
+\section{型と証明支援系言語}
+現在，私がプログラムに追加する情報として注目しているのが型である．
+
+型と論理は対応しており，証明が存在する定理は型によって表現できる．
+満たすべき性質を証明として型が記述できれば，その型は性質を満たすと言える．
+
+仕様を全て論理で記述し，対応する型を記述すると仕様を満たすプログラムが記述できると思われる．
+しかし，論理を満たす型の記述には非常に大きなコストがかかる．
 
-Delta によって表現されたプログラムの任意のバージョンを2つ選ぶ．
-2つのバージョンを同時に実行し，実行結果が変化する点を検出する．
-変化した実行結果の比較により，プログラムの変更時に混入したバグを発見できるのでは無いかと考えた．
+私は研究において関数型プログラミング言語Haskellと証明支援系プログラミング言語Agdaを利用している．
+プログラムの変更を表すことのできるデータ型を用意し，異なるバージョンのプログラム間の関係を形式化する試みである．
+この研究において，Haskell でデータ型と対応する処理を50行ほど記述した．
+そのデータ型と処理が満たすべき条件をAgdaで記述すると500行ほどとなった．
+行換算すると実装に対して仕様には10倍のコストがかかっている．
 
-さらに，2つのバージョンのうち片方を実行しつつ，もう片方はデバッグモードとして実行する．
-そうすることにより，バージョンアップ前の挙動をバージョンアップ後も保存しているか確認することができる．
-加えて，テストなどと併用することにより異なるバージョン間における信頼性や品質の比較も可能である．
+個別のプロジェクトにおいて個別のデータ型を定義し，満たすべき性質を記述するのでは非常に大きなコストがかかってしまう．
+よって，既に証明された型どうしを組み合せることによってプログラムを記述するのが望ましいと考える．
+そこで問題となるのが，証明された型のみで任意のプログラムを記述可能なのか，という点である．
 
 
-\section{まとめと課題}
-本研究ではプログラムの変更をMonadによって表現した．
-定義したデータ構造 Delta により全てのバージョンを同時に実行できることを確認した．
-Delta における特定のバージョン2つを同時に実行することにより，デバッグの支援や信頼性の比較を行なう手法 Parallel Debugger を提案した．
-
-今後の課題としては大きく3つある．
-1 つめは Delta におけるプログラムの表現能力である．
-可能なプログラムの全ての変更を Delta によって表現可能かどうか調べなくてはならない．
-この課題については Delta と他の Monad との組み合せが可能であれば可能であると考えている．
-今回 Delta を実装した Haskell においては入出力の処理が Monad として表現される．
-そのため，入出力を含めた変更は Monad との組み合せが必要になる．
-
-2 つめはDelta におけるそれぞれのバージョンのトレースを得ることである．
-異なるバージョンにおいて実行結果が変化する点を指摘するには実行結果が比較可能でなくてはいけない．
-このためにバージョンごとの実行結果やトレースを得る必要がある．
-この問題に対しても Monad との組み合せによって解決しようと考えている．
-トレースを得る Monad を定義し，そのMonadと Delta との組み合せで各バージョンのトレースを得る．
-
-3 つめは Delta を圏として表現することとその解析である．
-Monad は Kleisli圏の Kleisli Triple との対応が存在しており\cite{category}，Deltaもある圏を構築すると考えている．
-特に， Parallel Debugger は圏における Product と対応すると考えている．
-圏における他の性質から，プログラムの変更の性質の解析や他の手法を提案する．
-
-
-%}{
-
-\begin{thebibliography}{10}
-
-\bibitem{moggi} Eugenio Moggi: Notion of Computation and Monads(1991)
-\bibitem{category} Michael Barr and Charles Wells: Category Theory for Computing Science(1989)
-\bibitem{proofs-and-types} Jean-Yves Girard, Paulr Taylor, Yves Lafont: Proofs and Types(1990)
-\bibitem{agda} The Agda Wiki - Agda: \url{http://wiki.portal.chalmers.se/agda}
-
-\end{thebibliography}
+\section{まとめ}
 
 %}