Testing

This pages describes the Overture test framework and how to use to write new tests and work with existing ones. The framework is located in core/testing/framework. The code is reasonably documented so take a look. Sample tests are also available at core/testing/samples

Framework Overview

The test framework has two guiding design principles:

• Minimize the amount of test code developers have to write by automating common tasks and providing opinionated defaults.
• Provide a standard workflow for all tests that can be used by most modules for most of their testing.

The framework works predominantly with parameterised tests. You define the basic behavior of the test and the test is repeated multiple times, with a parameter input every time. Parameters are defined by test writers. In Overture, they are almost always VDM sources.

The workflow for a test is:

1. grab the source from its path

• parse and type-check it to make an AST
• process the AST to produce some result (proof obligations, interpreter results, generated code, etc.)
• compare the produced result against a previously stored one

The primary test class in the framework (ParamStandard) automates steps 1-2, provides a mandatory hook for step 3 and an optional hook for step 4. This class should be adequate for writing most kinds of tests. However, there are a few alternatives for dealing with special cases:

• ParamFineGrainTest provides a hook for step 2. This allows it to deal with sources that do not parse or type-check correctly. This class exists mainly to help test the parser and type checker. Be warned: invoking the parser and type checker is laborious. You should not use this class unless you really need to.
• ParamExternalsTest runs tests with VDM sources available externally (that is, outside of the overture repository). Since external sources can contain errors, this is a subclass of ParamFineGrainTest. To run tests defined with this class, the path to the external sources must be passed via a Java property (see below).
• ParamNoResultFileTest runs tests that do not store results. This is a variation of ParamStandardTest but step 4 simply provides a hook to analyze the result. This class is useful for "No crash" and other kinds of tests that do not need any stored results.

Working with existing tests

There are 3 things to know when working with existing tests: how to add a new input, how to pass external inputs and how to inspect failures and update results.

In order to add a new input to an existing, place the VDM source somewhere under the root for that test. You can find the root in the test code (look for the @Parameters annotation). When you add a source for a standard test, you must use the correct extension as those are used by the framework to work out which dialect needs to be used.

In order pass the external sources to a ParamExternalsTest, use the Java VM Property externalTestsPath=/path/to/files. This property can be set in the run configurations of most IDEs. On the command line, you can do it with maven by using the argument -DexternalTestsPath=/path/to/files

When a test fails, you should see a message like this: [Input: x, Result: y, Update Property:z] along with the details of the test failure (differences in actual versus expected result, etc.). From this information, you can decide if there is a problem with the test input source (in which case, you simply edit the file) or the result file (in which case, you update it by rerunning the test while passing the listed property). Note that you only get this information for tests that fail due to assertion errors. If there is an unexpected internal tool error during the test, you will only see the standard exception stack trace.

Writing new tests

TBD. For now, look at the samples

• how to write a new test;
• how to write tests that use the external inputs;

Advanced

TBD

• using assumptions
• language releases
• bulk property passing
• great result classes