Think Stitch
  最近の更新


非決定的選択構文 AMB

Pthread Model Checker version 1.3.0 をリリースしました.

今回のリリースでは非決定的選択構文 AMB というものを追加しました.

構文は次のとおりです:

AMB stmt1 OR stmt2

意味は stmt1 または stmt2 のどちらか一方を非決定的に(任意に)選んで実行するというものです.

例えば次の例では x の値は 0 または 1 になります:

int x;
AMB x = 0; OR x = 1;
assert(x == 0 || x == 1);

一般に,プログラムでは外部からの入力や内部の計算の結果で振る舞いを変えます.このようなプログラムを検査したいとき,実際に外部から入力をもらったり,計算部分をそのまま入れたりすることはできません.そうするとある範囲の値について調べたいときに,いちいち定数を書き換えて検査することになり面倒です.

しかし非決定的選択構文 AMB を使えばパラメータの選択を自動的に行えるので便利です. 1つのモデルで複数のケースを検査しているような感じになります.

上の例では 0 または 1 の2値でしたが,AMB があれば任意の値を選択することができます.例えばつぎのようにします:

int main(void)
{
    int x;
    for (x = 0; x < 10; ++x) {
        AMB {
            ;
        } OR {
            break;
        }
    }
    assert(x >= 0 && x <= 10);
    return 0;
}

0  モデルを実行可能にする

AMB という構文はC言語にはありませんから,このままだとモデルをコンパイルして実行することはできなくなってしまいました.しかし次のようなヘッダファイルを用意して include すれば Pthread Model Checker は無視しますから実行可能なモデルを維持できます.

#include <stdlib.h>

#define AMB if (rand() % 2)
#define OR  else

テストに応じて乱数の種や確率分布をかえるとよいでしょう.あるいは選択の系列を用意してシナリオ検査をすることもできますね.

2017/10/11

© 2013-2017 PRINCIPIA Limited