3. Class Specifications

The file `PriorityQueue.java-refined' shown below specifies PriorityQueue, a class that implements the interface PriorityQueueUser. Because this class implements an interface, it inherits specifications, and hence implementation obligations, from that interface. The specification given thus adds more obligations to those given in previous specifications.

package org.jmlspecs.samples.jmlkluwer; //@ model import org.jmlspecs.models.*; public class PriorityQueue implements PriorityQueueUser { /*@ public normal_behavior @ assignable entries; @ ensures entries != null && entries.isEmpty(); @ ensures_redundantly @ entries.equals(new JMLValueSet()); @*/ public PriorityQueue(); //@ private pure model JMLValueSet abstractValue(); /*@ public normal_behavior @ requires entries.isEmpty(); @ assignable \nothing; @ ensures \result == -1; @ also @ public normal_behavior @ requires !(entries.isEmpty()); @ assignable \nothing; @ ensures (\forall QueueEntry e; entries.has(e); @ \result >= e.timeStamp); @ ensures (\exists QueueEntry e; entries.has(e); @ \result == e.timeStamp); @ public pure model long largestTimeStamp() { // FIXME: once model fields become usable within model methods // then delete the following local declaration JMLValueSet entries = abstractValue(); if(entries.isEmpty()) return -1; long max = Long.MIN_VALUE; JMLValueSetEnumerator i = null; for(i = entries.elements(); i.hasMoreElements(); ) { QueueEntry e = (QueueEntry)i.nextElement(); if (max < e.timeStamp) max = e.timeStamp; } return max; } @*/ /*@ public normal_behavior @ old long lts = largestTimeStamp(); @ requires !contains(argObj); @ requires argPriorityLevel >= 0; @ requires largestTimeStamp() < Long.MAX_VALUE; @ assignable entries; @ ensures entries.equals(\old(entries).insert( @ new QueueEntry(argObj, argPriorityLevel, lts+1))); @ also @ public exceptional_behavior @ requires contains(argObj) || argPriorityLevel < 0; @ assignable \nothing; @ signals_only PQException; @*/ public void addEntry(Object argObj, int argPriorityLevel) throws PQException; public /*@ pure @*/ boolean contains(Object argObj); public /*@ pure @*/ Object next() throws PQException; public void remove(Object argObj); public /*@ pure @*/ boolean isEmpty(); }

The pure model method largestTimeStamp is specified purely to help make the statement of addEntry more comprehensible. Since it is a model method, it does not need to be implemented. Without this specification, one would need to use the quantifier found in the second case of largestTimeStamp within the specification of addEntry.

The interesting method in PriorityQueue is addEntry. One important issue is how the timestamps are handled; this is hopefully clarified by the use of largestTimeStamp() in the postcondition of the first specification case.

A more subtle issue concerns finiteness. Since the precondition of addEntry's first case does not limit the number of entries that can be added, the specification seems to imply that the implementation must provide a literally unbounded priority queue, which is surely impossible. We avoid this problem, by following Poetzsch-Heffter [Poetzsch-Heffter97] in releasing implementations from their obligations to fulfill specification case's postcondition when Java runs out of storage. That is, a method implementation correctly implements a specification case if, whenever the method is called in a state that satisfies the precondition of that specification case, either

• the method terminates in a state that satisfies the postcondition of that specification case, having assigned only the locations permitted by its assignable clause, or

• Java signals an error, by throwing an exception that inherits from java.lang.Error.