// @(#) $Id: E_SLList.jml-refined,v 1.6 2005/12/24 21:20:31 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.

// Author:  Clyde Ruby

package org.jmlspecs.samples.list.list1;

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

  //@ public model int changeLog;       in theList;

  //@ public constraint changeLog >= \pre(changeLog);

  /*@  public normal_behavior
    @  {|
    @    assignable theList, cursor;
    @    ensures theList.isEmpty() && cursor == 0;
    @   also
    @    assignable changeLog;
    @    ensures changeLog == 0;
    @  |}
    @*/
  public E_SLList();

  // accessors
  // ---------

  /*@  public normal_behavior
    @   assignable \nothing;
    @   ensures \result == theList.int_length();
    @*/
  public /*@ pure @*/ int length();

  /*@  public normal_behavior
    @   assignable \nothing;
    @   ensures \result == theList.isEmpty();
    @*/
  public /*@ pure @*/ boolean isEmpty();

  // to allow multiple iterations over the same list
  // -----------------------------------------------

  /*@  public normal_behavior
    @    assignable \nothing;
    @    ensures \result.listPtr.theList.equals(this.theList)
    @        && \result.currIndex == 0;
    @*/
  public ListIterator createIterator();

  // methods for changing the list
  // -----------------------------

  /*@ also
    @  public normal_behavior
    @   requires !isOffFront() && !isOffEnd();
    @   assignable changeLog;
    @   ensures changeLog == \pre(changeLog) + 1;
    @*/
  public void removeEntry();

  /*@ also
    @  public normal_behavior
    @   requires newEntry != null && !isOffEnd();
    @   assignable changeLog;
    @   ensures changeLog == \pre(changeLog) + 1;
    @*/
  public void insertAfterCursor(Object newEntry);

  /*@ also
    @  public normal_behavior
    @   requires newEntry != null && !isOffFront();
    @   assignable changeLog;
    @   ensures changeLog >= \pre(changeLog) + 1;
    @*/
  public void insertBeforeCursor(Object newEntry);

  /*@ also
    @  public normal_behavior
    @   requires !isOffFront() && !isOffEnd() && newEntry != null;
    @   assignable changeLog;
    @   ensures changeLog == \pre(changeLog) + 1;
    @*/
  public void replaceEntry(Object newEntry);

  /*@  public normal_behavior
    @    requires newEntry != null;
    @    assignable theList, cursor;
    @    ensures theList.equals(\pre(theList).insertBack(newEntry))
    @             && cursor == theList.int_length() - 1;
    @ also
    @    requires newEntry != null;
    @    assignable changeLog;
    @    ensures changeLog >= \pre(changeLog) + 1;
    @*/
  public void append(Object newEntry);

  /*@  public normal_behavior
    @    assignable theList, cursor;
    @    ensures theList.isEmpty() && cursor == 0;
    @ also
    @  public normal_behavior
    @    assignable changeLog;
    @    ensures changeLog >= \pre(changeLog) + 1;
    @*/
  public void removeAllEntries();

  /*@ also
    @  public normal_behavior
    @    assignable \nothing;
    @    ensures \result instanceof E_SLList
    @            && ((E_SLList)\result).theList.equals(theList)
    @            && ((E_SLList)\result).cursor == 0
    @            && ((E_SLList)\result).changeLog == 0
    @            && \fresh(\result);
    @*/
  public /*@ non_null @*/ Object clone();
}