org.jmlspecs.samples.stacks
Interface BoundedStackInterface

All Superinterfaces:

BoundedThing

All Known Implementing Classes:

BoundedStack

@Model(value="public instance JMLObjectSequence theStack; in size;")
@Initially(header="public",
           value=" theStack != null && theStack.isEmpty();")
@Represents(header="public instance",
            value="size <- theStack.int_length();")
@InvariantDefinitions(value={@Invariant(header="public instance",value="theStack != null;"),@Invariant(header="public instance",redundantly=true,value="theStack.int_length() <= MAX_SIZE;"),@Invariant(header="public instance",value="(#forall int i; 0 <= i && i < theStack.int_length();theStack.itemAt(i) != null);")})
public interface BoundedStackInterface
extends BoundedThing

Method Summary

void	pop()
void	push(java.lang.Object x)
java.lang.Object	top()

Methods inherited from interface org.jmlspecs.samples.stacks.BoundedThing

clone, getSizeLimit, isEmpty, isFull

Method Detail

pop

@Also(value={@SpecCase(header="public normal_behavior",requires="!theStack.isEmpty();",assignable="size, theStack;",ensures="theStack.equals(#old(theStack.trailer()));"),@SpecCase(header="public exceptional_behavior",requires="theStack.isEmpty();",assignable="#nothing;",signalsOnly="BoundedStackException;")})
void pop()
         throws BoundedStackException

Throws:

BoundedStackException

push

@Also(value={@SpecCase(header="public normal_behavior",requires="theStack.int_length() < MAX_SIZE && x != null;",assignable="size, theStack;",ensures="theStack.equals(#old(theStack.insertFront(x)));",ensuresRedundantly="theStack != null && top() == x&& theStack.int_length()== #old(theStack.int_length()+1);"),@SpecCase(header="public exceptional_behavior",requires="theStack.int_length() >= MAX_SIZE || x == null;",assignable="#nothing;",signalsOnly="BoundedStackException, NullPointerException;",signals="(Exception e)((e instanceof BoundedStackException) ==> theStack.int_length() == MAX_SIZE)&& ((e instanceof NullPointerException) ==> x == null));")})
void push(java.lang.Object x)
          throws BoundedStackException,
                 java.lang.NullPointerException

Throws:

BoundedStackException

java.lang.NullPointerException

top

@Also(value={@SpecCase(header="public normal_behavior",requires="!theStack.isEmpty();",ensures="#result == theStack.first() && #result != null;"),@SpecCase(header="public exceptional_behavior",requires="theStack.isEmpty();",signalsOnly="BoundedStackException;",signals="(BoundedStackException e)#fresh(e) && e != null && e.getMessage() != null&& e.getMessage().equals(\"empty stack\");")})
java.lang.Object top()
                     throws BoundedStackException

Throws:

BoundedStackException