Mercurial > hg > Papers > 2018 > nozomi-master

comparison paper/summary.tex @ 80:73da47f32888

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Update summary
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Wed, 08 Feb 2017 17:25:27 +0900
parents 4b8a75618f36
children 3f63f697ed3a
comparison
equal deleted inserted replaced
79:4985359bd08b 80:73da47f32888
1 \chapter{まとめ} 1 \chapter{まとめ}
2 本論文では Continuation based C のプログラムの CodeSegment と DataSegment が部分型で型付け可能なことを示した。 2 本論文ではメタ計算を用いた Continuation based C プログラムの検証手法を二つ提案した。
3 部分型を利用した定義により Agda で CbC のプログラムを記述し、GearsOS のデータ構造 SingleLinkedStack の性質を証明した。
4 よって、 CbC コンパイラやランタイムに依存型を加えることでCbCが自身を証明可能となることが分かった。
5 3
6 また、部分型の定義により CodeSegment の再利用性が向上する機能を提案した。 4 一つはモデル検査的なアプローチであり、メタ計算ライブラリ akasha を用いて GearsOS の非破壊赤黒木の仕様を保証した。
7 GearsOS では実行するプログラムごとに Meta DataSegemnt から DataSegment を取り出す CodeSegment \verb/stub/ を記述する必要があったが、部分型を利用することでコンパイル時やランタイムに自動生成できることが分かった。 5 CbC における仕様の定義は assert に渡す論理式として定義され、状態の数え上げは軽量継続 \verb/meta/ を切り替えることで実現できた。
8 具体的には、プログラムを実行する際の全ての DataSegment の部分型となるような Meta DataSegment を処理系が用意することで実現できる。 6 CbC で記述された非破壊赤黒木のプログラムを検証用に変更することなく、CbC 自身で検証した。
7 検証できた範囲は有限の要素数のみであるが、有限モデルチェッカ CBMC よりも大きな範囲を検証した。
9 8
10 さらに、証明とは別のアプローチとしてモデル検査的な検証が可能であることを示した。 9 二つめは定理証明的なアプローチである。
11 メタ計算ライブラリ akasha を用いて赤黒木のプログラムを変更することなく仕様を保証した。 10 akasha を用いた検証では挿入回数は有限の数に限定されていた。
12 その際、全ての状態を総当たりで列挙することは非効率であり、状態を縮小させる手法を適用すべきことが分かった。 11 データ構造とそれにまつわる処理を直接証明することにより、任意の回数操作を行なっても性質を保証する。
13 この状態の縮小にも、依存型が利用できると考えている。 12 部分型を利用して CbC の型システムの定義を行ない、依存型を持つ言語 Agda 上で記述することで CbC の形式的な定義とした。
14 証明された性質を利用して、検査の必要が無い状態を排除するのである。 13 Agda 上で記述された CbC プログラムの性質を証明することで、 CbC が部分型できちんと型付けできること、依存型をCbCコンパイラに組み込むことでCbC 自身を証明できることが分かった。
15 14
16 CbC の型システムを定義することで、証明とモデル検査的なアプローチにおける検証手法と、GearsOS における CodeSegment の再利用性の向上を提案できた。 15 また、型システムは証明以外にも実用的に利用できることが分かった。
16 akasha を用いて検証を行なう際、全ての CodeSegment に対して stub をユーザが定義する必要があった。
17 CbC の型を定義することにより、stub の自動生成と型チェックが行なえることが分かった。
17 18
18 \section{今後の課題} 19 \section{今後の課題}
19 今後の課題として、型システムの詳細な性質の解析がある。 20 今後の課題として、型システムの詳細な性質の解析がある。
20 本論文では部分型の定義を CbC に適用した。 21 本論文では部分型の定義を CbC に適用した。
21 CodeSegment は関数呼び出しを末尾でしか許さない制限があるので、関数型の計算規則をより制限できるはずである。 22 CodeSegment は関数呼び出しを末尾でしか許さない制限があるので、関数型の計算規則をより制限できるはずである。
22 その制約の元に生まれた計算体系の持つ性質や表現能力に興味がある。 23 その制約の元に生まれた計算体系の持つ性質や表現能力に興味がある。
23 24
24 また、提案した Agda における CbC 表現をより利用しやすい形でユーザに提供することも必要である。 25 また、提案した型システムを CbC コンパイラの内部に組み込み、CodeSegment と DataSegment の型チェックを行なえるようにしたい。
25 例えば CbC のコードから Agda のコードへの変換系や、Agda の内部表現から直接 CbC を生成することなどが考えられる。 26 加えて部分型を組み込むことにより、stub の自動生成をする。
26 27 さらに依存型を加えれば CbC で CbC 自身を証明できるようになる。
27 stub の自動生成に関しては、コンパイル時に DataSegment の部分型を自動で構成するようコンパイラを改良する必要がある。
28 また、ランタイム時に生成された部分型情報を比較することにより、ネットワーク越しに CodeSegment を接続した際に互換性の確認が行なえると考えている。
29 28
30 モデル検査的アプローチの展望としては、依存型を CbC コンパイラに実装し、型情報を用いた記号実行や状態の列挙を行なうシステムの構築などがある。 29 モデル検査的アプローチの展望としては、依存型を CbC コンパイラに実装し、型情報を用いた記号実行や状態の列挙を行なうシステムの構築などがある。
31 30
32 また、型システムの拡張として総称型などを CbC に適用することも挙げられる。 31 また、型システムの拡張としては総称型などを CbC に適用することも挙げられる。
33 総称型は \verb/Java/ における Generics や \verb/C++/ におけるテンプレートに相当し、ユーザが定義できるデータ構造の表現能力が向上する。 32 総称型は \verb/Java/ におけるジェネリクスや \verb/C++/ におけるテンプレートに相当し、ユーザが定義できるデータ構造の表現能力が向上する。
34 他にも、CbC における型推論や推論器のコンパイラへの実装などが挙げられる。 33 他にも、CbC における型推論や推論器のコンパイラへの実装などが挙げられる。