// @(#)$Id: QueueEntry.jml-refined,v 1.3 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;

import org.jmlspecs.models.JMLType;

public /*@ pure @*/ class QueueEntry implements JMLType {

    //@ public model Object obj;
    //@ public model int    priorityLevel;
    //@ public model long   timeStamp;

    /*@ public invariant 
      @           priorityLevel >= 0 && timeStamp >= 0;
      @*/

    /*@ public normal_behavior
      @   requires argLevel >= 0 && argTimeStamp >= 0;
      @   assignable obj, priorityLevel, timeStamp;
      @   ensures obj == argObj && priorityLevel == argLevel
      @       && timeStamp == argTimeStamp;
      @*/
    public QueueEntry(Object argObj, int argLevel,
                      long argTimeStamp);

    /*@ also
      @  public normal_behavior
      @    ensures \result instanceof QueueEntry;
      @    ensures_redundantly this.equals(\result);
      @*/
    public Object clone();

    /*@ also
      @  public normal_behavior
      @    old QueueEntry oldo = (QueueEntry)o;
      @    requires o instanceof QueueEntry;
      @    ensures \result <==>
      @        oldo.obj == obj
      @     && oldo.priorityLevel == priorityLevel
      @     && oldo.timeStamp == timeStamp;
      @ also
      @  public normal_behavior
      @    requires !(o instanceof QueueEntry);
      @    ensures \result == false;
      @*/
    public boolean equals(/*@ nullable @*/ Object o);

    //@ ensures \result == priorityLevel;
    public int getLevel();

    //@ ensures \result == obj;
    public Object getObj();
}