org.jmlspecs.samples.stacks
Class BoundedStack

java.lang.Object
  org.jmlspecs.samples.stacks.BoundedStack

All Implemented Interfaces:

BoundedStackInterface, BoundedThing

@RepresentsDefinitions(value={@Represents(header="private",value="MAX_SIZE <- maxSize;"),@Represents(header="protected",value="theStack <- theStackRep;"),@Represents(header="protected",redundantly=true,value="theStack #such_that theStack != null&& theStack.int_length() == nextFree&& (#forall int i; 0 <= i && i < nextFree;        theStack.itemAt(i) == theItems[i]);")})
@InvariantDefinitions(value={@Invariant(header="protected",value="0 <= nextFree && nextFree <= theItems.length;"),@Invariant(header="protected",value="theItems != null;"),@Invariant(header="protected",value="(#forall int i; 0 <= i && i < nextFree;theItems[i] != null);")})
@ModelMethod(value="protected pure model JMLObjectSequence theStackRep() {   JMLObjectSequence ret = new JMLObjectSequence();   int i;   for (i = 0; i < nextFree; i++) {      ret = ret.insertFront(theItems[i]);   }   return ret;}")
public class BoundedStack
extends java.lang.Object
implements BoundedStackInterface

Constructor Summary

BoundedStack()

BoundedStack(int maxSize)

Method Summary

java.lang.Object	clone()
int	getSizeLimit()
boolean	isEmpty()
boolean	isFull()
void	pop()
void	push(java.lang.Object x)
java.lang.Object	top()
java.lang.String	toString()

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, wait, wait, wait

Constructor Detail

BoundedStack

@SpecCase(header="public normal_behavior",
          assignable="MAX_SIZE, size, theStack;",
          ensures="theStack.equals(new JMLObjectSequence());",
          ensuresRedundantly="theStack.isEmpty() && size == 0;")
public BoundedStack()

BoundedStack

@SpecCase(header="public normal_behavior",
          assignable="MAX_SIZE, size, theStack;",
          ensures="theStack.equals(new JMLObjectSequence());",
          ensuresRedundantly="theStack.isEmpty() && size == 0&& MAX_SIZE == maxSize;")
public BoundedStack(int maxSize)

Method Detail

clone

public java.lang.Object clone()

Specified by:

clone in interface BoundedThing

Overrides:

clone in class java.lang.Object

getSizeLimit

public int getSizeLimit()

Specified by:

getSizeLimit in interface BoundedThing

isEmpty

public boolean isEmpty()

Specified by:

isEmpty in interface BoundedThing

isFull

public boolean isFull()

Specified by:

isFull in interface BoundedThing

pop

public void pop()
         throws BoundedStackException

Specified by:

pop in interface BoundedStackInterface

Throws:

BoundedStackException

push

public void push(java.lang.Object x)
          throws BoundedStackException

Specified by:

push in interface BoundedStackInterface

Throws:

BoundedStackException

top

public java.lang.Object top()
                     throws BoundedStackException

Specified by:

top in interface BoundedStackInterface

Throws:

BoundedStackException

toString

@Also(value=@SpecCase(header="public normal_behavior",assignable="#nothing;",ensures="#result != null&& (* a string encoding of this is returned *);"))
public java.lang.String toString()

Overrides:

toString in class java.lang.Object