Test Framework

Note: This guide refers to the original Overture test framework. This framework is being phased in favor of a new one (see Testing). We maintain this guide because some tests still run on the old framework but if you are creating new tests, use the new framework.

This page is a quick guide on how to write tests for overture. Mostly, you will rely on the Test Framework. The framework is quite idiosyncratic for a variety of reasons but once you get the hang of it, it can be quite useful. The test framework is in core/testframework. Have a look around if you have any questions.

A new test framework is on its way (yay!) but this should help until then. Some developers also use custom test frameworks for their stuff. But we should standardize testing at some point.

Setting up a test suite

Overture follows the Maven project structure so tests need to be in the same project as the code they are testing.

The test code goes under src/test/java/ and the test resources (input and result files) go under src/test/resources/

Start out by creating a test case class:

MyTestCase extends ResultTesCase<MyResultType>

You must then implement some methods for this class:

test()
protected abstract boolean assertEqualResults(R expected, R actual)
protected abstract File createResultFile(String filename)
protected abstract File getResultFile(String filename)
void encondeResult(MyResultType result, Document doc, Element resultElement)
T decodeResult(Node node)

Then create a test suite:

public class MyTestSuite extends BaseTestSuite {

    public static Test suite() throws IllegalArgumentException, SecurityException, InstantiationException, 
        IllegalAccessException, InvocationTargetException, NoSuchMethodException, IOException 
    {
        LexLocation.absoluteToStringLocation = false;
        String name = "My Test Suite ";
        String root = "\\src\\test\\resources\\<yourtestfolder>";
        TestSuite test = createTestCompleteFile(name, root, MyTestCase.class, "");
        return test;
    }
}

Now all you need are some test inputs. These normally take the form of VDM files. Place them under src/test/resources/. The suite will automatically go through the root folder (and subfolders) you set and use any files in it as test inputs. Files with the .RESULT extension are used to store test results.

Running the tests

The framework is based on JUnit 4. You can either run it from Eclipse as any other test (Run As > JUnit Test). Or you can run it with Maven - simply cd to the module folder and invoke mvn test.

To run tests with additional input sources from outside the repository, use mvn test -DexternalTestsPath=/path/to/tests/

If running the tests on a terminal with no graphics enabled then disable the UI test profile ui-tests. The maven argument for this is -P ui-tests. For example": mvn test -P !ui-tests.

Updating results

Test results are automatically generated and maintained by the framework. For the type checker, interpreter and pog, when you run the tests, you can either compare them to existing result files or generate new ones. To update results, simply execute the tests with the override property.

To do this run the tests under Maven with mvn test -Dtesting.ID.override.TYPE. You can also pass the property as a VM argument in Eclipse. The ID and TYPE fields are used to identify which tests you want to override results for.

ID can be tc for the type checker, po for the POG and interpreter for the interpreter. TYPE refers to the type of tests you want to override such as module.sl or all. You can check the getPropertyID() method on the various test cases to find out more possibilities.

So, for example, to regenerate all type checker test results use -Dtesting.tc.override.module.sl. Or, to regenerate all SL POG test results use -Dtesting.po.override.all.

Expanding a test suite

Once a test suite is up an running, you may simply want to expand its coverage by adding more inputs to it. This is very easy. Simply go to that suite's relevant resource folder and create additional VDM files there. For reference, here are the main resource folders for the type checker, interpreter and POG modules. These three use the test framework the most.

• src/test/resources/classes for VDMpp files
• src/test/resources/classesRT for VDM-RT files
• src/test/resources/expressions for files with plain VDM expressions (TC and interpreter only)
• src/test/resources/modules for VDM-SL files