JMLTestsDesign

JMLTests Design

This page contains some rough design notes and ideas. Eventually we'll describe the actual design here.

XML-based Test Descriptions

The current design concept is to use XML specifications to describe the tests while still supporting *.java files on disk as the actual test inputs. The XML test specfications could indicate the expected results of running the test at a variety of levels of detail.

Below are some of very rough examples to give an idea of what this might look like. (These are just intended to give a flavor for the idea. Dominique Schneider's work, posted to the jmlspecs-developers list on June 4, 2009 is also informative.)

Using XML-based test specifications would allow (reasonably) writable tests but simplify the task of creating test adapters for individual projects. For example, one could extend the appropriate JUnit framework classes to create a JUnit adapter that ran the XML-specified tests. Developers of individual JML-based tool good extend these adapters to use the JMLTests for their tools.

Example 1

<testcase>
    <input>
        <file name="Requires1.java">
    </input>
    <output type="positive" />
</testcase>

Example 2

<tests>
    <testcase>
        <input>
            <file name="Requires1.java">
        </input>
        <output type="positive" />
    </testcase>
    <testcase>
        <input>
            <methodspec>
                //@ requires x != \old(x);
                public void foo() {}
            </methodspec>
        </input>
        <output type="negative">
            <contains>
                not in scope
            </contains>
            <exact tool="JAJML">
                <file name="NotInScope.java" />
            </exact>
        </output>
    </testcase>
</tests>

Example 3

<tests>
    <testcase>
        <input>
            <file filter="*OK.java />
        </input>
        <output type="positive" />
    </testcase>
    <testcase>
        <input>
            <file filter="*Bad.java />
        </input>
        <output type="positive" />
    </testcase>
</tests>

Test Structure

Here's an idea for how we might structure the subdirectories of the project and how a client project might use the tests.

• JMLTests
  • Tests -- a hierarchy of folders containing test inputs, each folder would contain a tests.xml file, somewhat analogous to Schneider's suites.xml, describing the tests in that folder. The tests.xml file would also associate tags with tests, which is unlike Schneider's embedding of tags in comments within the test inputs.
  • org.jmlspecs.JMLTests
  • JUnit -- contains adapter classes that extend appropriate JUnit classes and can themselves be extended within client projects to access the JMLTests suite, provide methods that can be overridden in individual projects to specify how to run checks, compile code, or execute generated code using those projects
  • other adapter packages
• JAJML (for example)
  • testConfig.xml -- describes the tests from the JMLTests suite that should be included for this project (This is similar to the components section of the config.xml file from Schneider's work, though it also would include the tags idea from his suites.xml.)
  • TestSuite.java -- extends the appropraite adapter class from JMLTests project to allow JUnit execution of tests, defines how to execute JAJML on a given test input
  • regression.xml -- describes the expected pass/fail status of the tests so that tools can detect regressions even if project doesn't yet pass all of the tests in the test suite