java.util
Class Stack

java.lang.Object
  java.util.AbstractCollection
      java.util.AbstractList
          java.util.Vector
              java.util.Stack

All Implemented Interfaces:

Cloneable, Collection, List, RandomAccess, Serializable

public class Stack

extends Vector

JML's specification of Stack.

Version:

$Revision: 1.13 $

Author:

Kristina Boysen, Gary T. Leavens

Class Specifications

Specifications inherited from class Vector

public invariant this.maxCapacity >= 0&&this.capIncrement >= 0&&this.theList.int_size() <= this.maxCapacity; public invariant 0 <= this.elementCount; public invariant this.elementCount == this.size(); public constraint this.capIncrement == \old(this.capIncrement); protected represents theList <- org.jmlspecs.models.JMLEqualsSequence.convertFrom(this.elementData,this.elementCount); public represents maxCapacity <- this.capacity(); protected represents capIncrement <- this.capacityIncrement;

Specifications inherited from class AbstractList

protected initially this.modCount == 0;

Specifications inherited from class Object

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

Specifications inherited from interface List

instance public represents theCollection <- this.theList.toBag();

Specifications inherited from interface Collection

instance public invariant this.elementType == this.theCollection.elementType; instance public invariant this.containsNull == this.theCollection.containsNull; instance public invariant !this.nullElementsSupported ==> !this.containsNull;

Model Field Summary

 

Model fields inherited from class java.util.Vector

capIncrement, maxCapacity

 

Model fields inherited from class java.lang.Object

_getClass, objectState, theString

 

Model fields inherited from interface java.util.List

theList

 

Model fields inherited from interface java.util.Collection

addOperationSupported, elementState, nullElementsSupported, removeOperationSupported, theCollection

 

Ghost Field Summary

 

Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

 

Ghost fields inherited from interface java.util.Collection

containsNull, elementType

 

Field Summary

 

Fields inherited from class java.util.Vector

capacityIncrement, elementCount, elementData

 

Fields inherited from class java.util.AbstractList

modCount

 

Constructor Summary

Stack()

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Model methods inherited from interface java.util.Collection

hashValue

 

Method Summary
boolean	empty()
Object	peek()
Object	pop()
Object	push(Object item)
int	search(Object o)

 

Methods inherited from class java.util.Vector

add, add, addAll, addAll, addElement, capacity, clear, clone, contains, containsAll, copyInto, elementAt, elements, ensureCapacity, equals, firstElement, get, hashCode, indexOf, indexOf, insertElementAt, isEmpty, lastElement, lastIndexOf, lastIndexOf, remove, remove, removeAll, removeAllElements, removeElement, removeElementAt, removeRange, retainAll, set, setElementAt, setSize, size, subList, toArray, toArray, toString, trimToSize

 

Methods inherited from class java.util.AbstractList

iterator, listIterator, listIterator

 

Methods inherited from class java.lang.Object

finalize, getClass, notify, notifyAll, wait, wait, wait

 

Methods inherited from interface java.util.List

iterator, listIterator, listIterator

 

Constructor Detail

Stack

public Stack()

Specifications:

public normal_behavior
assignable theCollection, maxCapacity, capIncrement, elementType, containsNull;
ensures this.theList.isEmpty();
ensures this.elementType == \type(java.lang.Object)&&!this.containsNull;
ensures this.maxCapacity > 0&&this.capIncrement >= 0;

    implies_that

ensures this.elementCount == 0;
ensures this.elementType == \type(java.lang.Object);

push

public Object push(Object item)

Specifications:

public model_program { ... }

     also

public normal_behavior
requires \typeof(item) <: this.elementType;
requires this.containsNull||item != null;
assignable theCollection;
ensures this.theList.equals(\old(this.theList).insertBack(item));
ensures this.theList.int_size() <= this.maxCapacity;

     also

public normal_behavior
requires \typeof(this) == \type(java.util.Vector);

{|

requires this.theList.int_size() < this.maxCapacity;
ensures \not_modified(maxCapacity)&&\not_modified(capIncrement);

also

requires this.theList.int_size() == this.maxCapacity;

{|

requires 0 < this.capIncrement&&this.maxCapacity <= 2147483647-this.capIncrement;
assignable maxCapacity, theList;
ensures this.maxCapacity == \old(this.maxCapacity)+this.capIncrement;

also

requires this.capIncrement == 0&&this.maxCapacity == 0;
assignable maxCapacity, theList;
ensures this.maxCapacity == 1;

also

requires this.capIncrement == 0&&this.maxCapacity > 0&&this.maxCapacity < 1073741823;
assignable maxCapacity, theList;
ensures this.maxCapacity == \old(this.maxCapacity)*2;

|}

|}

     also

requires \typeof(item) <: this.elementType;
requires this.containsNull||item != null;
assignable elementCount;
ensures this.elementCount == \old(this.elementCount)+1;

pop

public Object pop()

Specifications:

public model_program { ... }

    implies_that

public normal_behavior
requires !this.theList.isEmpty();
assignable theCollection;
ensures \result == \old(this.theList.last())&&this.theList.equals(\old(this.theList).header());
ensures_redundantly this.theList.int_size() == \old(this.theList.int_size()-1);

     also

assignable elementCount;
ensures !this.containsNull ==> \result != null;
ensures this.elementCount == \old(this.elementCount)+1;

peek

public Object peek()

Specifications: pure

public model_program { ... }

    implies_that

public normal_behavior
requires !this.theList.isEmpty();
assignable \nothing;
ensures \result == \old(this.theList.last());

     also

ensures !this.containsNull ==> \result != null;

empty

public boolean empty()

Specifications: pure

public model_program { ... }

    implies_that

public normal_behavior
assignable \nothing;
ensures \result == this.theList.isEmpty();
ensures_redundantly \result <==> this.size() == 0;

search

public int search(Object o)

Specifications: pure

public model_program { ... }

    implies_that

public normal_behavior

{|

requires this.contains(o);
assignable \nothing;
ensures (this.theList.itemAt(\result ) == o||this.theList.itemAt(\result ).equals(o))&&!this.theList.removePrefix((int)(\result +1)).has(o);
ensures_redundantly (* \result is the index of the last occurrence of obj in theList *);

also

requires !this.contains(o);
assignable \nothing;
ensures \result == -1;

|}