Sample output from Daikon dynamic invariant detector

This is a simple example of Daikon's ouput. The colored annotations starting with @ (in JML format) were automatically detected by Daikon and automatically inserted in the source code.
package DataStructures;

// StackAr class
//
// CONSTRUCTION: with or without a capacity; default is 10
//
// ******************PUBLIC OPERATIONS*********************
// void push( x )         --> Insert x
// void pop( )            --> Remove most recently inserted item
// Object top( )          --> Return most recently inserted item
// Object topAndPop( )    --> Return and remove most recently inserted item
// boolean isEmpty( )     --> Return true if empty; else false
// boolean isFull( )      --> Return true if full; else false
// void makeEmpty( )      --> Remove all items
// ******************ERRORS********************************
// Overflow and Underflow thrown as needed

/**
 * Array-based implementation of the stack.
 * @author Mark Allen Weiss
 */
public class StackAr
{
    //@ invariant this.theArray != null;
    //@ invariant \typeof(this.theArray) == \type(java.lang.Object[]);
    //@ invariant this.topOfStack >= -1;
    //@ invariant this.topOfStack <= this.theArray.length-1;
    //@ invariant (\forall int i; (this.topOfStack+1 <= i && i <= this.theArray.length-1) ==> (this.theArray[i] == null));
    //@ invariant (\forall int i; (0 <= i && i <= this.topOfStack) ==> (this.theArray[i] != null));
    //@ invariant theArray.owner == this;


    //@ requires capacity >= 0;
    //@ ensures \old(capacity) == this.theArray.length;
    //@ ensures this.topOfStack == -1;
    /**
     * Construct the stack.
     * @param capacity the capacity.
     */
    public StackAr( int capacity )
    {
        theArray = new Object[ capacity ];
        //@ set theArray.owner = this;
        topOfStack = -1;
    }

    //@ ensures (\result == false)  ==  (this.topOfStack >= 0);
    //@ ensures (\result == true)  ==  (this.topOfStack == -1);
    /**
     * Test if the stack is logically empty.
     * @return true if empty, false otherwise.
     * @observer
     */
    public boolean isEmpty( )
    {
        return topOfStack == -1;
    }

    //@ ensures (this.topOfStack < this.theArray.length-1)  ==  (\result == false);
    /**
     * Test if the stack is logically full.
     * @return true if full, false otherwise.
     * @observer
     */
    public boolean isFull( )
    {
        return topOfStack == theArray.length - 1;
    }


    //@ modifies this.theArray[*], this.topOfStack;
    //@ ensures (\forall int i, j; (\old(this.topOfStack)+1 <= i && i <= this.theArray.length-1 && \old(this.topOfStack+1) <= j && j <= \old(this.theArray.length-1) && (i-(\old(this.topOfStack)+1)) == (j-(\old(this.topOfStack+1)))) ==> ( this.theArray[i] == \old(this.theArray[j]) ));
    //@ ensures this.topOfStack == -1;
    /**
     * Make the stack logically empty.
     */
    public void makeEmpty( )
    {
        java.util.Arrays.fill(theArray, 0, topOfStack + 1, null);
        topOfStack = -1;
    }

    //@ ensures (\result != null)  ==  (this.topOfStack >= 0);
    //@ ensures (this.topOfStack >= 0)  ==>  (\result == this.theArray[this.topOfStack]);
    /**
     * Get the most recently inserted item in the stack.
     * Does not alter the stack.
     * @return the most recently inserted item in the stack, or null, if empty.
     * @observer
     */
    public Object top( )
    {
        if( isEmpty( ) )
            return null;
        return theArray[ topOfStack ];
    }

    //@ requires this.topOfStack >= 0;
    //@ modifies this.theArray[*], this.topOfStack;
    //@ ensures (\forall int i, j; (0 <= i && i <= this.topOfStack && 0 <= j && j <= \old(this.topOfStack)-1 && i == j) ==> ( this.theArray[i] == this.theArray[j] ))(\forall int i, j; (0 <= i && i <= this.topOfStack && 0 <= j && j <= \old(this.topOfStack-1) && i == j) ==> ( this.theArray[i] == \old(this.theArray[j]) ))(\forall int i, j; (0 <= i && i <= this.topOfStack && 0 <= j && j <= \old(this.topOfStack-1) && i == j) ==> ( this.theArray[i] == \old(this.theArray[j]) ));
    //@ ensures \old(this.topOfStack) == this.topOfStack + 1;
    /**
     * Remove the most recently inserted item from the stack.
     * @exception Underflow if stack is already empty.
     */
    public void pop( ) throws Underflow
    {
        if( isEmpty( ) )
            throw new Underflow( );
        theArray[ topOfStack-- ] = null;
    }

    //@ requires x != null;
    //@ modifies this.theArray[*], this.topOfStack;
    //@ ensures \old(x) == this.theArray[this.topOfStack];
    //@ ensures (\forall int i, j; (this.topOfStack+1 <= i && i <= this.theArray.length-1 && \old(this.topOfStack+2) <= j && j <= \old(this.theArray.length-1) && (i-(this.topOfStack+1)) == (j-(\old(this.topOfStack+2)))) ==> ( this.theArray[i] == \old(this.theArray[j]) ));
    //@ ensures (\forall int i, j; (0 <= i && i <= \old(this.topOfStack) && 0 <= j && j <= \old(this.topOfStack) && i == j) ==> ( this.theArray[i] == \old(this.theArray[j]) ));
    //@ ensures \old(this.topOfStack) == this.topOfStack - 1;
    /**
     * Insert a new item into the stack, if not already full.
     * @param x the item to insert.
     * @exception Overflow if stack is already full.
     */
    public void push( Object x ) throws Overflow
    {
        if( isFull( ) )
            throw new Overflow( );
        theArray[ ++topOfStack ] = x;
    }

    //@ modifies this.theArray[*], this.topOfStack;
    //@ ensures (\forall int i, j; (0 <= i && i <= this.topOfStack && 0 <= j && j <= this.topOfStack && i == j) ==> ( this.theArray[i] == \old(this.theArray[j]) ));
    //@ ensures (\forall int i, j; (\old(this.topOfStack)+1 <= i && i <= this.theArray.length-1 && \old(this.topOfStack+1) <= j && j <= \old(this.theArray.length-1) && (i-(\old(this.topOfStack)+1)) == (j-(\old(this.topOfStack+1)))) ==> ( this.theArray[i] == \old(this.theArray[j]) ));
    //@ ensures (\old(this.topOfStack) >= 0)  ==  (\result != null);
    //@ ensures (\old(this.topOfStack) >= 0)  ==>  (\old(this.topOfStack) == this.topOfStack + 1);
    //@ ensures (\old(this.topOfStack) >= 0)  ==>  (\result == \old(this.theArray[this.topOfStack]));
    //@ ensures this.topOfStack <= \old(this.topOfStack);
    /**
     * Return and remove most recently inserted item from the stack.
     * @return most recently inserted item, or null, if stack is empty.
     */
    public Object topAndPop( )
    {
        if( isEmpty( ) )
            return null;
        Object topItem = top( );
        theArray[ topOfStack-- ] = null;
        return topItem;
    }

    /*@ spec_public */ private Object [ ] theArray;
    /*@ spec_public */ private int        topOfStack;

}

Daikon homepage