# HG changeset patch # User Yasutaka Higa # Date 1470128187 -32400 # Node ID 68b4b331370325dd57b34420f7bdddec4704f58e # Parent 9d8b37748b1eee5f5e1b309ed80d014f734bad1a Fix slides diff -r 9d8b37748b1e -r 68b4b3313703 presentation/slide.md --- 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 の行数 +* 実行時間 +