SE450: Examples [13/24]

Some examples:

/**
 * @invariant y >= 0
 */
public class Test {
    
    private int y;

    public static void main(String args[]) {
	Test t = new Test();
	t.run();
    }

    /**
     * a simple non static test function
     */
    void run() {
	try {
	    for(int i = 2; i > -9; i-=3) {
		this.command2(i);
	    }
	} catch (Error e) {
	    // don't want to do a try/catch, just here so we
	    // can show it works!
	    e.printStackTrace();
	}

	try {
	    this.command("hey");
	    this.command(null); // throws an IllegalArumentException
	} catch(Exception e) {
	    // don't need to catch this, it's a RuntimeException!
	    e.printStackTrace();
	}
    }

    /**
     * a command
     * @pre arg != null
     * @param arg a String arument
     */
    public void command(String arg) {
	if(arg == null) {
	    throw new IllegalArgumentException("arg can't be null");
	}
	System.out.println("arg set to " + arg);
	// a little extra (y didn't change, but run it anyway)
	assert(invariant() == true);
    }

    /**
     * another command
     * @post arg = arg@pre + 1
     * @param arg an int to increment
     */
    public void command2(int i) {
	int i_old = i;
	i++;
	y += i; // so we can test invariant
	System.out.println("i is " + i + ", y is " + y);
	// post condition
	assert(i == i_old + 1);
	// invariant
	assert(invariant() == true);
    }

    /**
     * an example of an invariant method
     * @return whether the class invariant has been violated
     */
    boolean invariant() {
	if(y < 0) {
	    return false;
	}
	return true;
    }

}

When run from the command line, the above prints

D:\>java -ea -classpath . Test
i is 3, y is 3
i is 0, y is 3
i is -3, y is 0
i is -6, y is -6
java.lang.AssertionError
        at Test.command2(Test.java:61)
        at Test.run(Test.java:19)
        at Test.main(Test.java:10)
arg set to hey
Exception in thread "main" java.lang.AssertionError
        at Test.command(Test.java:47)
        at Test.run(Test.java:28)
        at Test.main(Test.java:10)

Note that the AssertionError won't show up unless assertions are enabled. (java -ea)

/**
 * @invariant size() >= 0
 */
public interface Queue {
    // commands
    /**
     * @post size() == size()@pre + 1
     * @post elements().get( size() -1) == o
     */
    public void add( Object o );

    /**
     * @pre size() >= 1
     * @post size() == size()@pre - 1
     * @post forall int i in 0 .. size() -1 |
     *    elements().get(i) == 
     *       elements()@pre.get(i + 1)
     * 
     */
    public Object remove();
 
    /**
     * @post return == elements().size()
     */
    public int size();

    /**
     * @pre size() >= 1
     * @post @result == elements().get(0)
     */
    public Object head();

    /**
     * Check if queue is empty - derived query
     * 
     * @post @result == (size() == 0)
     */     
    public boolean isEmpty();

    public Vector elements();
}