Mercurial > hg > Papers > 2018 > parusu-master

annotate paper/summary.tex @ 32:ebcf093795f3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add twice examples
author Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
date Sat, 03 Feb 2018 20:56:35 +0900
parents 106c1d35afd2
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
6
106c1d35afd2 Add tex files
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 \chapter{まとめ}
106c1d35afd2 Add tex files
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 本論文ではメタ計算を用いた Continuation based C プログラムの検証手法を二つ提案した。
106c1d35afd2 Add tex files
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
3
106c1d35afd2 Add tex files
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 一つはモデル検査的なアプローチであり、メタ計算ライブラリ akasha を用いて GearsOS の非破壊赤黒木の仕様を保証した。
106c1d35afd2 Add tex files
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 CbC における仕様の定義は assert に渡す論理式として定義され、状態の数え上げは軽量継続 \verb/meta/ を切り替えることで実現できた。
106c1d35afd2 Add tex files
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 CbC で記述された非破壊赤黒木のプログラムを検証用に変更することなく、CbC 自身で検証した。
106c1d35afd2 Add tex files
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 検証できた範囲は有限の要素数のみであるが、有限モデルチェッカ CBMC よりも大きな範囲を検証した。
106c1d35afd2 Add tex files
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
8
106c1d35afd2 Add tex files
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 二つめは定理証明的なアプローチである。
106c1d35afd2 Add tex files
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 akasha を用いた検証では挿入回数は有限の数に限定されていた。
106c1d35afd2 Add tex files
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 プログラムを直接証明することにより、任意の回数の操作においても性質を保証する。
106c1d35afd2 Add tex files
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 部分型を利用して CbC の型システムの定義を行ない、依存型を持つ言語 Agda 上で記述することで CbC の形式的な定義とした。
106c1d35afd2 Add tex files
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 Agda 上で記述された CbC プログラムの性質を証明することで、 CbC が部分型できちんと型付けできること、依存型をCbCコンパイラに組み込むことでCbC 自身を証明できることが分かった。
106c1d35afd2 Add tex files
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
14
106c1d35afd2 Add tex files
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 また、型システムは証明以外にも実用的に利用できることが分かった。
106c1d35afd2 Add tex files
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 akasha を用いて検証を行なう際、全ての CodeSegment に対して stub をユーザが定義する必要があった。
106c1d35afd2 Add tex files
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 CbC の型を定義することにより、stub の自動生成と型チェックが行なえることが分かった。
106c1d35afd2 Add tex files
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
18
106c1d35afd2 Add tex files
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 \section{今後の課題}
106c1d35afd2 Add tex files
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 今後の課題として、型システムの詳細な性質の解析がある。
106c1d35afd2 Add tex files
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 本論文では部分型の定義を CbC に適用した。
106c1d35afd2 Add tex files
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 CodeSegment は関数呼び出しを末尾でしか許さない制限があるので、関数型の計算規則をより制限できるはずである。
106c1d35afd2 Add tex files
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 その制約の元に生まれた計算体系の持つ性質や表現能力に興味がある。
106c1d35afd2 Add tex files
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
24
106c1d35afd2 Add tex files
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 また、提案した型システムを CbC コンパイラの内部に組み込み、CodeSegment と DataSegment の型チェックを行なえるようにしたい。
106c1d35afd2 Add tex files
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 加えて部分型を組み込むことにより、stub の自動生成ができる。
106c1d35afd2 Add tex files
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 さらに依存型を加えれば CbC で CbC 自身を証明できるようになる。
106c1d35afd2 Add tex files
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 他にも SingleLinkedStack の証明を元にした赤黒木の証明などが考えられる。
106c1d35afd2 Add tex files
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
29
106c1d35afd2 Add tex files
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 モデル検査的アプローチの展望としては、依存型を CbC コンパイラに実装し、型情報を用いた記号実行や状態の列挙を行なうシステムの構築などがある。
106c1d35afd2 Add tex files
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
31
106c1d35afd2 Add tex files
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 また、型システムの拡張としては総称型などを CbC に適用することも挙げられる。
106c1d35afd2 Add tex files
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 多相型は \verb/Java/ におけるジェネリクスや \verb/C++/ におけるテンプレートに相当し、ユーザが定義できるデータ構造の表現能力が向上する。
106c1d35afd2 Add tex files
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 他にも、CbC の型推論や推論器の実装などが挙げられる。