# Sample output from Daikon dynamic invariant detector

This is a simple example of Daikon's output. 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