現在、MicrosoftResearchによるSpecExplorer2010を評価しています。テストケースがどのように生成されるのか少し疑問に思います。
SEで生成されたテストサンプルモデル(アキュムレータ)で遊んでいます。メンバー変数に0より大きい自然数を追加するAccumulator.Addメソッドがあります。
モデルは以下を指定します:
[Rule(Action = "Add(x)")]
static void AddRule(int x)
{
Condition.IsTrue(x > 0);
accumulator += x;
}
ご覧のとおり、上記の条件(x> 0)はモデルコード内で指定されています。さらに、CORDファイル内でAccumulator.Addの可能な入力を指定しました。
config ParameterCombination: Main
{
action abstract static void Accumulator.Add(int x)
where x in {-3..3};
}
ただし、ステートメントCondition.IsTrue(x> 0)は、SpecExplorerに値> 0のテストのみを生成するように強制します。これは私が期待したものではありません。入力パラメーターの型はintであるため、正でない数をメソッドに渡すことができます。仕様により、メソッドはそのような数を許可するべきではありません。私の見解では、SEは、アルゴリズムがそれらを受け入れないことを確認するために、非正の入力を使用してテストを生成する必要があります。
この振る舞いはどういうわけかモデル化できますか?PEXはホワイトボックステスト専用であるため、PEXのようなソリューションを指摘しないでください。SEはむしろブラックボックステストに焦点を合わせており、私が学んだことから、ブラックボックステストは私の仕様に基づく等価クラスを使用して機能するはずです。それらは次のようになります。
Equivalence class 1: Positive input
Equivalence class 2: Non-positive input
ただし、SEは後者の場合のテストケースを生成しません。
助言がありますか?前もって感謝します。