org.jmlspecs.samples.stacks
Interface BoundedStackInterface

All Superinterfaces:

BoundedThing

All Known Implementing Classes:

BoundedStack, BoundedStackImplementation

public interface BoundedStackInterface

extends BoundedThing

Class Specifications

instance public invariant this.theStack != null; instance public invariant_redundantly this.theStack.int_length() <= this.MAX_SIZE; instance public invariant ( \forall int i; 0 <= i&&i < this.theStack.int_length(); this.theStack.itemAt(i) != null); instance public represents size <- this.theStack.int_length(); public initially this.theStack != null&&this.theStack.isEmpty();

Specifications inherited from class Object

represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT; public represents _getClass <- \typeof(this);

Specifications inherited from interface BoundedThing

instance public invariant this.MAX_SIZE > 0; instance public invariant 0 <= this.size&&this.size <= this.MAX_SIZE; instance public constraint this.MAX_SIZE == \old(this.MAX_SIZE);

Model Field Summary
[instance]  JMLObjectSequence	theStack

 

Model fields inherited from interface org.jmlspecs.samples.stacks.BoundedThing

MAX_SIZE, size

 

Method Summary
void	pop()
void	push(Object x)
Object	top()

 

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

clone, getSizeLimit, isEmpty, isFull

 

Model Field Detail

theStack

public JMLObjectSequence theStack

Specifications: instance
is in groups: size
datagroup contains: org.jmlspecs.samples.stacks.BoundedStack.theItems theItems[*] org.jmlspecs.samples.stacks.BoundedStack.nextFree theItems[*] org.jmlspecs.samples.stacks.BoundedStackImplementation.nextFree

pop

public void pop()
                  throws BoundedStackException

Throws:

BoundedStackException

Specifications:

public normal_behavior
requires !this.theStack.isEmpty();
assignable size, theStack;
ensures this.theStack.equals(\old(this.theStack.trailer()));

     also

public exceptional_behavior
requires this.theStack.isEmpty();
assignable \nothing;
signals_only org.jmlspecs.samples.stacks.BoundedStackException;

    implies_that

public behavior
requires !this.theStack.isEmpty();
assignable size, theStack;
ensures this.theStack.equals(\old(this.theStack.trailer()));
signals (java.lang.Exception) false;

     also

public behavior
requires this.theStack.isEmpty();
assignable \nothing;
ensures false;
signals_only org.jmlspecs.samples.stacks.BoundedStackException;
signals (java.lang.Exception) true;

     also

public behavior
requires !this.theStack.isEmpty()||this.theStack.isEmpty();
assignable size, theStack;
ensures \old(!this.theStack.isEmpty()) ==> this.theStack.equals(\old(this.theStack.trailer()));
ensures \old(this.theStack.isEmpty()) ==> \not_assigned(size)&&\not_assigned(theStack);
signals_only org.jmlspecs.samples.stacks.BoundedStackException;
signals (java.lang.Exception) \old(!this.theStack.isEmpty()) ==> false;
signals (java.lang.Exception) \old(this.theStack.isEmpty()) ==> \not_assigned(size)&&\not_assigned(theStack);

push

public void push(Object x)
                   throws BoundedStackException,
                          NullPointerException

Throws:

BoundedStackException

NullPointerException

Specifications:

public normal_behavior
requires this.theStack.int_length() < this.MAX_SIZE&&x != null;
assignable size, theStack;
ensures this.theStack.equals(\old(this.theStack.insertFront(x)));
ensures_redundantly this.theStack != null&&this.top() == x&&this.theStack.int_length() == \old(this.theStack.int_length()+1);

     also

public exceptional_behavior
requires this.theStack.int_length() >= this.MAX_SIZE||x == null;
assignable \nothing;
signals_only org.jmlspecs.samples.stacks.BoundedStackException, java.lang.NullPointerException;
signals (org.jmlspecs.samples.stacks.BoundedStackException) this.theStack.int_length() == this.MAX_SIZE;
signals (java.lang.NullPointerException) x == null;

top

public Object top()
                    throws BoundedStackException

Throws:

BoundedStackException

Specifications: pure

public normal_behavior
requires !this.theStack.isEmpty();
ensures \result == this.theStack.first()&&\result != null;

     also

public exceptional_behavior
requires this.theStack.isEmpty();
signals_only org.jmlspecs.samples.stacks.BoundedStackException;
signals (org.jmlspecs.samples.stacks.BoundedStackException e) \fresh(e)&&e != null&&e.getMessage() != null&&e.getMessage().equals("empty stack");