JML

org.jmlspecs.samples.jmlkluwer
Class PriorityQueue

java.lang.Object
  extended byorg.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
Constructor Detail

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());
Model Method Detail

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);
Method Detail

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;

JML

JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.