Mercurial > hg > Papers > 2015 > atton-sigse

comparison sigse.tex @ 27:ce6ce56bd414

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Writing position paper ...
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Thu, 11 Dec 2014 12:59:57 +0900
parents 158ee14c3615
children c73b1c3d88ad
comparison
equal deleted inserted replaced
26:fa9bde939db6 27:ce6ce56bd414
25 $\backslash$#1\fi} 25 $\backslash$#1\fi}
26 26
27 %\checklines % 行送りを確認する時に使用 27 %\checklines % 行送りを確認する時に使用
28 \begin{document}%{ 28 \begin{document}%{
29 % 和文表題 29 % 和文表題
30 \title{形式手法とプログラミング言語の型} 30 \title{hoge}
31 % 英文表題 31 % 英文表題
32 \etitle{Formal Methods and Types of Programming Languages} 32 \etitle{hoge}
33 % 所属ラベルの定義 33 % 所属ラベルの定義
34 \affilabel{ie-ryukyu}{琉球大学工学部情報工学科 \\ Department of Information Engineering, University of the Ryukyus.} 34 \affilabel{ie-ryukyu}{琉球大学工学部情報工学科 \\ Department of Information Engineering, University of the Ryukyus.}
35 % 和文著者名 35 % 和文著者名
36 \author{比嘉 健太\affiref{ie-ryukyu} \and 36 \author{比嘉 健太\affiref{ie-ryukyu} \and
37 河野 真治\affiref{ie-ryukyu}} 37 河野 真治\affiref{ie-ryukyu}}
39 \eauthor{Yasutaka Higa\affiref{ie-ryukyu}\and 39 \eauthor{Yasutaka Higa\affiref{ie-ryukyu}\and
40 Shinji Kono\affiref{ie-ryukyu}} 40 Shinji Kono\affiref{ie-ryukyu}}
41 41
42 % 和文概要 42 % 和文概要
43 \begin{abstract} 43 \begin{abstract}
44 任意のプログラムに対して形式手法が適用可能であるべきであると考える． 44 卒業研究までの一年間で得た形式手法への感想と理想を語ろうかと．
45 そのために，全てのプログラムへ形式手法が対話的に実行できる処理系を考えたい． 45
46 その処理系が実行するプログラムに記述するべき情報量とプログラムに対する制約の強度について興味がある．
47 \end{abstract} 46 \end{abstract}
48 % 英文概要 47 % 英文概要
49 \begin{eabstract} 48 \begin{eabstract}
50 I think any program must be check by formal methods. 49
51 I want to programming language executer that applicative formal methods to any program interactively.
52 I interest constraints of program and amounts of information that enough for formal methods.
53 \end{eabstract} 50 \end{eabstract}
54 51
55 % 表題などの出力 52 % 表題などの出力
56 \maketitle 53 \maketitle
57 54
58 %}{ 55 %}{
59 56
60 % 本文はここから始まる 57 % 本文はここから始まる
61 \section{はじめに} 58 \section{自己紹介}
62 形式手法によるチェックはプログラム実装言語の処理系とユーザ間で対話的に行なわれるべきだと考える． 59 私は琉球大学工学部情報工学科に所属する四年次の学生である．
63 任意のプログラムに対して形式手法が適用可能であり，必要ならばユーザが制約をさらに厳しくする． 60 自動でプログラムのバグを見付ける機構が欲しいと思い，卒業研究はそのようなテーマで取り組んでいる．
64 制約の追加が対話的入力であり，反例の指摘などが対話的出力に相当する．
65 61
66 対話的に実行する理由は，必要とされる仕様の厳密さに柔軟に対応するためである． 62 研究を進めるにつれ，プログラムのバグを見付けるには仕様やテストを記述する必要があることを知った．
67 例えば，使い捨てのプログラムなどに厳密な仕様を策定するのはコストが高すぎる． 63 テストを記述するコストはおそらくプログラムを書くコストと同じかそれ以上かかる．
68 しかし非常に単純なバグを自動で見つけるために形式手法を利用したい． 64 あくまで私はプログラムのみでバグを見付けたかった．
69 そのバグのみを見つけるための条件を対話的な出力とし，ユーザが入力をする． 65 そのために，プログラムの変更に着目することによりバグを見付ける手法を提案することにした．
70 他にも，徐々に仕様が複雑になり整理したい，といった場合なども対話的に必要な分だけ対応したい．
71 そのためにも仕様が存在しないような任意のプログラムに対しても形式手法を実行したい．
72 66
73 そのような対話的チェックを実現するには，実装言語が通常の処理系に加えて形式手法をサポートする必要があると考える． 67 \section{卒業研究 と Category と Agda}
68 私の研究においてまず問題となったのがプログラムの変更の表現だった．
74 69
75 \section{形式手法をサポートした言語} 70 そこで指導教員からプログラムに対する変更を Monad によって表現するアイデアを頂いた．
76 任意のプログラムに対して形式手法を適用可能な処理系は作成できると考える． 71 アイデアを実現するために取った過程を示したい．
77 なぜなら，アプリケーションの仕様に関わらず実行してはいけない処理などが存在するからである．
78 72
79 例えば，0による除算や配列外へのアクセスはどのようなプログラムにおいても実行してはいけない． 73 まず， Monad とは何かを知る必要があった．
80 よって，全てのプログラムが共通に持つべき仕様として定義可能である． 74 Monad はプログラミング言語 Haskell では型クラスとして用意されており，まず型とは何かを知る必要があった．
81 処理系が仕様のチェック機構を持つことにより，全てのプログラムに対して形式手法が導入可能となる． 75 そこで，Proofs and Types を指導教員と読むこととなった．
82 仕様はユーザ定義の満たすべき条件として定義する． 76 Proofs and Types では型と論理の対応について知ることができた．
83 基本的な満たすべき条件の拡張として記述することにより，仕様が存在するプログラムにも対応することができる． 77 例題は証明支援系言語 Agda によって記述した．
78 Agda では項とその書き換えによる等式変形を意識することとなった．
84 79
85 ここで，プログラム実装言語が自動で仕様をチェックするために必要な情報を考えたい． 80 型の整合性で記述する % TODO: もうちょい書けるがまとまらない
86 どれだけの情報をプログラムに記述すれば自動でチェックできるかは私の中ではまだはっきりしていない． 81
87 仕様をチェックするに足る情報の量と，その情報から仕様をチェックする手法に興味がある． 82 型の理論背景を知った後，次に Monad とは一体何か知る必要があった．
83 Monad は Category Theory から computer science に持ち込まれたものであった．
84 そのために Category theory を知る必要があった．
85 Monad には満たすべき Monad則が存在し、Monad 則の証明も型によって Agda で記述できた。
88 86
89 87
90 \section{型と証明支援系言語} 88 \section{産業界に形式手法を普及するには}
91 現在，私がプログラムに追加する情報として注目しているのが型である． 89 \section{わたしのりそう}
92 型と論理は対応しており，証明が存在する定理は型によって表現できる． 90 \section{まとめ?}
93 満たすべき性質を証明として型が記述できれば，その型は性質を満たすと言える．
94 仕様を全て論理で記述し，対応する型を記述すると仕様を満たすプログラムが記述できると思われる．
95 しかし，論理を満たす型の記述には非常に大きなコストがかかる．
96
97 私は研究において関数型プログラミング言語Haskellと証明支援系プログラミング言語Agdaを利用している．
98 プログラムの変更を表すことのできるデータ型を用意し，異なるバージョンのプログラム間の関係を形式化する試みである．
99 この研究において，Haskell でデータ型とそのデータ型への処理を50行ほど記述した．
100 そのデータ型と処理が満たすべき条件をAgdaで記述すると500行ほどとなった．
101 行換算すると実装に対して仕様には10倍のコストがかかっている．
102 Agda では非常に単純な性質は自動で導くが，ほとんどの性質は自ら記述する．
103 Agda が行なうのは，性質を満たしているかのチェックと満たすべき性質が必要とする性質の指摘である．
104 Agda によって性質を記述すると，性質の詳細や依存関係は明確になるが，性質を直接解くコストは必須である．
105
106 個別のプロジェクトにおいて個別のデータ型を定義し，満たすべき性質を記述するのでは非常に大きなコストがかかってしまう．
107 よって，既に証明された型どうしを組み合せることによってプログラムを記述するのが望ましいと考える．
108 そこで問題となるのが，証明された型のみで任意のプログラムを記述可能なのか，という点である．
109 これは，型がプログラムに加えている制約の強さの問題でもある．
110 任意のプログラムに対して形式手法が適用可能な処理系を考えた際に，どの程度の制約が必要なのかも考えなくてはならない．
111
112 \section{まとめ}
113 私は形式手法は実行可能なプログラムに対して処理系と対話的に行なうべきものだと考えている．
114 仕様が定まっていなくとも満たすべき条件は存在し，それはどのプログラムにも共通と言って良い．
115 さらに，具体的な仕様が決まるのならば拡張として定義していく．
116
117 対話的に形式手法を実行するためには実行可能プログラムの処理系が形式手法をサポートする必要がある．
118 そのためにプログラムに加えるべき情報と制約に興味がある．
119 特に，現在は型の情報と制約について調べている．
120 私としては依存型は情報量は十分だが制約が強すぎ，線形型では情報量が不十分なのでは無いかと考えている．
121 91
122 %} 92 %}
123 93
124 \end{document} 94 \end{document}