Binary file sigse.pdf has changed

--- a/sigse.tex	Wed Dec 10 16:28:34 2014 +0900
+++ b/sigse.tex	Wed Dec 10 16:49:10 2014 +0900
@@ -62,7 +62,15 @@
 形式手法によるチェックはプログラム実装言語の処理系とユーザ間で対話的に行なわれるべきだと考える．
 任意のプログラムに対して形式手法が適用可能であり，必要ならばユーザが制約をさらに厳しくする．
 制約の追加が対話的入力であり，反例の指摘などが対話的出力に相当する．
-対話的チェックを実現するには，実装言語が通常の処理系に加えて形式手法をサポートする必要があると考える．
+
+対話的に実行する理由は，必要とされる仕様の厳密さに柔軟に対応するためである．
+例えば，使い捨てのプログラムなどに厳密な仕様を策定するのはコストが高すぎる．
+しかし非常に単純なバグを自動で見つけるために形式手法を利用したい．
+そのバグのみを見つけるための条件を対話的な出力とし，ユーザが入力をする．
+他にも，徐々に仕様が複雑になり整理したい，といった場合なども対話的に必要な分だけ対応したい．
+そのためにも仕様が存在しないような任意のプログラムに対しても形式手法を実行したい．
+
+そのような対話的チェックを実現するには，実装言語が通常の処理系に加えて形式手法をサポートする必要があると考える．
 
 \section{形式手法をサポートした言語}
 任意のプログラムに対して形式手法を適用可能な処理系は作成できると考える．