Spec Explorer: False tests

Question

At the moment, I'm evaluating Spec Explorer 2010 by Microsoft Research. I'm a bit wondered how test cases are generated.

I'm playing around with the test sample model (Accumulator) generated by SE. There's a method Accumulator.Add which adds a natural number > 0 to a member variable.

The model specifies:

[Rule(Action = "Add(x)")]
static void AddRule(int x)
{
    Condition.IsTrue(x > 0);
    accumulator += x;
}

As you can see, the condition stated above (x > 0) is specified within the model code. Additionally, I specified possible inputs for Accumulator.Add within the CORD file:

config ParameterCombination: Main 
{
    action abstract static void Accumulator.Add(int x)
        where x in {-3..3};    
}

But the statement Condition.IsTrue(x > 0) forces SpecExplorer to only generate tests with values > 0. This is not what I expected: the input parameter type is int, so a non-positive number could be passed into the method. By specification, the method should not allow such numbers. From my point of view, SE should generate tests using non-positive input to verify the algorithm don't accept them.

Can this behavior be modelled somehow? Please do not point me to solutions like PEX, as PEX is dedicated to white-box tests. SE rather focuses black box tests and from what I learned, a black box test should work using equivalence classes based on my specification. Those would be:

Equivalence class 1: Positive input
Equivalence class 2: Non-positive input

But SE never generates test cases for the latter case.

Any suggestions? Thank you in advance.

Answer 1

Afaik Spec Explorer will generate tests based on the exploration done on the model. So if a rule does not fire because of a failing (Pre-)Condition, Spec Explorer won't create tests.

My suggestion to model this, is to do the creation of equivalence classes manually, i.e. create another rule for negative values, but for the same action:

[Rule(Action="Add(x)")]
static void AddRule2(int x)
{
   Condition.IsTrue(x <= 0);
}

The configuration-file as well as the implementation can stay the same and the test-suite will report an error if a negative value is added (I just tried that).

You will also need to create a second rule for negative values, or remove the condition at the beginning.