TTwo Example

Example

Here is a simple class called SortedList (There is an error in it, perhaps you can see where?).

public class SortedList {

    private LinkedList<Comparable> s ;     //   I keep the list here
    private Comparable max ;                  //   I also want to maintain a pointer to the max-element

    /**
     * A constructor to make an empty list.
     */
    public SortedList() { s = new LinkedList<Comparable>() ; }

    /**
     * Insert x into the list; maintain the list sorted, and relink max
     * accordingly.
     */
    public void insert(Comparable x) {
        int i = 0 ;
        for (Comparable y : s) {
            if (y.compareTo(x) > 0) break ;
            i++ ; }
        s.add(i,x) ;
        if (max==null || x.compareTo(max) < 0) max = x ;   
    }

    /**
     * Retrieve the max-element from the list. The list should not be empty.
     */
    public Comparable get() {
        Comparable x = max ;
        s.remove(max) ;
        max = s.getLast() ;
        return x ;
    }
}
}

You can use T2 directly to test this class, though you'll probably get false errors. But anyway, using T2 is very easy:

java -ea -cp T2.jar Sequenic.T2.Main MySortedList

This will probably report an error, complaining about null receiver within the method "get". This error is a false error, because we're not supposed to call get on a list with an empty "s". However, so far this is an informal specification. We need to make this explicit.

You can write specifications in plain Java. T2 does not require you to write complete specifications. It's up to you. Weaker specifications are easy to write. Stronger specs filter out more false errors and identify more true errors.

For example, we'll add the following class invariant and specification for "get" to the above class. These specifications are very weak, but is sufficient to identify the error in the class.

public class SortedList {

     ... // as above

     /**
      * A class invariant can be encoded as a (private) method returning a
      * boolean. T2 will check if it holds after each method call.
      */
     private boolean classinv() {  return s.isEmpty() || s.contains(max) ; }


     /**
      * We can write a specification for the method "get" by adding
      * assertions into it; or alternatively, if you don't want to clutter
      * the method, as a separate method named "get_spec" as below.
      * This get_spec MUST have exactly the same signature as get.
      */
     public Comparable get_spec() {
         // Express your pre-condition here. IMPORTANT: mark it with "PRE". 
         assert !s.isEmpty() : "PRE" ;
         // Call the specified method:
         Comparable ret = get() ;
         // Express the post-condition. If you want, you can also
         // catch exceptions, and express specifications as to
         // what the state should be when they are thrown.
         assert s.isEmpty() || ret.compareTo(s.getLast()) >= 0 : "POST" ;
         // Pass on the value returned by get:
         return ret ;
     }
}

Again we can run RT2 as before:

java -ea -cp T2.jar  Sequenic.T2.Main MySortedList

This time, it will report a real error. Note that the error is caught, despite the very partial specifications we have given.

T2 comes with lots of options; e.g. you can specify how many tests to generate, which methods you want to include or exclude, etc. Check out the Manual.