Mercurial > hg > Papers > 2016 > atton-ipsjpro

changeset 51:68b4b3313703

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix slides
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 02 Aug 2016 17:56:27 +0900
parents 9d8b37748b1e
children 02e5ae71c319
files presentation/slide.md
diffstat 1 files changed, 32 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- a/presentation/slide.md	Tue Aug 02 16:56:14 2016 +0900
+++ b/presentation/slide.md	Tue Aug 02 17:56:27 2016 +0900
@@ -90,10 +90,15 @@
     * 実装の記述は変更したくない
     * どこまでがソフトウェア本体でどこまでが実装コード?
 * メタ計算で計算を階層化することで解決する
-    * 実装はノーマルレベル
-    * 検証はメタレベル
+    * 実装はノーマルレベル、検証はメタレベル
     * メタからノーマルは見えて、ノーマルからメタは見えない
 
+# 階層化のメリット
+* メモリ管理などの検証が難しい部分もメタレベルで行なう
+    * 検証するべきノーマルレベルはシンプルになる
+    * ノーマルレベルではポインタが出てこない
+* メモリ管理アルゴリズムの切り替えも楽になる
+
 # Examples of Meta Computation
 * 計算を実現するような計算
 * プログラムを生成するようなプログラム
@@ -218,19 +223,41 @@
 # Result of Verification
 * CbC のメタ計算 Akasha では要素数13個までチェックできた
 * CBMC ではチェックできなかった
-* TODO: 表でまとめておく
+
+|                                  | akasha | CBMC |
+|----------------------------------|:------:|:----:|
+| 要素数1個までは仕様を保証        | 可     | 不可 |
+| 要素数13個までは仕様を保証       | 可     | 不可 |
+| 実装にバグを入れた際に反例を表示 | 可     | 不可 |
+
 
 # Comparison of tools
-* valgrind, cbmc, akasha, valgrind, manual unit test
-* TODO
+
+|                        | akasha     | cbmc           | unit test  | Spin         | 証明         |  JavaPathFinder | valgrind |
+|------------------------|:----------:|:--------------:|:----------:|:------------:|:------------:|:---------------:|:--------:|
+| 検証用に実装の変更     | 必要なし   | 必要なし       | 必要なし   | 必要         | 必要なし     | 必要なし        | 必要なし |
+| 検証用に記述する言語   | 実装と同じ | 実装とほぼ同じ | 実装と同じ | 実装と異なる | 実装と異なる | 必要なし        | 必要なし |
+| 仕様の検証             | 可能       | 可能           | 不可能     | 可能         | 可能         | 不可能          | 不可能   |
+| メモリリークなどの検出 | 今は不可能 | 不可能?        | 不可能     |              |              |                 | 可能     |
+| 状態の数え上げ         | 可能       | 可能           | 不可能     | 可能         | ものによる   | 可能            |          |
+| 反例の表示             | 可能       | 可能           | 不可能     |              |              | 不可能          |          |
+
 
 # Conclusion and Future Works
 * CBMC では検証できない範囲の検証を行なうことができた
 * 動作するプログラムの記述を変更することなく検証を行なえた
+    * テストケースの自動生成+仕様の反例表示ができた
 * 今後の課題
     * 挿入だけでなく削除を含む赤黒木の仕様検証
     * 状態の抽象化による探索の効率化
     * ポインタへの不正アクセス検出などの機能
+    * 言語処理系に検証を行ないやすくする機構の導入
+
+# TODO: おまけ
+* cbmc のバージョン、オプション
+* rbtree の行数
+* 実行時間
+
 
 
 <!-- vim: set filetype=markdown.slide: -->