Mercurial > hg > Papers > 2016 > atton-ipsjpro

changeset 55:3d80db3be1b6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Update slides
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Thu, 04 Aug 2016 18:46:58 +0900
parents a0bffeced069
children c361708587eb
files presentation/slide.md
diffstat 1 files changed, 19 insertions(+), 19 deletions(-) [+]
line wrap: on
line diff
--- a/presentation/slide.md	Thu Aug 04 18:23:40 2016 +0900
+++ b/presentation/slide.md	Thu Aug 04 18:46:58 2016 +0900
@@ -136,20 +136,6 @@
 ```
 
 
-# 他の言語でのメタ計算
-* 計算を実現するような計算
-* プログラムを生成するようなプログラム
-    * TemplateHaskell in Haskell, Template in C++, Generics
-    * コンパイル時メタプログラミング
-* 言語が特別な API を提供する
-    * method_missing, define_method in Ruby
-* プログラムがその言語処理系の挙動を変える
-    * reflection in Java
-* 副作用などの言語処理系に依存した処理を表現する
-    * Monad in Haskell
-* CbC では関数呼び出しが存在していないのでメタ計算を挟むことが容易になっている
-
-
 
 # Meta Code Segment を使った実際の検証
 * goto する時に必ず通る Meta Code Segment `meta` を作る
@@ -181,13 +167,13 @@
 
 # Verification Method of Programs Using Continuation based C
 * メタ計算として検証機構を導入する
-* 仕様は常に成り立つべき式としてCbCで記述する
+* 仕様はCbCで記述する
+    * どのような状態でも成り立つべき式として定義
 * 仕様を満たさない Input Data Segment が無いかチェックしていく
 * 検証の対象として CbC で記述された赤黒木を用いる
 
 # Red-Black Tree
 * 赤黒木とは木構造のデータ構造
-* 各ノードに赤と黒の色を割り当て、その色を用いて木のバランスを取る
 * 赤黒木の条件:
     * 各ノードは赤または黒の色を持つ
     * ルートの色は黒である
@@ -205,7 +191,7 @@
     * 深さ優先探索で有限個の要素の挿入順番を総当たりで列挙
     * 挿入後の木はきちんとバランスしているかチェックする
 * CbC のメタ計算 Akasha では要素数13個までチェックできた
-* 実装にわざとバグを入れた場合にはバランスしていない入力例を返した
+* 実装にわざとバグを入れた場合にはバランスしない入力例を返した
 
 # C Bounded Model Checker
 * Carnegie Mellon University で開発されている記号実行モデルチェッカ
@@ -220,7 +206,9 @@
 * 動作するプログラムの記述を変更せず検証を行なえた
     * テストケースの自動生成+仕様の反例表示ができた
 * CBMC では検証できない範囲の検証を行なうことができた
-    * 総当たりでチェックしているため
+    * 総当たりでチェックしているため扱えるサイズは小さい
+        * CBMC に比べ高速
+* ポインタアクセスに由来するバグなどは見付けられない
 
 # Comparison of tools
 
@@ -238,7 +226,7 @@
 * 挿入だけでなく削除を含む赤黒木の仕様検証
 * 状態の抽象化による探索の効率化
 * ポインタへの不正アクセス検出などの機能
-* 言語処理系に検証を行ないやすくする機構の導入
+* CbC コンパイラに検証を行ないやすくする機構の導入
 
 # CBMC Informations
 * CBMC 5.4
@@ -249,6 +237,18 @@
     * 赤黒木部分のみ: 330行
     * スタックやメモリのアロケータなどを含める: 640行
 
+# 他の言語でのメタ計算
+* 計算を実現するような計算
+* プログラムを生成するようなプログラム
+    * TemplateHaskell in Haskell, Template in C++, Generics
+    * コンパイル時メタプログラミング
+* 言語が特別な API を提供する
+    * method_missing, define_method in Ruby
+* プログラムがその言語処理系の挙動を変える
+    * reflection in Java
+* 副作用などの言語処理系に依存した処理を表現する
+    * Monad in Haskell
+* CbC では関数呼び出しが存在していないのでメタ計算を挟むことが容易になっている
 
 
 <!-- vim: set filetype=markdown.slide: -->