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

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.

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

If you do not provide the test file with your data sets, the tests will be run on empty data sets, meaning that most of the probably will pass without anything being tested. In order to provide test sets you should, for every type T, modify the createTestSet test generator stubs in the XTestGenerator classes.

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) };
  }
This gives a test data set of 9 elements. Note that we have repeated some of the values several times in order that, among others transitivty axioms, will get cases which fully exercises them.

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