Java Q&A
by Krishnan Rangaraajan


Listing One
/** 
     @inv (top >= 0 && top < max) 
*/
class MyStack {
        private Object[] elems;
        private int top, max;
    /**
        @pre (sz > 0)
        @post (max == sz && elems != null)
    */
    public MyStack(int sz) {
            max = sz;
            elems = new Object[sz];
    }
    /**
        @pre !isFull()
            @post (top == $prev (top) + 1) && elems[top-1] == obj
    */
    public void push(Object obj)  {
            elems[top++] = obj;
    }
    /**
        @pre !isEmpty()
            @post (top == $prev (top) - 1) && $ret == elems[top]
    */
    public Object pop()  {
            return elems[--top];
    }
    /**
        @post ($ret == (top == max))
    */
    public boolean isFull() {
            return top == max;
    }
    /**
        @post ($ret == (top == 0))
    */
    public boolean isEmpty() {
            return top == 0;
    }
} // End MyStack


Listing Two
/*  Trigger file for class #default.MyStack. Generated by JMSAssert on 
 * Monday, April 12, 1999. Any changes you make to this file will be 
 * overwritten if you regenerate this file.
 */
import macro;

// Postcondition for method - MyStack(int)
MyStackPost(meth, $obj, sz) {
    assertPost(($obj.max == sz && $obj.elems != null));
}
// Precondition for method - MyStack(int)
MyStackPre(meth, $obj, sz) {
    assertPre((sz > 0));
}
// Postcondition for method - void push(Object)
pushPost(meth, $obj, obj, $ret) {
    assertPost(($obj.top == 
              this.top$prev + 1) && $obj.elems[this.top$prev] == obj);
}
// Precondition for method - void push(Object)
pushPre(meth, $obj, obj) {
    this.top$prev = $obj.top;
    assertPre(!$obj.isFull());
}
// Postcondition for method - Object pop()
popPost(meth, $obj, $ret) {
    assertPost(($obj.top == this.top$prev - 1) && $ret == 
                                           $obj.elems[$obj.top]);
}
// Precondition for method - Object pop()
popPre(meth, $obj) {
    this.top$prev = $obj.top;
    assertPre(!$obj.isEmpty());
}
// Postcondition for method - boolean isFull()
isFullPost(meth, $obj, $ret) {
    assertPost(($ret == ($obj.top == $obj.max)));
}
// Postcondition for method - boolean isEmpty()
isEmptyPost(meth, $obj, $ret) {
    assertPost(($ret == ($obj.top == 0)));
}
MyStackinv(meth, $obj) {
    assertInv(($obj.top >= 0 && $obj.top <= $obj.max));
}
static {
    assertStrMyStack = {
        { "<init>(I)V", "POSTCONDITION", "MyStackPost" },
        { "<init>(I)V", "PRECONDITION", "MyStackPre" },
        { "push(Ljava/lang/Object;)V", "POSTCONDITION", "pushPost" },
        { "push(Ljava/lang/Object;)V", "PRECONDITION", "pushPre" },
        { "pop()Ljava/lang/Object;", "POSTCONDITION", "popPost" },
        { "pop()Ljava/lang/Object;", "PRECONDITION", "popPre" },
        { "isFull()Z", "POSTCONDITION", "isFullPost" },
        { "isEmpty()Z", "POSTCONDITION", "isEmptyPost" },
        { "", "INVARIANT", "MyStackinv" }
    };
    setClassTrigger("MyStack",     assertStrMyStack);
}
load() {}


Listing Three
//Startup trigger file - c:\ranga\jverify\Startup.jms
import macro;
load() {} 
static { 
   default_MyStack.load();
}


Listing Four
class StackTest {
    public static void main(String[] args) {
        MyStack s = new MyStack(2); // Can push at most two elements
            s.push(new Integer(1));
            s.push(new Integer(23));
            s.push(new Integer(0)); // Precondition violation here! 
    }
}





1