Spec Explorer and Design by Contract

Question

Just wondering if there is any way of combining the idea of DbC with Spec Explorer.

My current understanding with my as yet limited use of Spec Explorer is that the model needs to produce an exact result of how the system should behave (for the given behaviour we are interested in), which will be compared with the actual results from the SUT. The result can be the return value of the rule method, or out parameters. A simple equality comparison between model results and SUT results is all that is available.

However, there are times when the model may not be able to work out the exact response - rather, the best we might be able to do is to specify some logical postconditions. For example, if our system is supposed to be able to find prime factors of a number, maybe it's too hard to model that (without just copying the real implementation etc). In that case, I'd like my model to be able to say - whatever result you get, you should be able to multiply them together to get the original number.

So, I can't return any exact value from my model, but I certainly know how to check the result that the SUT gives me.

So instead of just saying, here is a value from the model, see if it is exactly equal to the actual result, I want to do some other comparison with the actual value - like is it greater than this, or if you multiply all these together, do you get this, etc.

Of course, you could just put pre/post conditions in the actual system code, using CodeContracts, but I kind of liked the idea of putting them in the Spec Explorer model, as to me, it really is part of the logical model of the system, just specified in a slightly different way.

Does this make sense ?

Thanks ! :)

Answer 1

I guess I can put the postconditions in the adapter code. Again, a little separate from the model, but not too bad.

If I really can't determine an exact result in the model, then I'll have to make the model rule method not return anything, so that no checking occurs in the generated tests. The actual checking will then happen in the adapter code.

Answer 2

Hi Guraaku,

You have already given the main-stream solution to your question.
To show some more of Spec Explorer:

You can easily switch an output to an input within the model.
This sounds strange, but it works like this:
Assume you have the SUT-function

        static int AddOneRule(int x)
        {
            return (x+1);
        }

In the model you can now simply switch the ouptut to an input using the method attribute - using exactly this SUT-function and no test adapter is needed:

        [Rule(Action = "AddOneRule(x)/result")]
        static void AddOneRule(int x, int result)
        {
            Condition.IsTrue(x == 0 | x == 1);
            Condition.IsTrue(result == x + 1);
        }

Now as long as everything is exactly known, this is not a major trick for Spec Explorer:
Spec Explorer knows the inputs and outputs before test execution anyway.

In your case the model can't determine the result.
So you have a problem now: how can I explore the model, if I don't
know what the input “result” is? For example you only know that result can be divided by 3:

        [Rule(Action = "AddOneRule(x)/result")]
        static void AddOneRule(int x, int result)
        {
            Condition.IsTrue(x == 0 | x == 1);
            Condition.IsTrue(result %3 == 0 );
            Combination.KeepUnexpanded(result);

        }

Now you can see I added another thing: I keep “result” symbolic or unexpanded.
The effect in our case is now, that the test will call the SUT-function, takes it and checks if “result” can be devided by 3!
By the way you can also treat an input like x symbolically.
All symbolic treatment is experimental (though it works terrific). I haven't tested this one,
but I think this is a possibilty to move all your post-conditions into the model.

Hope this helps.

Answer 3

Hi Bububa,

Thanks for that :)

I've tried your suggestion, and it works well - I'm able to put the postconditions in the model, where I want them :)

Thanks again !