DEFINITION MODULE Queues; 
(* So sollen Spezifikationen aussehen. *)
(* Formalitaetsgrad der Kommentare nach Belieben. *)

TYPE  Queue;		(* Folge 						*)
      Entry = CHAR;	(* aus Elementen vom Typ Entry.				*)
      CONST max = 200;	(* Inv.: maximale Laenge ist max.			*)

PROCEDURE append(e: Entry; q: Queue): BOOLEAN;
		(* Vor.: Die Laenge von q ist kleiner als max.			*)
		(*		  [Genauer: q#NIL, und die Laenge von q^ ...]	*)
		(* Eff.: q ist hinten um e erweitert.				*)
		(*[Erg.: TRUE falls q#NIL, und die Laenge von q^ ...,	*)
		(*       sonst FALSE.					   ]	*)
		
PROCEDURE remove(VAR e: Entry; q: Queue): BOOLEAN;
		(* Vor.: q ist nicht leer.					*)
		(* Eff.: q ist um das erste Element reduziert.			*)
		(*       e hat den Wert dieses Elements.			*)
		
PROCEDURE length(q: Queue): CARDINAL;
		(* Vor.: -							*)
		(* Erg.: Die Laenge von q.					*)
		
PROCEDURE newQueue(): Queue;
		(* Vor.: -							*)
		(* Erg.: Eine neue Folge, leer.					*)
		(*       [Genauer: Ein Verweis auf ein neues Folgen-	        *)
		(*		  Objekt, initialisiert als leere Folge.]       *)
		
PROCEDURE dispQueue(VAR q: Queue);
		(* Vor.: -							*)
		(* Eff.: Effekt von DISPOSE(q)					*)
		(*       [nach Finalisierung von q]				*)
END Queues.
