// @(#)$Id: PriorityQueueUser.jml-refined,v 1.2 2007/11/04 20:15:29 leavens 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;

//@ refine "PriorityQueueUser.java-refined";
//@ model import org.jmlspecs.models.*;

public interface PriorityQueueUser {

 /*@ public model instance JMLValueSet entries;
   @ public initially entries.isEmpty();
   @*/
 /*@ public instance invariant
   @      (\forall JMLType e; entries.has(e);
   @                           e instanceof QueueEntry);
   @ public instance invariant
   @   (\forall QueueEntry e1; entries.has(e1);
   @       (\forall QueueEntry e2;
   @         entries.has(e2) && !(e1.equals(e2));
   @           e2.obj != e1.obj
   @           && e2.timeStamp != e1.timeStamp ) );
   @*/
}