--- a/presentation/slide.md	Tue Feb 14 11:31:08 2017 +0900
+++ b/presentation/slide.md	Tue Feb 14 15:03:04 2017 +0900
@@ -28,18 +28,44 @@
     *  なのでそちらをメインで発表します
 
 # モデル検査的アプローチについての流れ
+* 既存のモデル検査器について
 * Continuation based C (CbC) 言語について
 * CbC における CodeSegment と DataSegment を用いたプログラミングスタイル
 * CbC とメタ計算について
 * CbC で記述された GearsOS とそのデータ構造である赤黒木
 * 赤黒木の仕様の定義とその検証手法
 
+# 既存のモデル検査器 spin
+* spin
+    * promela と呼ばれる言語でプログラムを記述
+    * 並列に動作するプログラムの仕様を検証可能
+    * 検証した promela から実行可能な C ソースを生成可能
+    * 仕様は bool になる式を用いた assert
+    * デメリット: promela は C とは記述が異なる
+
+```
+assert(x < 10);
+```
+
+# 既存のモデル検査器 CBMC
+* CBMC
+    * 検証対象のCソースを変更しないでも良い
+    * C/C++ 言語の記号実行が可能
+        * 条件分岐を網羅的に実行
+    * 仕様は bool になる式を用いた assert
+    * 有限ステップだけ検証する有界モデル検査器
+
+```
+assert(x < 10);
+```
+
 # Continuation based C
 * 当研究室で開発しているプログラミング言語
 * アセンブラとC言語の中間のような言語であり、構文はほとんど C 言語
 * OS や組み込みソフトウェアなどを対象にしている
 * CodeSegment と DataSegment という単位を用いてプログラミングする
-* 両検証手法をメタ計算として利用可能
+* モデル検査と証明の両検証手法をメタ計算として利用可能
+    * CbC で CbC 自身を検証可能
 
 # CodeSegment
 * CodeSegment とは
@@ -84,13 +110,13 @@
 * メタ計算を行なう CodeSegment
 * 通常の CodeSegment どうしの接続の間に入る
 
-![mcs](./images/mcs.svg){:width="50%"}
+![mcs](./images/mcs.svg){:width="75%"}
 
 # Meta DataSegment
 * メタ計算用の DataSegment
 * 通常の DataSegment を含むような DataSegment
 
-![mds](./images/mds.svg){:width="50%"}
+![mds](./images/mds.svg){:width="75%"}
 
 # 並列に信頼性高く動作する GearsOS
 * CbC を用いたメタ計算の例として本研究室で開発している GearsOS がある
@@ -110,7 +136,6 @@
 # GearsOS における赤黒木の利用例(ノードの挿入)
 * 挿入したい要素を DataSegment に格納して次の CodeSegment へ goto
 * goto する前に Meta CodeSegment が実行されて木に挿入する
-* GearsOS では木の実装のためにスタックを用いて経路情報を保持している
 
 
 ![put](./images/put.svg){:width="50%"}
@@ -121,34 +146,10 @@
 
 # 仕様の記述とその確認
 * 「バランスが取れている」とは何かを表現できる必要がある
-    * 実行可能な CbC の式を使った assert になる
+    * 実行可能な CbC の条件式を使った assert になる
 * そしてそれを保証したい
     * プログラムの全ての状態においてこれは常に成り立つのか?
 
-# 既存のモデル検査器 spin
-* spin
-    * promela と呼ばれる言語でプログラムを記述
-    * 並列に動作するプログラムの仕様を検証可能
-    * 検証した promela から実行可能な C ソースを生成可能
-    * 仕様は bool になる式を用いた assert
-    * デメリット: promela は C とは記述が異なる
-
-```
-assert(x < 10);
-```
-
-# 既存のモデル検査器 CBMC
-* CBMC
-    * 検証対象のCソースを変更しないでも良い
-    * C/C++ 言語の記号実行が可能
-        * 条件分岐を網羅的に実行
-    * 仕様は bool になる式を用いた assert
-    * 有限ステップ検証する有界モデル検査器
-
-```
-assert(x < 10);
-```
-
 # チェックする仕様
 * 赤黒木の高さに関する仕様に以下のものがある
     * 木をルートから辿った際に最も長い経路は最も短い経路の高々2倍に収まる
@@ -173,7 +174,7 @@
     * その度に仕様の式は成り立つかをチェックする
 * ノーマルレベルのコードを検証用に変更せず検証可能
 
-![akashaPut](./images/akashaPut.svg){:width="51%"}
+![akashaPut](./images/akashaPut.svg){:width="50%"}
 
 # akasha と CBMC の比較
 * akasha は有限の要素数の組み合わせをチェックする
@@ -187,7 +188,7 @@
 
 # 定理証明を Continuation based C へ適用するには
 * 任意の回数だけ木の操作を行なっても大丈夫なことを保証したい
-* そのままプログラムの性質を保証してやる
+* 直接プログラムの性質を証明
 * Coq, Agda, ATS2 などのプログラミング言語で証明が可能
     * 本当は CbC で CbC 自身を証明したい
     * しかし CbC の形式的な定義が無いために今はできない
@@ -195,6 +196,7 @@
 
 # Agda と DataSegment
 * CbC の DataSegment は Agda のレコード型
+    * 名前付きの値が複数ある(C の構造体)
 
 ```
 __code cs0(int a, int b){
@@ -209,7 +211,8 @@
 ```
 
 # Agda と CodeSegment
-* CbC の CodeSegment は、Agda の関数型(Input を取って Output を返す)
+* CbC の CodeSegment は、Agda の関数型
+    * Input を取って Output を返す
 
 ```
 __code cs0(int a, int b){
@@ -270,10 +273,11 @@
     * データ構造 SingleLinkedStack の証明ができた
 
 # 今後の課題
+* より大きなサイズの赤黒木の検証
+* 赤黒木の挿入に関する性質を証明する
 * 部分型を利用してCbCを型付け
 * 依存型をCbC に導入して自身を証明可能にする
 * 型情報から stub を自動生成すkる
-* 赤黒木の挿入に関する性質を証明する
 
 # 発表履歴
 * Agda 入門.