(****
 *
 * A new, improved list class.  It's much like the current one, with just some
 * clean up here and there.  Major changes are getting rid of Put and Pull ops,
 * replacing them with Append, Prepend, Enqueue, and Dequeue.  Also, the Enum
 * op has been removed and a new ListIterator object defined, to allow multiple
 * simultaneous enumerations to be created for a single list.  It is suggested
 * that the C++ implementation be template-based instead of the current
 * mock-generic implementation.
 *
 *)

module NewList;

  define obj attribute implementation;

  obj ListElem;
  obj List is ListElem*
    ops: Append, Prepend, Insert, Push, Pop, Enqueue, Dequeue,
	GetNth, SetNth, RemoveNth, DelNth, Find, FindPos, Len, Print;
    description: (*
	List is a standard flexible list.
    *)
  end;

  obj OrderedList < List
    ops: Sort;
    description: (*
	OrderedList 
  end;


  op Append(l:List, le:ListElem)->(l':List)
    description: (*
	Append the given ListElem to the end of the given list and return the
	result.
    *);

    pre: ;

    post:
	(*
	 * The length of l' is one greater than l.
         *)	
	(#l = #l' + 1)

	    and

	(*
	 * The last element of l' is the given new element le.
         *)
	(l'[#l + 1] = le)

	    and

	(*
	 * No junk, no confusion.  I.e., everything in l' is the same as in l,
	 * up to but not including the newly appended element.  This includes
	 * the positions of elements, not just their existence in the list.
         *)
	forall (i in [1..#l]) (l[i] = l'[i]);

    implementation: l' := l + le;

  end;

  obj ListIterator is List and IterationState
    ops: GetNext, Reset;
  end;

  obj IterationState is integer;

end NewList;