org.jmlspecs.samples.jmlkluwer
Class PriorityQueue

java.lang.Object
  org.jmlspecs.samples.jmlkluwer.PriorityQueue

All Implemented Interfaces:

PriorityQueueUser

public class PriorityQueue

extends Object

implements PriorityQueueUser

Class Specifications

private invariant ( \forall int i; 0 <= i&&i < this.levels.size(); this.levels.get(i) instanceof java.util.ArrayList&&!((java.util.ArrayList)this.levels.get(i)).isEmpty()&&( \forall int j; 0 <= j&&j < ((java.util.ArrayList)this.levels.get(i)).size(); ((java.util.ArrayList)this.levels.get(i)).get(j) instanceof org.jmlspecs.samples.jmlkluwer.QueueEntry&&((org.jmlspecs.samples.jmlkluwer.QueueEntry)((java.util.ArrayList)this.levels.get(i)).get(j)).getLevel() == ((org.jmlspecs.samples.jmlkluwer.QueueEntry)((java.util.ArrayList)this.levels.get(i)).get(0)).getLevel())&&( \forall int k; 0 <= k&&k < i; this.getLevelOf(this.levels.get(k)) < this.getLevelOf(this.levels.get(i)))); public invariant_redundantly -1 <= this.largestTimeStamp(); private invariant this.nextTS == this.largestTimeStamp()+1; private invariant_redundantly 0 <= this.nextTS; private represents entries <- this.abstractValue();

Specifications inherited from class Object

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

Specifications inherited from interface PriorityQueueUser

instance public invariant ( \forall org.jmlspecs.models.JMLType e; this.entries.has(e); e instanceof org.jmlspecs.samples.jmlkluwer.QueueEntry); instance public invariant ( \forall org.jmlspecs.samples.jmlkluwer.QueueEntry e1; this.entries.has(e1); ( \forall org.jmlspecs.samples.jmlkluwer.QueueEntry e2; this.entries.has(e2)&&!(e1.equals(e2)); e2.obj != e1.obj&&e2.timeStamp != e1.timeStamp)); public initially this.entries.isEmpty();

Model Field Summary

 

Model fields inherited from class java.lang.Object

_getClass, objectState, theString

 

Model fields inherited from interface org.jmlspecs.samples.jmlkluwer.PriorityQueueUser

entries

 

Ghost Field Summary

 

Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

 

Field Summary
private  ArrayList	levels
private  long	nextTS

 

Constructor Summary

PriorityQueue()

 

Model Method Summary
private  JMLValueSet	abstractValue()
long	largestTimeStamp()

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
void	addEntry(Object argObj, int argPriorityLevel)
boolean	contains(Object argObj)
private  ArrayList	getLevelList(int argPriorityLevel)
private  int	getLevelOf(Object levelList)
private  int	getLevelOf(ArrayList levelList)
boolean	isEmpty()
Object	next()
void	remove(Object argObj)
String	toString()

 

Methods inherited from class java.lang.Object

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

 

Field Detail

levels

private ArrayList levels

Specifications: non_null
is in groups: entries
maps levels.theCollection \into entries

nextTS

private long nextTS

Specifications:
is in groups: entries

PriorityQueue

public PriorityQueue()

Specifications:

public normal_behavior
assignable entries;
ensures this.entries != null&&this.entries.isEmpty();
ensures_redundantly this.entries.equals(new org.jmlspecs.models.JMLValueSet());

abstractValue

private JMLValueSet abstractValue()

Specifications: pure

largestTimeStamp

public long largestTimeStamp()

Specifications: pure

public normal_behavior
requires this.entries.isEmpty();
assignable \nothing;
ensures \result == -1;

     also

public normal_behavior
requires !(this.entries.isEmpty());
assignable \nothing;
ensures ( \forall org.jmlspecs.samples.jmlkluwer.QueueEntry e; this.entries.has(e); \result >= e.timeStamp);
ensures ( \exists org.jmlspecs.samples.jmlkluwer.QueueEntry e; this.entries.has(e); \result == e.timeStamp);

addEntry

public void addEntry(Object argObj,
                     int argPriorityLevel)
              throws PQException

Throws:

PQException

Specifications:

public normal_behavior
old long lts = this.largestTimeStamp();
requires !this.contains(argObj);
requires argPriorityLevel >= 0;
requires this.largestTimeStamp() < 9223372036854775807;
assignable entries;
ensures this.entries.equals(\old(this.entries).insert(new org.jmlspecs.samples.jmlkluwer.QueueEntry(argObj, argPriorityLevel, lts+1)));

     also

public exceptional_behavior
requires this.contains(argObj)||argPriorityLevel < 0;
assignable \nothing;
signals_only org.jmlspecs.samples.jmlkluwer.PQException;

getLevelList

private ArrayList getLevelList(int argPriorityLevel)

Specifications: helper

private normal_behavior
requires ( \exists int i; 0 <= i&&i < this.levels.size(); this.levels.get(i) != null&&((org.jmlspecs.samples.jmlkluwer.QueueEntry)((java.util.ArrayList)this.levels.get(i)).get(0)).priorityLevel == argPriorityLevel);
assignable \nothing;
ensures this.levels.theCollection.has(\result );

     also

private normal_behavior
requires !( \exists int i; 0 <= i&&i < this.levels.size(); this.levels.get(i) != null&&((org.jmlspecs.samples.jmlkluwer.QueueEntry)((java.util.ArrayList)this.levels.get(i)).get(0)).priorityLevel == argPriorityLevel);
assignable levels.theCollection;
ensures \fresh(\result )&&this.levels.theList.has(\result );
ensures ( \forall int i; 0 <= i&&i < this.levels.size(); this.levels.get(i) == \result ||(\old(this.levels.theList).has(this.levels.get(i))&&(\old(this.levels.theList).get(i).equals(this.levels.get(i))||\old(this.levels.theList).get(i-1).equals(this.levels.get(i)))));

getLevelOf

private int getLevelOf(ArrayList levelList)

Specifications: pure helper

requires levelList != null&&!levelList.isEmpty();
assignable \nothing;

getLevelOf

private int getLevelOf(Object levelList)

Specifications: pure helper

requires levelList instanceof java.util.ArrayList;
requires !((java.util.ArrayList)levelList).isEmpty();
assignable \nothing;

contains

public boolean contains(Object argObj)

Specified by:

contains in interface PriorityQueueUser

Specifications: pure

Specifications inherited from overridden method contains(Object argObj) in interface PriorityQueueUser:
       pure

     also

public normal_behavior
ensures \result <==> ( \exists org.jmlspecs.samples.jmlkluwer.QueueEntry e; this.entries.has(e); e.obj == argObj);

next

public Object next()
            throws PQException

Specified by:

next in interface PriorityQueueUser

Throws:

PQException

Specifications: pure

Specifications inherited from overridden method in interface PriorityQueueUser:
       pure

     also

public normal_behavior
requires !this.entries.isEmpty();
ensures ( \exists org.jmlspecs.samples.jmlkluwer.QueueEntry r; this.entries.has(r)&&\result == r.obj; ( \forall org.jmlspecs.samples.jmlkluwer.QueueEntry o; this.entries.has(o)&&!(r.equals(o)); r.priorityLevel >= o.priorityLevel&&(r.priorityLevel == o.priorityLevel ==> r.timeStamp < o.timeStamp)));

     also

public exceptional_behavior
requires this.entries.isEmpty();
signals_only org.jmlspecs.samples.jmlkluwer.PQException;

remove

public void remove(Object argObj)

Specified by:

remove in interface PriorityQueueUser

Specifications inherited from overridden method remove(Object argObj) in interface PriorityQueueUser:

     also

public normal_behavior
requires this.contains(argObj);
assignable entries;
ensures ( \exists org.jmlspecs.samples.jmlkluwer.QueueEntry e; \old(this.entries.has(e))&&e.obj == argObj; this.entries.equals(\old(this.entries.remove(e))));

     also

public normal_behavior
requires !this.contains(argObj);
assignable \nothing;
ensures \not_modified(entries);

isEmpty

public boolean isEmpty()

Specified by:

isEmpty in interface PriorityQueueUser

Specifications: pure

Specifications inherited from overridden method in interface PriorityQueueUser:
       pure

     also

public normal_behavior
ensures \result <==> this.entries.isEmpty();

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;