xml description

General structure

This explanation of the TestEAS input format assumes knowledge about the [Kind 2 contracts](kind 2 contracts) formalism. In particular modes, global modes and assume-guarantee reasoning.

TestEAS expect several things in order to run test cases:

• some binaries to test
• some oracles which, given the inputs and outputs of the binaries, return the value of the specification item
• some test cases.

In TestEAS a test run is specified by several, hierarchical xml files.

Test context

The top level, called the test context must specify the oracle(s) and the test class(es). It can also contain binaries, although that's not mandatory. Binaries can be given in the command line. A test class is a family of tests and is used to separate unit from integration tests for instance.

A typical top level xml file looks like this:

<?xml version="1.0"?>
<data system="PFS">

  <oracle path="oracle/PFS_oracle">
    <output global="true">global_R1_R4</output>
    <output global="false">init_contract</output>
    <output global="false">only_one_active_R2</output>
    <output global="false">change_R3</output>
    <output global="false">unchanged_R5</output>
  </oracle>
  
  <tests>unit-tests.xml</tests>

</data>

This file only specifies one oracle and and one test class.

Oracle field

An oracle field gives the path to the runnable oracle as well as the different modes the oracle is for. The oracle should be listen to stdin and read space-separated values corresponding to the inputs of the current step of a test sequence, followed by the values output by the binary. The values ends with an EOL.

In response to these values, the oracle should produce the value for each of the modes mentioned in the top xml file, as follows. For a global mode, the value of the (conjunction of) the ensure(s) of that mode. For a mode, the value of the (conjunction of) the requirement(s) followed by the value of the (conjunction of) the ensure(s).

For example, if the oracle is specified in the top level file as

  <oracle path="oracle/PFS_oracle">
    <output global="true">global_R1_R4</output>
    <output global="false">init_contract</output>
    <output global="false">only_one_active_R2</output>
    <output global="false">change_R3</output>
    <output global="false">unchanged_R5</output>
  </oracle>

then binary oracle/PFS_oracle should return 9 booleans when fed with the inputs and the outputs of a test step. The first one is the ensure of global mode global_R1_R4, the second and third ones are the require and ensure of init_contract respectively, etc.