Package daikon.test.inv

Class InvariantAddAndCheckTester

  • public class InvariantAddAndCheckTester
extends Object
    This is a tester for the results of adding or checking an sample to an invariant. It can test practically any invariant in the Daikon system given the appropriate commands. The test are configured from the InvariantTest.commands file and errors that occur are written to the InvariantTest.diffs file. For conveince a partcailly complete file InvariantTest.input can be used to generate a complete commands file. To generate InvariantTest.commands from InvariantTest.input run this class's main method with option "--generate_goals".

    Each test case starts with a line containing the full name of the invariant then a second line containing the types of the arguments to the invariant's check and add method (excluding the count argument). After the test case's header any number of command lines may be included in a command file. Finally, after all command lines, the key work "end" must appear on its own line.

    Each command line is starts with a command: "add:" or "check:". Following the command comes the arguments to be checked or added to the invariant. These arguments should be in the same format as in a dtrace file. Next comes the InvariantStatus that is expected to be returned by the check or add command on checking or adding the arguments. Finally, the expected format of the Invariant after checking or adding the arguments is included. (The format of the invariant is given by "Invariant.format_using(OutputFormat.DAIKON)")

    A full example test case is as follows: 

     daikon.inv.binary.twoSequence.PairwiseIntEqual
 int_array int_array
 add: [ 1 2 3 ]; [1 2 3 ]; no_change; a[] == b[] (elementwise)
 add: [ 10 -1 6 ]; [10 -1 6 ]; no_change; a[] == b[] (elementwise)
 add: [ -3 -3 -9 ]; [-3 6 -9 ]; falsified; a[] == b[] (elementwise)
 end
    Alternatively, this class can be used to generate a test case when given command lines that do not include expected InvariantStatus or invariant format. The proper input to generate the test above would be: 
     daikon.inv.binary.twoSequence.PairwiseIntEqual
 int_array int_array
 add: [ 1 2 3 ]; [1 2 3 ]
 add: [ 10 -1 6 ]; [10 -1 6 ]
 add: [ -3 -3 -9 ]; [-3 6 -9 ]
 end
    To run a test case the method runTest should be used. To generate a test case the method generateTest should be used.

    Note: no test case should contain the character ';' in any way other than to divide arguments with in a command line.