org.jmlspecs.samples.jmlkluwer
Interface PriorityQueueUser

All Known Implementing Classes:

PriorityQueue

public interface PriorityQueueUser

Class Specifications

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();

Specifications inherited from class Object

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

Model Field Summary
[instance]  JMLValueSet	entries

 

Method Summary
boolean	contains(Object argObj)
boolean	isEmpty()
Object	next()
void	remove(Object argObj)

 

Model Field Detail

entries

public JMLValueSet entries

Specifications: instance
datagroup contains: org.jmlspecs.samples.jmlkluwer.PriorityQueue.levels levels.theCollection org.jmlspecs.samples.jmlkluwer.PriorityQueue.nextTS

contains

public boolean contains(Object argObj)

Specifications: 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

Throws:

PQException

Specifications: 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)

Specifications:

     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()

Specifications: pure

     also

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