Improve test strategy

[treiher]

Motivation

• Improve maintainability of tests
• Improve test coverage by systematic testing of features and feature combination

Description

Currently, our tests are mainly based on the specification of some example protocols. Not all possible cases are covered by this approach. A more systematic testing approach should be based on a list of features (#342) and feature combinations. The list of features and feature combinations should also be used to detect and document feature disparities between the SPARK code generator and PyRFLX.

Each integration test should be based on one (or a combination of) specification(s) and cover the following parts:

• [x] Check parsability of specification
• [x] Check compilability of generated SPARK code
• [x] Check for changes in generated SPARK code (compare to known good code)
• [ ] Check correctness of generated SPARK code by unit tests
• [x] Check correctness of generated SPARK code by formal verification (GNATprove)
• [ ] Check correctness of PyRFLX code by unit tests

[senier]

I like that idea very much. We could consider applying contract-based testing (using icontract or whatever is the most suitable framework) to PyRFLX to make the case stronger.

We should discuss whether we want to do this within version 0.4 or later. For now, I moved it to 0.4 so we don't forget this discussion.

NB: I'd argue that there should be not feature disparities between SPARK and PyRFLX, at least in releases. Hence, the tests should detect those, such we can fix them.

[treiher]

Due to the separation of the example specifications into a separate repository the improvement of our test strategy gets more important. Currently, changing an example specification can lead to a high maintenance effort, which just gets evident when the specification submodule gets updated. Unit tests should always use generic test specifications located in the same repository to avoid such issues.

[treiher]

The dependency of the tests on example specifications is removed in #669 by creating copies of the currently used example specifications. These copies should be replaced by generic test specifications in the long term.