// @(#) $Id: OneWayNode.jml-refined,v 1.11 2005/12/09 04:20:15 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.

// Author:  Clyde Ruby

package org.jmlspecs.samples.list.node;

//@ model import org.jmlspecs.models.JMLObjectSequence;

public class OneWayNode { // Singly Linked Node

    // data members

    //@ public model JMLObjectSequence entries;
    /*@ public model JMLObjectSequence allButFirst;
      @                                in entries;
      @*/

    // 'allButFirst' is an abstraction so checking for a null 
    // 'nextNode' is not required (as often) in specifications. 

    /*@ public model nullable Object theEntry;
      @                     in entries;
      @*/
    /*@ public model nullable OneWayNode nextNode;
      @                         in entries, allButFirst;
      @*/

    // The maps-into clause above recursively includes the 
    // rest of the entries!

    //@ public invariant_redundantly entries != null && allButFirst != null;

  /*@  public normal_behavior
    @    assignable entries;
    @    ensures theEntry == null && entries.int_size() == 1
    @         && entries.itemAt(0) == null && allButFirst.isEmpty();
    @*/
    public OneWayNode();

  /*@  public normal_behavior
    @    assignable entries;
    @    ensures theEntry == ent && entries.int_size() == 1
    @       &&  entries.itemAt(0) == ent && allButFirst.isEmpty();
    @*/
    public OneWayNode(/*@ nullable @*/ Object ent);

  /*@  public normal_behavior
    @    assignable \nothing;
    @    ensures \result == theEntry;
    @*/
    public /*@ pure nullable @*/ Object getEntry();

  /*@  public normal_behavior
    @    assignable theEntry;
    @    ensures theEntry == newEntry 
    @       &&  entries.itemAt(0) == newEntry;
    @*/
    public void setEntry(/*@ nullable @*/ Object newEntry);

  /*@  public normal_behavior
    @    assignable \nothing;
    @    ensures \result == nextNode;
    @*/
    public /*@ pure nullable @*/ /* rep */ OneWayNode getNextNode();

  /*@  public normal_behavior
    @    assignable allButFirst;
    @    ensures allButFirst.equals(
    @               \old(allButFirst).insertFront(newEntry)); 
    @*/
    public void insertAfter(/*@ nullable @*/ Object newEntry);

  /*@  public normal_behavior
    @    requires ! allButFirst.isEmpty();
    @    assignable entries;
    @    ensures allButFirst.equals(\old(allButFirst).trailer());
    @  also
    @    requires allButFirst.isEmpty();
    @    assignable \nothing;
    @    ensures \not_modified(entries);
    @*/
    public void removeNextNode();

  /*@  public normal_behavior
    @    assignable \nothing;
    @    ensures \result == (nextNode != null);
    @*/
    public boolean hasNext();

  /*@ also
    @  public normal_behavior
    @    assignable \nothing;
    @    ensures \result instanceof OneWayNode 
    @         && ((OneWayNode)\result).entries.equals(entries);
    @*/
    public Object clone();
}