# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1418194149 -32400
# Node ID 33ab1d8af5dc78b92d0cf546ae35bd5111a28895
# Parent  2ab39686323ad018c8f93b83c47d853f4ad89e89
Writing position paper .....

diff -r 2ab39686323a -r 33ab1d8af5dc sigse.tex
--- a/sigse.tex	Wed Dec 10 15:33:51 2014 +0900
+++ b/sigse.tex	Wed Dec 10 15:49:09 2014 +0900
@@ -91,9 +91,18 @@
 個別のプロジェクトにおいて個別のデータ型を定義し，満たすべき性質を記述するのでは非常に大きなコストがかかってしまう．
 よって，既に証明された型どうしを組み合せることによってプログラムを記述するのが望ましいと考える．
 そこで問題となるのが，証明された型のみで任意のプログラムを記述可能なのか，という点である．
-
+これは、型がプログラムに加えている制約の強さの問題でもある。
+任意のプログラムに対して形式手法が適用可能な処理系を考えた際に、どの程度の制約が必要なのかも考えなくてはならない。
 
 \section{まとめ}
+私は形式的手法は実行可能なプログラムに対して処理系と対話的に行なうべきものだと考えている。
+仕様が定まっていなくとも満たすべき条件は存在し、それはどのプログラムにも共通と言って良い。
+さらに、具体的な仕様が決まるのならば拡張として定義していく。
+
+対話的に形式的手法を実行するためには実行可能プログラムの処理系が形式的手法をサポートする必要がある。
+そのためにプログラムに加えるべき情報と制約に興味がある。
+特に、現在は型の情報と制約について調べている。
+私としては情報量は十分だが制約が強すぎるのではないかと考えている。
 
 %}