-
Notifications
You must be signed in to change notification settings - Fork 21
Combinatorial Testing Guide
So what is the Combinatorial Testing Guide all about?
Right, so we looked briefly at the idea of "traces" in the User Guide. The idea is that a trace, defined within a VDM specification, can be expanded to a large number of independent tests. This expansion process is called "combinatorial testing", because we're generating tests using all possible combinations of options.
And the User Guide explains how they work?
Well, only superficially. It has to introduce them to show how to use them from the command line, which is the purpose of the User Guide. But it leaves out a lot of detail. The Combinatorial Testing Guide fills in those gaps and gives more realistic examples.
I see. So who should read this one?
It's useful for any specifier who wants to test their specification with a large number of systematically generated tests.
That sounds like most people?
It is a very important and powerful aspect of the tools, yes. Most specifications would benefit from testing with traces. At the very least you can create a trace which runs each of the one-shot tests that you've created. The tool can then be instructed to run all of your tests in a batch and show you the results, which is useful.
So can you quickly tell us how the document is structured?
It starts with a very simple example...
Always a good idea.
...and uses that to show the basic principles of how a trace is expanded, and how to use variables to define a range of values to test with. It shows what happens when individual tests fail, and how to reduce a very large set of tests while you're working on your trace.
Reduce the set of tests?
Well, for example, it may be that you invent a trace that expands to a million test cases, and it takes a few hours to run them. But while you're working on that trace or changing it, you don't want to have to run all of the tests over and over again to see whether your change is working. So you can reduce the combinatorial output, say to 1% of the total number. That would give you some idea that everything was working, or not, within a few minutes.
Ah, okay I see.
Finally, it defines how each of the possible trace expressions will expand, using a condensed notation.
Interesting. Okay, so is there more?
Yes, next it shows a few "patterns" - that is, how traces can be used to achieve certain very commonly needed results, like permutations and combinations of inputs.
Okay, I can see that would help a lot. Is the more?
Yes, then it gives two real world examples. The problem with simple examples is that, although they make it easy to understand, it's sometimes hard to see how a simple trace could be used in a much more complex system. So the real world examples show that.
What are they?
One shows traces for a faulty implementation of the Luhn check digit algorithm. The other shows traces for an ARTS retail web service. Both of them use techniques that are hopefully applicable elsewhere.
Okay, those do sound more substantial. Is there more?
Lastly, it gives the formal grammar for traces, talks about support in the various IDEs, and then gives the source listing of the models used in the real world examples. But that's all.
This really is an interesting area! Somehow it feels like something that hasn't yet been used to its full potential?
Yes, I agree. In a sense, the VDM community is still trying to work out what we can do with this. But it is very powerful.
Okay. So thanks for going through that document for us.
- TL;DR
- VDM Method
- VDMJ Overview
- VDMJ Docs for Specifiers
- VDMJ Docs for Tool Developers
- VDMJ Docs for LSP Developers