Mercurial > hg > Papers > 2016 > atton-ipsjpro
changeset 57:728bbe91b6a2
Update slide
| author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 05 Aug 2016 17:01:36 +0900 |
| parents | c361708587eb |
| children | 21c3332c2578 |
| files | presentation/slide.md |
| diffstat | 1 files changed, 20 insertions(+), 25 deletions(-) [+] |
line wrap: on
line diff
--- a/presentation/slide.md Thu Aug 04 18:53:59 2016 +0900 +++ b/presentation/slide.md Fri Aug 05 17:01:36 2016 +0900 @@ -28,9 +28,8 @@ * モデル検査用に特化した言語で実装を記述する必要がある # Akasha の目的 -* 実装言語そのものを検査する - * 実装に入り込むバグをする - * 単語の打ち間違いによるバグ +* 実装そのものを検査する + * 実装に入り込むバグを見付ける * 高速かつ網羅的に検査する * メタ計算の切り替えで様々な検証を行なう * 高速なメタ計算が行なえる言語(CbC) を用いる @@ -58,30 +57,27 @@ ``` __code addTen(struct Count c) { - struct Port p; - p.port = c.x+10; - goto twice(p); + c.x = c.x+10; + goto twice(c); } -__code twice(struct Port p) { - p.x = p.x*2; - goto showValue(p); +__code twice(struct Count c) { + c.x = c.x*2; + goto showValue(c); } ``` # CbC のメタ計算 * Code Segment 間の接続はメタ計算レベルで行なわれる -* Code Segment で使われる Data Segment は Meta Data Segment である Context に全て定義されている -* ポインタの扱いや並列実行はメタ計算レベルで行なう * メタ計算も Code Segment と Data Segment で表現される - * メタレベルではポインタを扱っても良い + * ポインタの扱いや並列実行はメタ計算レベルで行なう {:width="50%"} # CbC のメタ計算の実際 -* プログラムで使用する Data Segment は Meta Data Segment で全て定義されている +* Code Segment で使われる Data Segment は Meta Data Segment である Context に全て定義されている ``` union Data { @@ -96,7 +92,6 @@ struct Context { union Data *data; // Data Segment unsigned int gotoCount; // メタ計算に必要なデータ - unsigned int stepOfAddTen; }; ``` @@ -157,7 +152,7 @@ # Verification Method of Programs Using Continuation based C * メタ計算として検証機構を導入する * 仕様はCbCで記述する - * どのような状態でも成り立つべき式として定義 + * 常に真になるべき式として定義 * 仕様を満たさない Input Data Segment が無いかチェックしていく * 検証の対象として CbC で記述された赤黒木を用いる @@ -197,18 +192,20 @@ * CBMC では検証できない範囲の検証を行なうことができた * 総当たりでチェックしているため扱えるサイズは小さい * CBMC に比べ高速 + * 有限の個数しか扱えない * ポインタアクセスに由来するバグなどは見付けられない # Comparison of tools -| | akasha | cbmc | unit test | Spin | 証明 | JavaPathFinder | valgrind | -|------------------------|:----------:|:--------------:|:----------:|:------------:|:------------:|:---------------:|:--------:| -| 検証用に実装の変更 | 必要なし | 必要なし | 必要なし | 別に記述 | 別に記述 | 必要なし | 必要なし | -| 検証用に記述する言語 | 実装と同じ | 実装とほぼ同じ | 実装と同じ | 実装と異なる | 実装と異なる | 必要なし | 必要なし | -| 仕様の検証 | 可能 | 可能 | 不可能 | 可能 | 可能 | 不可能 | 不可能 | -| メモリリークなどの検出 | 不可能 | 可能 | 不可能 | 不可能 | 不可能 | 不可能 | 可能 | -| 状態の数え上げ | 可能 | 可能 | 不可能 | 可能 | 不可能 | 可能 | 不可能 | -| 反例の表示 | 可能 | 可能 | 不可能 | 可能 | 不可能 | 不可能 | 不可能 | +| | akasha | cbmc | unit test | Spin | 証明 | JavaPathFinder | valgrind | +|------------------------|:--------------:|:--------------:|:----------:|:------------:|:------------:|:---------------:|:--------:| +| 検証用に実装の変更 | 必要なし | 必要なし | 必要なし | 別に記述 | 別に記述 | 必要なし | 必要なし | +| 検証用に記述する言語 | 実装と同じ | 実装とほぼ同じ | 実装と同じ | 実装と異なる | 実装と異なる | 必要なし | 必要なし | +| 仕様の検証 | 可能 | 可能 | 不可能 | 可能 | 可能 | 不可能 | 不可能 | +| メモリリークなどの検出 | 不可能 | 可能 | 不可能 | 不可能 | 不可能 | 不可能 | 可能 | +| 状態の数え上げ | 可能 | 可能 | 不可能 | 可能 | 不可能 | 可能 | 不可能 | +| 反例の表示 | 可能 | 可能 | 不可能 | 可能 | 不可能 | 不可能 | 不可能 | +| 赤黒木の検証 | 有限個まで保証 | 検証できず | | | | | | # Future Works @@ -235,8 +232,6 @@ * method_missing, define_method in Ruby * プログラムがその言語処理系の挙動を変える * reflection in Java -* 副作用などの言語処理系に依存した処理を表現する - * Monad in Haskell * CbC では関数呼び出しが存在していないのでメタ計算を挟むことが容易