|
70
|
1 \chapter{まとめ}
|
|
|
2 本論文では Continuation based C のプログラムの CodeSegment と DataSegment が部分型で型付け可能なことを示した。
|
|
|
3 部分型を利用した定義により Agda で CbC のプログラムを記述し、GearsOS のデータ構造 SingleLinkedStack の性質を証明した。
|
|
|
4 よって、 CbC コンパイラやランタイムに依存型を加えることでCbCが自身を証明可能となることが分かった。
|
|
|
5
|
|
|
6 また、部分型の定義により CodeSegment の再利用性が向上する機能を提案した。
|
|
|
7 GearsOS では実行するプログラムごとに Meta DataSegemnt から DataSegment を取り出す CodeSegment \verb/stub/ を記述する必要があったが、部分型を利用することでコンパイル時やランタイムに自動生成できることが分かった。
|
|
|
8 具体的には、プログラムを実行する際の全ての DataSegment の部分型となるような Meta DataSegment を処理系が用意することで実現できる。
|
|
|
9
|
|
|
10 さらに、証明とは別のアプローチとしてモデル検査的な検証が可能であることを示した。
|
|
|
11 メタ計算ライブラリ akasha を用いて赤黒木のプログラムを変更することなく仕様を保証した。
|
|
|
12 その際、全ての状態を総当たりで列挙することは非効率であり、状態を縮小させる手法を適用すべきことが分かった。
|
|
|
13 この状態の縮小にも、依存型が利用できると考えている。
|
|
|
14 証明された性質を利用して、検査の必要が無い状態を排除するのである。
|
|
|
15
|
|
|
16 CbC の型システムを定義することで、証明とモデル検査的なアプローチにおける検証手法と、GearsOS における CodeSegment の再利用性の向上を提案できた。
|
|
|
17
|
|
|
18 \section{今後の課題}
|
|
|
19 今後の課題として、型システムの詳細な性質の解析がある。
|
|
|
20 本論文では部分型の定義を CbC に適用した。
|
|
|
21 CodeSegment は関数呼び出しを末尾でしか許さない制限があるので、関数型の計算規則をより制限できるはずである。
|
|
|
22 その制約の元に生まれた計算体系の持つ性質や表現能力に興味がある。
|
|
|
23
|
|
|
24 また、提案した Agda における CbC 表現をより利用しやすい形でユーザに提供することも必要である。
|
|
|
25 例えば CbC のコードから Agda のコードへの変換系や、Agda の内部表現から直接 CbC を生成することなどが考えられる。
|
|
|
26
|
|
|
27 stub の自動生成に関しては、コンパイル時に DataSegment の部分型を自動で構成するようコンパイラを改良する必要がある。
|
|
|
28 また、ランタイム時に生成された部分型情報を比較することにより、ネットワーク越しに CodeSegment を接続した際に互換性の確認が行なえると考えている。
|
|
|
29
|
|
|
30 モデル検査的アプローチの展望としては、依存型を CbC コンパイラに実装し、型情報を用いた記号実行や状態の列挙を行なうシステムの構築などがある。
|
|
|
31
|
|
|
32 また、型システムの拡張として総称型などを CbC に適用することも挙げられる。
|
|
|
33 総称型は \verb/Java/ における Generics や \verb/C++/ におけるテンプレートに相当し、ユーザが定義できるデータ構造の表現能力が向上する。
|
|
|
34 他にも、CbC における型推論や推論器のコンパイラへの実装などが挙げられる。
|
