// @(#)$Id: PriorityQueue.java-refined,v 1.10 2007/11/13 11:48:41 chalin Exp $ // Copyright (C) 1998, 1999 Iowa State University // This file is part of JML // JML is free software; you can redistribute it and/or modify // it under the terms of the GNU General Public License as published by // the Free Software Foundation; either version 2, or (at your option) // any later version. // JML is distributed in the hope that it will be useful, // but WITHOUT ANY WARRANTY; without even the implied warranty of // MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the // GNU General Public License for more details. // You should have received a copy of the GNU General Public License // along with JML; see the file COPYING. If not, write to // the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA. 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(); }