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