Mercurial > hg > Papers > 2015 > atton-sigse
annotate sigse.tex @ 23:973fadbd6687
Mini fixes
| author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 10 Dec 2014 16:28:34 +0900 |
| parents | 3ce3612218a0 |
| children | 158ee14c3615 |
| rev | line source |
|---|---|
| 2 | 1 \documentclass{ipsjpapers} |
|
11
0863e8f0a3d6
Add figure for version combination
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
10
diff
changeset
|
2 \usepackage{url} |
|
0863e8f0a3d6
Add figure for version combination
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
10
diff
changeset
|
3 \usepackage[dvipdfmx]{graphicx} |
|
0863e8f0a3d6
Add figure for version combination
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
10
diff
changeset
|
4 |
| 2 | 5 |
| 6 % ユーザが定義したマクロなど． | |
| 7 \makeatletter | |
| 8 \let\@ARRAY\@array \def\@array{\def\<{\inhibitglue}\@ARRAY} | |
| 9 \def\<{\(\langle\)\nobreak} | |
| 10 \def\>{\nobreak\(\rangle\)} | |
| 11 \def\|{\verb|} | |
| 12 \def\Underline{\setbox0\hbox\bgroup\let\\\endUnderline} | |
| 13 \def\endUnderline{\vphantom{y}\egroup\smash{\underline{\box0}}\\} | |
| 14 \def\LATEX{\iLATEX\Large} | |
| 15 \def\LATEx{\iLATEX\normalsize} | |
| 16 \def\LATex{\iLATEX\small} | |
| 17 \def\iLATEX#1{L\kern-.36em\raise.3ex\hbox{#1\bf A}\kern-.15em | |
| 18 T\kern-.1667em\lower.7ex\hbox{E}\kern-.125emX} | |
| 19 \def\LATEXe{\ifx\LaTeXe\undefined \LaTeX 2e\else\LaTeXe\fi} | |
| 20 \def\LATExe{\ifx\LaTeXe\undefined \iLATEX\scriptsize 2e\else\LaTeXe\fi} | |
| 21 \def\Quote{\list{}{}\item[]} | |
| 22 \let\endQuote\endlist | |
| 23 \def\TT{\if@LaTeX@e\tt\fi} | |
| 24 \def\CS#1{\if@LaTeX@e\tt\expandafter\string\csname#1\endcsname\else | |
|
3
056c4b8a1f57
Wrote author, title
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
2
diff
changeset
|
25 $\backslash$#1\fi} |
| 2 | 26 |
|
3
056c4b8a1f57
Wrote author, title
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
2
diff
changeset
|
27 %\checklines % 行送りを確認する時に使用 |
| 2 | 28 \begin{document}%{ |
| 29 % 和文表題 | |
|
20
afdab6523b42
Wrote position paper
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
19
diff
changeset
|
30 \title{形式手法とプログラミング言語の型} |
| 2 | 31 % 英文表題 |
|
17
7ec73a287b63
Writing position paper ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
13
diff
changeset
|
32 \etitle{Formal Methods and Types of Programming Languages} |
| 2 | 33 % 所属ラベルの定義 |
|
3
056c4b8a1f57
Wrote author, title
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
2
diff
changeset
|
34 \affilabel{ie-ryukyu}{琉球大学工学部情報工学科 \\ Department of Information Engineering, University of the Ryukyus.} |
| 2 | 35 % 和文著者名 |
|
17
7ec73a287b63
Writing position paper ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
13
diff
changeset
|
36 \author{比嘉 健太\affiref{ie-ryukyu} \and |
|
3
056c4b8a1f57
Wrote author, title
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
2
diff
changeset
|
37 河野 真治\affiref{ie-ryukyu}} |
| 2 | 38 % 英文著者名 |
| 6 | 39 \eauthor{Yasutaka Higa\affiref{ie-ryukyu}\and |
| 40 Shinji Kono\affiref{ie-ryukyu}} | |
| 2 | 41 |
| 42 % 和文概要 | |
| 43 \begin{abstract} | |
|
20
afdab6523b42
Wrote position paper
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
19
diff
changeset
|
44 任意のプログラムに対して形式手法が適用可能であるべきであると考える． |
| 21 | 45 そのために，全てのプログラムへ形式手法が対話的に実行できる処理系を考えたい． |
|
20
afdab6523b42
Wrote position paper
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
19
diff
changeset
|
46 その処理系が実行するプログラムに記述するべき情報量とプログラムに対する制約の強度について興味がある． |
| 2 | 47 \end{abstract} |
| 48 % 英文概要 | |
| 49 \begin{eabstract} | |
|
20
afdab6523b42
Wrote position paper
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
19
diff
changeset
|
50 I think any program must be check by formal methods. |
|
afdab6523b42
Wrote position paper
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
19
diff
changeset
|
51 I want to programming language executer that applicative formal methods to any program interactively. |
|
afdab6523b42
Wrote position paper
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
19
diff
changeset
|
52 I interest constraints of program and amounts of information that enough for formal methods. |
| 2 | 53 \end{eabstract} |
| 54 | |
| 55 % 表題などの出力 | |
| 56 \maketitle | |
| 57 | |
|
4
3c333203c8c5
Delete unknown charcode
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
3
diff
changeset
|
58 %}{ |
| 2 | 59 |
| 60 % 本文はここから始まる | |
| 61 \section{はじめに} | |
|
17
7ec73a287b63
Writing position paper ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
13
diff
changeset
|
62 形式手法によるチェックはプログラム実装言語の処理系とユーザ間で対話的に行なわれるべきだと考える． |
|
20
afdab6523b42
Wrote position paper
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
19
diff
changeset
|
63 任意のプログラムに対して形式手法が適用可能であり，必要ならばユーザが制約をさらに厳しくする． |
|
18
2ab39686323a
Writing position paper ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
64 制約の追加が対話的入力であり，反例の指摘などが対話的出力に相当する． |
|
20
afdab6523b42
Wrote position paper
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
19
diff
changeset
|
65 対話的チェックを実現するには，実装言語が通常の処理系に加えて形式手法をサポートする必要があると考える． |
|
18
2ab39686323a
Writing position paper ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
66 |
|
20
afdab6523b42
Wrote position paper
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
19
diff
changeset
|
67 \section{形式手法をサポートした言語} |
|
afdab6523b42
Wrote position paper
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
19
diff
changeset
|
68 任意のプログラムに対して形式手法を適用可能な処理系は作成できると考える． |
|
18
2ab39686323a
Writing position paper ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
69 なぜなら，アプリケーションの仕様に関わらず実行してはいけない処理などが存在するからである． |
| 6 | 70 |
|
17
7ec73a287b63
Writing position paper ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
13
diff
changeset
|
71 例えば，0による除算や配列外へのアクセスはどのようなプログラムにおいても実行してはいけない． |
|
18
2ab39686323a
Writing position paper ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
72 よって，全てのプログラムが共通に持つべき仕様として定義可能である． |
|
20
afdab6523b42
Wrote position paper
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
19
diff
changeset
|
73 処理系が仕様のチェック機構を持つことにより，全てのプログラムに対して形式手法が導入可能となる． |
|
18
2ab39686323a
Writing position paper ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
74 仕様はユーザ定義の満たすべき条件として定義する． |
|
17
7ec73a287b63
Writing position paper ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
13
diff
changeset
|
75 基本的な満たすべき条件の拡張として記述することにより，仕様が存在するプログラムにも対応することができる． |
|
11
0863e8f0a3d6
Add figure for version combination
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
10
diff
changeset
|
76 |
|
17
7ec73a287b63
Writing position paper ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
13
diff
changeset
|
77 ここで，プログラム実装言語が自動で仕様をチェックするために必要な情報を考えたい． |
|
7ec73a287b63
Writing position paper ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
13
diff
changeset
|
78 どれだけの情報をプログラムに記述すれば自動でチェックできるかは私の中ではまだはっきりしていない． |
|
7ec73a287b63
Writing position paper ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
13
diff
changeset
|
79 仕様をチェックするに足る情報の量と，その情報から仕様をチェックする手法に興味がある． |
| 6 | 80 |
| 81 | |
|
17
7ec73a287b63
Writing position paper ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
13
diff
changeset
|
82 \section{型と証明支援系言語} |
|
7ec73a287b63
Writing position paper ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
13
diff
changeset
|
83 現在，私がプログラムに追加する情報として注目しているのが型である． |
|
7ec73a287b63
Writing position paper ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
13
diff
changeset
|
84 型と論理は対応しており，証明が存在する定理は型によって表現できる． |
|
7ec73a287b63
Writing position paper ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
13
diff
changeset
|
85 満たすべき性質を証明として型が記述できれば，その型は性質を満たすと言える． |
|
7ec73a287b63
Writing position paper ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
13
diff
changeset
|
86 仕様を全て論理で記述し，対応する型を記述すると仕様を満たすプログラムが記述できると思われる． |
|
7ec73a287b63
Writing position paper ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
13
diff
changeset
|
87 しかし，論理を満たす型の記述には非常に大きなコストがかかる． |
| 6 | 88 |
|
17
7ec73a287b63
Writing position paper ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
13
diff
changeset
|
89 私は研究において関数型プログラミング言語Haskellと証明支援系プログラミング言語Agdaを利用している． |
|
7ec73a287b63
Writing position paper ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
13
diff
changeset
|
90 プログラムの変更を表すことのできるデータ型を用意し，異なるバージョンのプログラム間の関係を形式化する試みである． |
| 23 | 91 この研究において，Haskell でデータ型とそのデータ型への処理を50行ほど記述した． |
|
17
7ec73a287b63
Writing position paper ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
13
diff
changeset
|
92 そのデータ型と処理が満たすべき条件をAgdaで記述すると500行ほどとなった． |
|
7ec73a287b63
Writing position paper ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
13
diff
changeset
|
93 行換算すると実装に対して仕様には10倍のコストがかかっている． |
|
20
afdab6523b42
Wrote position paper
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
19
diff
changeset
|
94 Agda では非常に単純な性質は自動で導くが，ほとんどの性質は自ら記述する． |
|
afdab6523b42
Wrote position paper
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
19
diff
changeset
|
95 Agda が行なうのは，性質を満たしているかのチェックと満たすべき性質が必要とする性質の指摘である． |
|
afdab6523b42
Wrote position paper
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
19
diff
changeset
|
96 Agda によって性質を記述すると，性質の詳細や依存関係は明確になるが，性質を直接解くコストは必須である． |
| 6 | 97 |
|
17
7ec73a287b63
Writing position paper ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
13
diff
changeset
|
98 個別のプロジェクトにおいて個別のデータ型を定義し，満たすべき性質を記述するのでは非常に大きなコストがかかってしまう． |
|
7ec73a287b63
Writing position paper ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
13
diff
changeset
|
99 よって，既に証明された型どうしを組み合せることによってプログラムを記述するのが望ましいと考える． |
|
7ec73a287b63
Writing position paper ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
13
diff
changeset
|
100 そこで問題となるのが，証明された型のみで任意のプログラムを記述可能なのか，という点である． |
|
20
afdab6523b42
Wrote position paper
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
19
diff
changeset
|
101 これは，型がプログラムに加えている制約の強さの問題でもある． |
|
afdab6523b42
Wrote position paper
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
19
diff
changeset
|
102 任意のプログラムに対して形式手法が適用可能な処理系を考えた際に，どの程度の制約が必要なのかも考えなくてはならない． |
| 6 | 103 |
|
17
7ec73a287b63
Writing position paper ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
13
diff
changeset
|
104 \section{まとめ} |
|
20
afdab6523b42
Wrote position paper
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
19
diff
changeset
|
105 私は形式手法は実行可能なプログラムに対して処理系と対話的に行なうべきものだと考えている． |
|
afdab6523b42
Wrote position paper
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
19
diff
changeset
|
106 仕様が定まっていなくとも満たすべき条件は存在し，それはどのプログラムにも共通と言って良い． |
|
afdab6523b42
Wrote position paper
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
19
diff
changeset
|
107 さらに，具体的な仕様が決まるのならば拡張として定義していく． |
|
19
33ab1d8af5dc
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
18
diff
changeset
|
108 |
|
20
afdab6523b42
Wrote position paper
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
19
diff
changeset
|
109 対話的に形式手法を実行するためには実行可能プログラムの処理系が形式手法をサポートする必要がある． |
|
afdab6523b42
Wrote position paper
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
19
diff
changeset
|
110 そのためにプログラムに加えるべき情報と制約に興味がある． |
|
afdab6523b42
Wrote position paper
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
19
diff
changeset
|
111 特に，現在は型の情報と制約について調べている． |
| 23 | 112 私としては依存型は情報量は十分だが制約が強すぎ，線形型では情報量が不十分なのでは無いかと考えている． |
| 2 | 113 |
|
13
b34ce7d49a0c
Mini fixes from OC-san
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
11
diff
changeset
|
114 %} |
| 2 | 115 |
| 116 \end{document} |