module StandardLibrary;

  export Object, AddWithRetentionAndNoJunk;

  obj Object;-- A la Java, this should be THE top object from which all inherit

  function AddWithRetentionAndNoJunk(
        o:Object, in_list:Object*, out_list:Object*) -> boolean =

    (*
     * The basic condition is stated straightforwardly using the "in" operator.
     *)
    (o in out_list)

        and

    (*
     * The retention condition is stated in logical terms as:
     *
     *     "For each element in the input list,
     *      that element is in the output list."
     *)
    (forall (o' in in_list) o' in out_list)

        and

    (*
     * The no junk condition is stated succinctly by saying that the number of
     * elements in the output list is one greater than the number of elements
     * in the input list.  Given the preceding two conditions, this precludes
     * any extra junk being in the output.
     *)
    (#out_list = #in_list + 1)

    description: (*
        The AddWithRetentionAndNoJunk function defines the logic of a
        "retention with no junk rule" for adding an object to a collection.
        The rule is stated in functional terms, based on an object to be added,
        an input list to which the addition is to be made, and an output list
        to which the object has been successfully added.  The logic uses only
        bounded quantification.

        The retention-with-no-junk rule is stated with three conditions:

            (1) The basic condition:
                The object to be added is in fact in the output list.
        
            (2) The retention condition:
                Everything in the input list is retained in the output list.

            (3) The no junk condition:
                Nothing else is in the output list.

        It is important to note that this logic is suited to the case where the
        input list does not contain duplicate items and the object to be added
        is not already in the input list.  If either or both of these
        conditions is false, then this logic does not ensure that the number of
        duplicate items is the same in the input and output lists.  For
        example, suppose o = 1 and in_list = [1, 1, 1, 1].  The logic of this
        function is true if out_list = [1, 1, 1, 1, 2], but it is also true if
        out_list = [1, 2, 2, 2, 2].
    *);

  end AddWithRetentionAndNoJunk;

end StandardLibrary;