# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1418279798 -32400
# Node ID c73b1c3d88ad7d6df03e7083eb03890af579b665
# Parent  ce6ce56bd4144c5b6d35e0905331af3af3e5fe5f
Writing position paper ....

diff -r ce6ce56bd414 -r c73b1c3d88ad sigse.pdf
Binary file sigse.pdf has changed
diff -r ce6ce56bd414 -r c73b1c3d88ad sigse.tex
--- a/sigse.tex	Thu Dec 11 12:59:57 2014 +0900
+++ b/sigse.tex	Thu Dec 11 15:36:38 2014 +0900
@@ -56,7 +56,7 @@
 
 % 本文はここから始まる
 \section{自己紹介}
-私は琉球大学工学部情報工学科に所属する四年次の学生である．
+私は琉球大学工学部情報工学科に所属する四年次の学生だ．
 自動でプログラムのバグを見付ける機構が欲しいと思い，卒業研究はそのようなテーマで取り組んでいる．
 
 研究を進めるにつれ，プログラムのバグを見付けるには仕様やテストを記述する必要があることを知った．
@@ -71,7 +71,7 @@
 アイデアを実現するために取った過程を示したい．
 
 まず， Monad とは何かを知る必要があった．
-Monad はプログラミング言語 Haskell では型クラスとして用意されており，まず型とは何かを知る必要があった．
+Monad はプログラミング言語 Haskell では型クラスとして用意されており，まず型とは何かを知ることになった．
 そこで，Proofs and Types を指導教員と読むこととなった．
 Proofs and Types では型と論理の対応について知ることができた．
 例題は証明支援系言語 Agda によって記述した．
@@ -82,11 +82,28 @@
 型の理論背景を知った後，次に Monad とは一体何か知る必要があった．
 Monad は Category Theory から computer science に持ち込まれたものであった．
 そのために Category theory を知る必要があった．
-Monad には満たすべき Monad則が存在し、Monad 則の証明も型によって Agda で記述できた。
+Monad には満たすべき Monad則が存在し，その証明も型によって Agda で記述できた．
+
+型とMonad を学んだ私は当初のアイデアであるプログラムに対する変更を Monad で表現することにした．
+Monad という指針が存在したため，プログラムの変更を定義することができた．
+結果的にプログラムの変更は変更前のプログラムと変更後のプログラムを同時に実行することで表わせた．
+
+\section{産業界に形式手法を普及するには}
+形式手法の普及に対して，私の卒業研究を通して得た知見は2つある．
+
+まず1つめは形式手法を直接用いるためには専門家が必須であることである．
+正直に言ってしまえば，指導教員の指摘が無ければ形式手法を用いる発想は出なかったであろう．
+さらに，学習のコストが高く，修得に期間がかかる．
+私は問題一つを形式化するのに一年かかった．
+それに加え，Monad によって形式化しようとする発想には必須な知識が存在する．
+どのように形式化するのかを判断できるようになるための学習コストも必要である．
+それらのコストは非常に大きく，私の経験上一年では足りないようである．
+
+2つめは，形式手法もシステムとして確立されているのなら利用しやすかったことである．
+型の理論的背景を理解せずとも，これまでにプログラムを書いた経験から型システムは問題無く利用できた．
+つまり，形式手法を直接適用するのではなく，形式化されたシステムであれば利用は比較的容易であった．
 
 
-\section{産業界に形式手法を普及するには}
-\section{わたしのりそう}
 \section{まとめ?}
 
 %}