org.jmlspecs.samples.stacks
Class UnboundedStackAsArrayList

java.lang.Object
  org.jmlspecs.samples.stacks.UnboundedStack
      org.jmlspecs.samples.stacks.UnboundedStackAsArrayList

public class UnboundedStackAsArrayList

extends UnboundedStack

Class Specifications

protected invariant this.elems != null; protected represents theStack <- this.abstractValue(); protected represents_redundantly theStack \such_that ( \forall int i; 0 <= i&&i < this.elems.size(); this.elems.get(i) == this.theStack.itemAt(i));

Specifications inherited from class UnboundedStack

public invariant this.theStack != null; 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);

Model Field Summary

 

Model fields inherited from class org.jmlspecs.samples.stacks.UnboundedStack

theStack

 

Model fields inherited from class java.lang.Object

_getClass, objectState, theString

 

Ghost Field Summary

 

Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

 

Field Summary
protected  ArrayList	elems

 

Constructor Summary

UnboundedStackAsArrayList()

 

Model Method Summary
protected  JMLObjectSequence	abstractValue()

 

Model methods inherited from class java.lang.Object

hashValue

 

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

 

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

 

Field Detail

elems

protected ArrayList elems

Specifications:
is in groups: theStack
maps elems.theList \into theStack

UnboundedStackAsArrayList

public UnboundedStackAsArrayList()

Specifications:

public normal_behavior
assignable theStack;
ensures this.theStack.isEmpty();

abstractValue

protected JMLObjectSequence abstractValue()

Specifications: pure

pop

public void pop()

Specifications:

     also

protected normal_behavior
requires !this.theStack.isEmpty();
assignable theStack;
ensures \not_modified(elems);

Specifications inherited from overridden method in class UnboundedStack:

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

push

public void push(Object x)

Specifications:

     also

protected normal_behavior
assignable theStack;
ensures \not_modified(elems);

Specifications inherited from overridden method push(Object x) in class UnboundedStack:

public normal_behavior
assignable theStack;
ensures this.theStack.equals(\old(this.theStack.insertFront(x)));

top

public Object top()

Specifications: (inherited)pure

Specifications inherited from overridden method in class UnboundedStack:
       pure

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

toString

public String toString()

Overrides:

toString in class Object

Specifications inherited from overridden method in class Object:
       non_null

public normal_behavior
assignable objectState;
ensures \result != null&&\result .equals(this.theString);
ensures (* \result is a string representation of this object *);

     also

public code normal_behavior
assignable \nothing;
ensures \result != null&&(* \result is the instance's class name, followed by an @, followed by the instance's hashcode in hex *);

     also

public code model_program { ... }

    implies_that

assignable objectState;
ensures \result != null;