// @(#) $Id: DLList.refines-jml,v 1.8 2006/01/04 02:09:35 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.list1;

//@ refine "DLList.java";

import org.jmlspecs.samples.list.list1.node.DLNode;

// FIXME: adapt this file to non-null-by-default and remove the following modifier.
/*@ nullable_by_default @*/ 
public class DLList extends E_SLList { // Doubly Linked List

  /*@ also
    @  protected code normal_behavior
    @    requires \same;
    @    accessible theListNode_, theListNode_.nextNode;
    @    callable  firstEntry(), new DLNode(Object),
    @              theListNode_.insertAfter(Object),
    @              theListNode_.getNextNode();
    @    captures \nothing;
    @*/
  public DLList();

// iteration methods
// -----------------
  /*@ also
    @  protected code normal_behavior
    @    requires \same;
    @    accessible theListNode_;
    @    callable theListNode_.getNextNode();
    @    captures \nothing;
    @*/
   public void firstEntry();

  /*@ also
    @  protected code normal_behavior
    @    requires \same;
    @    accessible cursorNode_, lastNode_;
    @    callable \nothing;
    @    captures \nothing;
    @*/
  public /*@ pure @*/ boolean isOffEnd();

  /*@ also
    @  protected code normal_behavior
    @    requires \same;
    @    accessible cursorNode_;
    @    callable isOffEnd(), theListNode_.getNextNode();
    @    captures \nothing;
    @*/
   public void incrementCursor();

  /*@ also
    @  protected code normal_behavior
    @    requires \same;
    @    accessible cursorNode_;
    @    callable isOffEnd(), cursorNode_.getEntry();
    @    captures \nothing;
    @*/
    /*@ non_null @*/ public Object getEntry();


// NEW iteration methods (for doubly linked list)
// ---------------------
  /*@ also
    @  protected code normal_behavior
    @    requires \same;
    @    accessible cursorNode_;
    @    callable isOffFront(), DLNode.getPrevNode();
    @    captures \nothing;
    @*/
   public void decrementCursor();

  /*@ also
    @  protected code normal_behavior
    @    requires \same;
    @    accessible lastNode_;
    @    callable decrementCursor();
    @    captures \nothing;
    @*/
   public void lastEntry();

  /*@ also
    @  protected code normal_behavior
    @    requires \same;
    @    accessible cursorNode_, length_;
    @    callable isOffEnd(), isOffFront(),
    @             DLNode.getPrevNode(),
    @             DLNode.removeNextNode();
    @    captures \nothing;
    @*/
   public void removeEntry();

  /*@ also
    @  protected code normal_behavior
    @    requires \same;
    @    accessible cursorNode_, length_;
    @    callable isOffEnd(), incrementCursor(),
    @             insertBeforeCursor(Object);
    @    captures newEntry;
    @*/
   public void insertAfterCursor(Object newEntry);

  /*@ also
    @  protected code normal_behavior
    @    requires \same;
    @    accessible length_, log_;
    @    callable isOffEnd(), incrementCursor(),
    @             DLNode.insertBefore(Object);
    @    captures newEntry;
    @*/
   public void insertBeforeCursor(Object newEntry);

  /*@ also
    @  protected code normal_behavior
    @    requires \same;
    @    accessible theList;
    @    callable new DLList(DLNode , int );
    @    captures theListNode_.entries;
    @*/
   public /*@ non_null @*/ Object clone();

// ***********************************************************
// protected methods

  /*@ also
    @  protected code normal_behavior
    @    requires \same;
    @    accessible othLst.theList;
    @    callable firstEntry();
    @    captures othLst.theList;
    @*/
   protected DLList(DLList othLst);

  /*@ also
    @  protected code normal_behavior
    @    requires \same;
    @    accessible length_, log_, listNode.entries;
    @    callable DLNode.getNextNode(), firstEntry();
    @    captures listNode;
    @*/
   protected DLList(DLNode listNode, int len);
}