Combinatorial Testing - overturetool/vdm-vscode GitHub Wiki
In order to better automate the testing process, a notion of test traces has been introduced into VDM. Traces are effectively regular expressions that can be expanded to a collection of test cases. Each test case comprises a sequence of operation calls. If you define a trace it is possible to make use of a special Combinatorial Testing View to automatically expand the trace and execute all of the resulting test cases. Subsequently, the results from the tests can be inspected and erroneous test cases easily found. You can then fix problems and re-run the trace to check they are fixed.
The syntax for trace definitions is defined in the VDM-10 Language Manual. If you have created a traces entry for a module or class it can be executed via the Combinatorial Testing view found in the left side of the VS Code window. Different icons are used to indicate the verdict in a test case. These are:
- Green: The test case has passed.
- Red: The test case has failed.
- Blue: The result of the test case is inconclusive.
- Grey: The test case has been filtered, i.e., not executed since it is known that it will pass based on the result of another test case.
- No icon: The test case has not been executed yet.
In the CT view, you can right-click on any individual test case, and then send it to the interpreter for execution (Send test to interpreter). This is particularly useful for failed test cases since the interpreter allows you to step through the evaluation to the place where it is failing. You can inspect the exact circumstances of the failure, including the values of the different variables in scope.
If you want to add filtering options, which will reduce the number of executed tests based on the configuration, click on the button Set Filter Options and a window will appear.
| Filter Option | Description |
|---|---|
| Trace Reduction Type | Filtering type |
| Trace Filtering Seed | Use a specific seed for "randomly" selecting test cases to execute |
| Subset Limitation (%) | Limit the number of executed tests to a certain amount |
| Reset | Reset all the filter options |
| OK | Confirm Changes |
The filter options are used when you execute the test trace with the button (Filtered Evaluation).
If you want to filter the combinatorial tests based on their verdict, you can click on (Show selected tests) and select one or many options between: ’Passed’, ’Failed’, ’Inconclusive’ and ’Filtered’.
You can also rebuild the trace outline with the button (Rebuild Trace Outline), or collapse all tests with the button (Collapse All). Finally, you can also navigate to the trace (Go to trace).
Trace Coverage Display
Execution coverage is collected cumulatively during trace execution. Typically, one or more trace executions would be performed and then the coverage information saved via the VDM >> Generate Coverage menu option. Using the coverage icon in an editor display will then overlay the coverage on the source file(s). See Coverage.