This is an example of JAxT specifications and useage prepared for testing with JUnit. The JAxT approach allows us to systematically write properties as axioms, axioms which are used as basis for systematic JUnit testing. We thereby shift the testing focus from individual test cases, to more general properties of the software under development. Hopefully this will give better and more systematic support for test-oriented software development methods, see the wikipedia List of software development philosophies for a superficial overview of these and other software design methods.

JAxT can also be thought of as a merging between design by contract and systematic testing: the contract is formalised by the axioms associated with interfaces and classes, while JAxT generates JUnit tests for checking adherence to the contract.

Writing a contract

An immediate contract is a class or an interface X together with a collection of axioms. The axioms are written in (one or more) abstract public classes XAxioms, which implement the interface jaxt.framework.Axioms and which extends or implements X (depending on whether X is a class or an interface),

The interface jaxt.framework.Axioms is empty, and its only purpose is to allow the JAxT tool to identify that a class XA is an axiom class. By letting XA extend or implement X, JAxT can easily figure out which axioms are declared for X. The axioms may be grouped in several different classes XA, e.g., separating absolute requirements from recommended behaviour. Consider the method java.lang.Comparable<T>.compareTo(T) - it is required to be an equivalence relation, but it is only recommended that this equivalence relation is the same as the equivalence relation given by java.lang.Object.equals(Object).

Each axiom in a class XA is a static public void method. An axiom may have free variables, which are coded as formal arguments to the method. Then the axiom may do any computation needed to check a property on its arguments. The checking is normally done using assertions from the junit.framework.Assertions class. It is normal to statically import all the assertion methods from this class for XA. Thus the axioms are formally written in a Java/JUnit specific logic. Pragmatically the assertion language lets us check for

• equality using assertEquals(Object, Object), which checks that both objects are equal with respect to the method java.lang.Object.equals(Object).
• object identity using assertSame(Object, Object), which checks that two object arguments refer to the same Object.
• satisfaction using assertTrue(boolean), which checks that the boolean expression is true.
• contradiction using assertFalse(boolean), which checks that the boolean expression is true.
• inconsistency using assertFail(), which claims failure of the axiom - and is used in the checking of exceptions, see e.g. jaxt.java.lang.CompareableAxioms.compareToProperty6strongSymmetry(Comparable, Comparable).

All of these assertions also exist for the Java primitive types.

By convention an axiom class XA, where possible, should reside in the same package as X. In the current release of JAxT, this is a requirement, and there is only one exception: Axioms for the standard Java classes and interfaces are placed in jaxt.java.lang etc.

The class X should of course satisfy all its immediate contracts XA, but also all contracts for any class it inherits from or it implements, either directly or indirectly. Thus any class in Java will need to satisfy the requirments on java.lang.Object, since every Java class inherits from it, either directly or indirectly.

Generating JAxT tests

When using JAxT within Eclipse, it works in much in the same way as generating JUnit tests from within Eclipse.

First you go to the Package Explorer and select the Java file X.java that contains the class X you want to test. Then you right-click on your selection and select Mould->Create Tests from the popup menu (towards the bottom part of the menu).

You will now find the file XTest.java alongside with the class X.java in your package. Following the defaults, XTest will be a functioning JUnit test class, except possibly for missing test data sets. See the next section on how to add these.

Additionally, for every type T in every axiom beloning to X, a test generator class TTestGenerator will be generated containing a method createTestSet(). By filling in this method, you provide the necessary test tests for that type.

The generated JUnit test case will be a public class XTest inheriting from junit.framework.TestCase and the file has all necessary imports. The test class itself will normally consist of the following.

• Constructor public XTest(String name) as used by JUnit.
• A fixture consisting of the methods setUp() and tearDown(). The method setUp() is called by JUnit before each test method, and tearDown() is called after each test method. The setUp() method is typically where the test data are computed.
• A test method for each axiom. The test method will call the axiom inside a nested loop which runs through the data set for each argument of the axiom. So an axiom a1(Object, int) will be inside a double loop, running through all elements of the test data sets dataObject and dataInt. An axiom a2(), with no free variables, will not need any data loop and just be called as is.
• For every argument type T, e.g., Object, int, X, Comparable, in the collection of axioms, there will be declared a data set T[] dataT, e.g., Object[] dataObject, int[] dataInt, X[] dataX, Comparable[] dataComparable. These attribute variables need not be arrays, but must be a collection type with an iterator on the corresponding element type.
• For each declared data set dataT, the setUp() method will be extended with the initialisation of this data.
• If the data is for X or a supertype of X, a call to the (fictive) static method XTestGenerator.createTestSet() will be inserted. For instance, dataObject = XTestGenerator.createTestSet(), dataX = XTestGenerator.createTestSet(), dataComparable = XTestGenerator.createTestSet().
• If the data is for Y, a subtype or unrelated type for X, a call to the (fictive) static method YTestGenerator.createTestSet() will be inserted. For instance, dataY = YTestGenerator.generateTestData().

You should never modify the code in a generated test, such as XTest. The current version of JAxT will unconditionally overwrite your changes next time you generate the tests.

What you must modify, however, are the XTestGenerator classes. For each argument type T of every axiom tested in the XTest a TTestGenerator class will be generated with a stub method T[] createTestSet(). You should fill in this method to provide an array (or you can change the return type to a Collection) of testable objects of type T. JAxT will never overwrite an existing TTestGenerator so you may modify it freely.

Writing test data sets

The simplest extension is to simply return a few test cases in place of the original empty set of cases. For example, consider a class X with a default constructor and a constructor that accepts an integer argument. In the corresponding XTestGenerator class you may want to implement the createTestSet() method like this:

  X[] createTestSet() {
    return new X[] { new X(), new X(100), new X(0), 
                     new X(-1), new X(1), new X(100), 
                     new X(100000), new X(), new X(100) };
  }

With the JAxT approach it is easy to provide much larger data sets, e.g., using the Java random number generator. Assume we have an axiom with free variables of type int. The JAxT generated test will then have an intTestGenerator class with a stub createTestSet(). We can easily let it provide the tests with 100 randomly chosen integers between 1 and 50 (note the oversampling in order to get several equal values).

  int[] createTestSet() {
    Random g = new Random();
    int[] dataInt = new int[100];
    for(int i=0; i
Remember to add the necessary import java.util.Random.



Of course this technique can also be used for the class X 
if it needs a larger test data set.
It can then be useful to place a method computing the data set in the class X
itself, and just call this method in the XTestGenerator class.
This has been done in the package jaxt.example.position,
where the static method Position.positionDataSet() creates 200
Position values for use in the tests.



Be warned that large data sets for axioms with many free variables takes its time to check.
A data set of 500 elements may be used to check axioms of 1-2 free variables in a few seconds.
But applying that test set to an axiom with four free variables, e.g. for checking the congruence of a binary operation like
jaxt.examples.position.Position.plus(Position), we get 500^4 = 62 500 000 000 tests.
An overnight job for any reasonable computers.



In general you can also change the return 
  type of a TTestGenerator.createTestSet() from the array type T[] to a Collection) of testable objects of type 
  T. Make certain your collection class has iterators of the appropriate element type T.



  The TTestGenerator.createTestSet() method may require
  support from additional generator methods in T. It is
  recommended that these be declared with package visibility,
  so that they do not come part of the external interface of 
  T unless you explicitly think these could be useful.


  


@see jaxt.framework.Axioms
@see jaxt.java.lang
@see jaxt.examples
@author Magne Haveraaen & Karl Trygve Kalleberg, 2007