# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1418195881 -32400
# Node ID afdab6523b428c1a641cc9caf1f7c8e0e2437112
# Parent  33ab1d8af5dc78b92d0cf546ae35bd5111a28895
Wrote position paper

diff -r 33ab1d8af5dc -r afdab6523b42 sigse.pdf
Binary file sigse.pdf has changed
diff -r 33ab1d8af5dc -r afdab6523b42 sigse.tex
--- a/sigse.tex	Wed Dec 10 15:49:09 2014 +0900
+++ b/sigse.tex	Wed Dec 10 16:18:01 2014 +0900
@@ -27,7 +27,7 @@
 %\checklines    % 行送りを確認する時に使用
 \begin{document}%{
 % 和文表題
-\title{形式化手法とプログラミング言語の型}
+\title{形式手法とプログラミング言語の型}
 % 英文表題
 \etitle{Formal Methods and Types of Programming Languages}
 % 所属ラベルの定義
@@ -41,11 +41,15 @@
 
 % 和文概要
 \begin{abstract}
-
+任意のプログラムに対して形式手法が適用可能であるべきであると考える．
+そのために，任意のプログラムに対して対話的に形式手法が適用可能な処理系を考えたい．
+その処理系が実行するプログラムに記述するべき情報量とプログラムに対する制約の強度について興味がある．
 \end{abstract}
 % 英文概要
 \begin{eabstract}
-
+I think any program must be check by formal methods.
+I want to programming language executer that applicative formal methods to any program interactively.
+I interest constraints of program and amounts of information that enough for formal methods.
 \end{eabstract}
 
 % 表題などの出力
@@ -56,17 +60,17 @@
 % 本文はここから始まる
 \section{はじめに}
 形式手法によるチェックはプログラム実装言語の処理系とユーザ間で対話的に行なわれるべきだと考える．
-任意のプログラムに対して形式的手法が適用可能であり，必要ならばユーザが制約をさらに厳しくする．
+任意のプログラムに対して形式手法が適用可能であり，必要ならばユーザが制約をさらに厳しくする．
 制約の追加が対話的入力であり，反例の指摘などが対話的出力に相当する．
-対話的チェックを実現するには，実装言語が通常の処理系に加えて形式的手法をサポートする必要があると考える．
+対話的チェックを実現するには，実装言語が通常の処理系に加えて形式手法をサポートする必要があると考える．
 
-\section{形式的手法をサポートした言語}
-任意のプログラムに対して形式的手法を適用可能な処理系は作成できると考える．
+\section{形式手法をサポートした言語}
+任意のプログラムに対して形式手法を適用可能な処理系は作成できると考える．
 なぜなら，アプリケーションの仕様に関わらず実行してはいけない処理などが存在するからである．
 
 例えば，0による除算や配列外へのアクセスはどのようなプログラムにおいても実行してはいけない．
 よって，全てのプログラムが共通に持つべき仕様として定義可能である．
-処理系が仕様のチェック機構を持つことにより，全てのプログラムに対して形式的手法が導入可能となる．
+処理系が仕様のチェック機構を持つことにより，全てのプログラムに対して形式手法が導入可能となる．
 仕様はユーザ定義の満たすべき条件として定義する．
 基本的な満たすべき条件の拡張として記述することにより，仕様が存在するプログラムにも対応することができる．
 
@@ -87,22 +91,25 @@
 この研究において，Haskell でデータ型と対応する処理を50行ほど記述した．
 そのデータ型と処理が満たすべき条件をAgdaで記述すると500行ほどとなった．
 行換算すると実装に対して仕様には10倍のコストがかかっている．
+Agda では非常に単純な性質は自動で導くが，ほとんどの性質は自ら記述する．
+Agda が行なうのは，性質を満たしているかのチェックと満たすべき性質が必要とする性質の指摘である．
+Agda によって性質を記述すると，性質の詳細や依存関係は明確になるが，性質を直接解くコストは必須である．
 
 個別のプロジェクトにおいて個別のデータ型を定義し，満たすべき性質を記述するのでは非常に大きなコストがかかってしまう．
 よって，既に証明された型どうしを組み合せることによってプログラムを記述するのが望ましいと考える．
 そこで問題となるのが，証明された型のみで任意のプログラムを記述可能なのか，という点である．
-これは、型がプログラムに加えている制約の強さの問題でもある。
-任意のプログラムに対して形式手法が適用可能な処理系を考えた際に、どの程度の制約が必要なのかも考えなくてはならない。
+これは，型がプログラムに加えている制約の強さの問題でもある．
+任意のプログラムに対して形式手法が適用可能な処理系を考えた際に，どの程度の制約が必要なのかも考えなくてはならない．
 
 \section{まとめ}
-私は形式的手法は実行可能なプログラムに対して処理系と対話的に行なうべきものだと考えている。
-仕様が定まっていなくとも満たすべき条件は存在し、それはどのプログラムにも共通と言って良い。
-さらに、具体的な仕様が決まるのならば拡張として定義していく。
+私は形式手法は実行可能なプログラムに対して処理系と対話的に行なうべきものだと考えている．
+仕様が定まっていなくとも満たすべき条件は存在し，それはどのプログラムにも共通と言って良い．
+さらに，具体的な仕様が決まるのならば拡張として定義していく．
 
-対話的に形式的手法を実行するためには実行可能プログラムの処理系が形式的手法をサポートする必要がある。
-そのためにプログラムに加えるべき情報と制約に興味がある。
-特に、現在は型の情報と制約について調べている。
-私としては情報量は十分だが制約が強すぎるのではないかと考えている。
+対話的に形式手法を実行するためには実行可能プログラムの処理系が形式手法をサポートする必要がある．
+そのためにプログラムに加えるべき情報と制約に興味がある．
+特に，現在は型の情報と制約について調べている．
+私としては情報量は十分だが制約が強すぎるのではないかと考えている．
 
 %}