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.

In addition to ParamStandard, there are a few other kinds of tests available in the framework:

• All tests meant to be parameterised (test w/ multiple sources as inputs).
• Standard workflow for all tests.
• 3 versions: Standard, FineGrain and Externals
• Some utility stuff (ParseTfFacade, etc.)

Working with existing tests

• how to add new inputs for existing tests;
• how to use external input files when testing (via property)
• how to inspect test failures and update results.

Writing new tests

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

Advanced

• using assumptions