--- a/presentation/slide.md	Tue Jul 26 17:33:52 2016 +0900
+++ b/presentation/slide.md	Tue Aug 02 15:48:45 2016 +0900
@@ -1,70 +1,59 @@
 title: Continuation based C を用いたプログラムの検証手法
 author: 比嘉健太
-profile: 琉球大学 大学院 理工学研究科
+profile: 琉球大学 大学院 理工学研究科 情報工学専攻
 lang: Japanese
 
-# 研究目的
+# ソフトウェアの実装の信頼性の向上
 * ソフトウェアの信頼性を向上させたい
-* ソフトウェアが仕様を常に満たすことを保証することで信頼性を確保する
-* 特に動作するソフトウェアを検証したい
-* 計算を拡張するメタ計算として検証機構を導入し、ソフトウェアの記述を変更せずに検証を行なう
+* 信頼性を向上させる手法には証明、モデル検査、テストなど様々な手法がある
+* ソフトウェアが定められた仕様を常に満たすか確認することで信頼性を保証する
+* 計算を拡張するメタ計算として検証機構を導入し、ソフトウェアの実装コードの検証を行なう
 
-# 研究内容
-* Code Segment と Code Segment を用いるプログラミングスタイルを提案する
-* Code Segment とは処理の単位であり、相互に接続することでプログラムを構成していく
-* メタ計算による処理の拡張は接続部分に Meta Code Segment を挟むことで実現できる
-* Continuation based C 言語で記述された赤黒木を検証していく
+# ソフトウェアの信頼性向上手法
+* アルゴリズムの正しさを証明する
+    * Agda, Coq, Idris といった証明支援系でプログラムを記述する
+    * TeX: アルゴリズムの証明をドキュメントとして記述している
+* ソフトウェアの仕様を記述し、その反例が無いかをチェックする
+    * Spin, NuSMV, CBMC といったモデルチェッカ
+* テストデータを入力して正しい出力を返すか
+    * ユニットテスト
+* assert や型システム、検証用の実行処理系
+    * Java Path Finder, Virtual VM, Valgrind
 
-# Code Segment
-* Code Segment は処理の単位
-* ループを含まないシンプルな処理のみを単一 Code Segment で行なう
-* Code Segment どうしを接続することで複雑な処理も実現できる
-* 依存のない Code Segment どうしは並列に実行することが可能
+# ソフトウェアの実装を検証したい
+* アルゴリズムの正しさが証明できても実装する際にバグが入ることがある
+    * 単語の打ち間違いによるバグ
+    * 同じアルゴリズムを検証と実装で二度記述する
+    * 検証と実装で言語も違うことも
+* 実際に動作するソフトウェアの実装をチェックしたい
+    * 実装コードを変更せずに仕様を保証する
+    * 実装部分と検証部分も同じ言語で記述したい
 
-# Data Segment
-* Data Segment はデータの単位
-* Code Segment は入出力である Input Data Segment と Output Data Segment を持つ
-* Code Segment 内部で扱うデータは Data Segment に格納される
-* Output Data Segment は次の Code Segment の Input Data Segment
+# Continuation based C (CbC)
+* 当研究室で開発している言語
+* 関数呼び出しは末尾のみ、の制約を持ったC言語
+    * Tail Call を言語仕様として持つ
+    * スタックは持たない
+    * goto で飛んで戻ってこない
+    * アーキテクチャに依存しないアセンブラ
+* 組込みシステムやOSの記述を目的としている
+* Code Segment, Data Segment という単位でソフトウェアを記述する
+
+# Code Segment: 処理の単位
+* 単一 Code Segment ではループを含まないシンプルな処理のみを行なう
+* Code Segment どうしを接続してソフトウェア全体を構築していく
+* 依存のない Code Segment どうしは並列に実行することが可能
 * TODO: figure of code segments
 
-# Meta Computations
-* 計算を実現する計算をメタ計算とする
-* メモリ管理や例外処理、並列実行など
-* 一つレベルが上の計算と考える
-* ノーマルレベルとメタレベル
-* ノーマルレベルの計算を保存するメタ計算を定義して、プログラムを変えずに全体の挙動を変える
-* 例:
-    * 直列に実行される想定でプログラムを記述する
-    * 並列に実行するメタ計算で拡張する
-    * ノーマルレベルのプログラムを変更せずに並列で動作するプログラムになる
-
-# Meta Code Segment
-* メタ計算は Code Segment と Code Segment の間に Code Segment を入れることで追加できる
-* Code Segment に対する Meta Code Segment
-* Code Segment に必要な Data Segment を用意したり
-* メモリ管理の例:
-    * Code Segment に必要な変数にメモリを割り当て、 Code Segment に Data Segment として渡す
-    * ノーマルレベルの Code Segment からはポインタが見えないのでポインタに由来するバグを減らせる
-
-# Meta Data Segment
-* Meta Code Segment に必要なデータを格納する
-* Data Segment を内包する Data Segment
-* メモリ管理の例:
-    * Data Segment は Code Segment に必要な変数を持つ
-    * Meta Data Segment は変数の割り当てに使用可能なメモリアドレスを保持
-* メモリのアロケータの変更が容易
-
-# Continuation based C (CbC)
-* Code Segment と Data Segment をサポートした言語
-* 関数呼び出しは末尾のみ、の制約を持ったC言語
-    * goto で飛んで戻ってこない
-    * C とアセンブラの中間のようなもの
-* 組込みシステムの記述やOSの記述を目的としている
+# Data Segment: データの単位
+* Code Segment は入出力である Input Data Segment と Output Data Segment を持つ
+* Output Data Segment は接続先の Code Segment の Input になる
+* Code Segment 内部で扱う変数は Data Segment に格納される
+* TODO: figure of code segments with data segments
 
 # Example of Code Segment in CbC
-* Code Segment は ``__code`` を付けた関数
-* 次の Code Segment への接続は ``goto`` で表される
+* Code Segment は `__code` を付けた関数
+* 次の Code Segment への接続は `goto` で表される
 
 ```
 __code addTen(int a) {
@@ -79,7 +68,7 @@
 ```
 
 # Example of Data Segment in CbC
-* 各 Code Segment で使うデータの構造体の共用体
+* 各 Code Segment で使うデータの構造体の共用体で表現される
 
 ```
 union Data {
@@ -92,9 +81,44 @@
 };
 ```
 
-# Meta Computation in Continuation based C
+
+# メタ計算による階層化
+* CbC で書いた実装を CbC で検証していく
+    * 仕様記述も CbC で行なう
+    * 仕様のチェックも CbC で行なう
+    * 実装の記述は変更したくない
+    * どこまでがソフトウェア本体でどこまでが実装コード?
+* メタ計算で計算を階層化することで解決する
+    * 実装はノーマルレベル
+    * 検証はメタレベル
+    * メタからノーマルは見えて、ノーマルからメタは見えない
+
+# Examples of Meta Computation
+* 計算を実現するような計算
+* プログラムを生成するようなプログラム
+    * TemplateHaskell in Haskell, Template in C++, Generics
+    * コンパイル時メタプログラミング
+* 言語が特別な API を提供する
+    * method_missing, define_method in Ruby
+* プログラムがその言語処理系の挙動を変える
+    * reflection in Java
+* 副作用などの言語処理系に依存した処理を表現する
+    * Monad in Haskell
+
+# Meta Code Segment
+* メタ計算は Code Segment の接続部分に Meta Code Segment を入れることで表現できる
+* 仕様定義、仕様検証は Meta Code Segment に記述
+* 実装である Code Segment の検証を行なえば良い
+    * Input Data Segment を作成して正しい Output Data Segment を出すかチェックする
+
+# Meta Data Segment
+* Meta Code Segment に必要なデータを格納する
+* Data Segment より上位の Data Segment
+
+
+# Code of Meta Computation in Continuation based C
 * メタ計算は Code Segment の間に挟まれた Code Segment で行なう
-* 例は Data Segment を指定する Meta Code Segment `twice_stub`
+* 例: Data Segment を指定する Meta Code Segment `twice_stub`
 * ノーマルレベルからはポインタは見えないものとする
 
 ```
@@ -158,7 +182,7 @@
 
 # Verification Method of Programs Using Continuation based C
 * メタ計算として検証機構を導入する
-* 仕様は CbC で記述し、恒真の式として定義する
+* 仕様は常に成り立つべき式としてCbCで記述する
 * 仕様を満たさない Input Data Segment が無いかチェックしていく
 * 検証の対象として CbC で記述された赤黒木を用いる
 
@@ -178,13 +202,14 @@
 * 木への挿入は有限の個数だけ行なわれる
 
 # Verification Library Akasha
-* CbC のメタ計算として高さをチェックしていく
-* 深さ優先探索で挿入順番を総当たりでチェック
-* Data Segment に木が入っている
+* 本研究で作成した検証用メタ計算ライブラリ
+* 実装コードの ``meta`` を上書きするだけで検証を行なうことができる
+* 深さ優先探索で有限個の要素の挿入順番を総当たりで列挙
+* 挿入後の木はきちんとバランスしているかチェックする
 * Meta Data Segment に挿入順番や実行履歴を記憶させる
 
 # C Bounded Model Checker
-* ANSI-C の記号実行モデルチェッカ
+* Carnegie Mellon University で開発されている ANSI-C の記号実行モデルチェッカ
 * CbC は `__code` を `void` に、`goto` を `return` に変えると C Syntaxになる
 * Red-Black Tree を C に変換して検証
 * 挿入順番は非決定的な入力 `nondet_int` を使う
@@ -194,12 +219,16 @@
 * CBMC ではチェックできなかった
 * TODO: 表でまとめておく
 
+# Comparison of tools
+* valgrind, cbmc, akasha, valgrind, manual unit test
+* TODO
+
 # Conclusion and Future Works
 * CBMC では検証できない範囲の検証を行なうことができた
 * 動作するプログラムの記述を変更することなく検証を行なえた
 * 今後の課題
     * 挿入だけでなく削除を含む赤黒木の仕様検証
     * 状態の抽象化による探索の効率化
-    * ポインタへの不正アクセス検出などのプログラムに依存しない仕様チェック機能
+    * ポインタへの不正アクセス検出などの機能
 
 <!-- vim: set filetype=markdown.slide: -->