head	1.1;
access;
symbols;
locks; strict;
comment	@# @;


1.1
date	93.07.22.19.39.52;	author ids;	state Exp;
branches;
next	;


desc
@@


1.1
log
@Initial revision
@
text
@MODULE LinkedList;

FROM Storage IMPORT DEALLOCATE;

TYPE
  List     = POINTER TO ListNode;
  ListNode = RECORD
               item : INTEGER; (* or whatever *)
               next : List
             END;


PROCEDURE DeleteItem (i : INTEGER; VAR L : List);
(* pre:  there is at most one ("special") list-node in L with item-value i
 * post: deletes the list-node in L with item-value i, if such there be,
 *       preserving the order of the remainder of L. Or, if there is
 *       no such special list-node, has no effect.
 *)

VAR
  before, temp : List;

BEGIN

  (* assertion: the special list-node either exists, once, or not at all
   *)

  IF (L # NIL) AND (L^.item = i) THEN (* we really do modify L, the pointer *)

    (* assertion: the special list-node exists, and is L^
     *)

    temp := L;
    L := temp^.next;
    DISPOSE(temp)

    (* assertion: the special list-node has been removed
     *
     * therefore: [trivially:] the special list-node does not still exist
     *
     * therefore: [trivially:] the special list-node, if there ever was any,
     *                         does not still exist
     *)

  ELSE (* we only modify things hanging off L, not L itself *)

    (* assertion: the special list-node, if it exists, is L^.next^
     *            or further
     *)

    before := L;

    (* assertion: the special list-node, if it exists, is before^.next^
     *            or further
     *)

    WHILE (before # NIL) AND (before^.next # NIL) DO

      (* assertion: the special list-node, if it still exists, is before^.next^
       *            or further
       *)

      IF before^.next^.item = i THEN

        (* assertion: the special list-node still exists, and is before^.next^
         *)

        temp := before^.next;
        before^.next := temp^.next;
        DISPOSE(temp);

        (* assertion: the special list-node has been removed
         *
         * therefore: [trivially:] the special list-node, if it still exists, is
         *                         before^.next^.next^ or further
         *)

        before := NIL (* to signal we've finished: you could just RETURN *)
      END(*IF*);

      (* assertion: the special list-node, if it still exists, is
       *            before^.next^.next^ or further
       *)

      before := before^.next

      (* assertion: the special list-node, if it still exists, is
       *            before^.next^ or further
       *)

    END(*WHILE*)

    (* assertion: the special list-node, if it still exists, is
     *            before^.next^ or further
     *
     * assertion: (before = NIL) OR (before^.next = NIL)
     *   that is: before^.next^ does not exist
     *            [and trivially, nor does anything further]
     *
     * therefore: the special list-node, if there ever was any,
     *            does not still exist
     *)

  END(*IF*)

  (* assertion: the special list-node, if there ever was any,
   *            does not still exist
   *)

END DeleteItem;


BEGIN
END LinkedList.
@