(****
 *
 * Module Rolodex defines the main Rolodex object, its component objects, and
 * the rolodex editing operations.
 *
 *)

module Rolodex;

  export Rolodex, Card, Name, Id, Add, Find, Change, Delete;

  object Rolodex is
    components: Card*;
    description: (*
	A Roldex is a collection of cards.
    *);
  end Rolodex;

  object Card is
    components: name:Name and id:Id and age:Age and sex:Sex and addr:Address;
    description: (*
	A Card contains the information for a person stored in a Rolodex.  The
        information is a name, id, age, sex, and street address.
    *);
  end Card;

  object Name is string;
  object Id is integer;
  object Age is integer;
  object Sex is Male or Female;
  object Male;
  object Female;
  object Address is string;

  operation Add
    inputs: r:Rolodex, c:Card;
    outputs: r':Rolodex;

    description: (*
        Add the given card to the given rolodex if a card of the same id is not
        already there.
    *);

    precondition:
        (*
         * There is no card in the input rolodex with the same id as the given
         * input card.
         *)
        not CardAlreadyThere(c, r)

            and

        (*
         * The values of the given card fields are valid.
         *)
        CardIsValid(c);

    postcondition:
        (* 
         * A card is in the output rolodex iff it is in the input rolodex or
         * it's the new card to be added.
         *)
        forall (c':Card)
            (c' in r') iff ((c' in r) or (c' = c));

  end Add;

  operation Find
    inputs: r:Rolodex, n:Name;
    outputs: cl:Card*;

    description: (*
        Find all of the cards of the given name in the given rolodex.
    *);

    postcondition:

        (*
         * Cards in the output list consist of those in the input rolodex with 
         * the given name.
         *)
        forall (c:Card)
            (c in cl) iff ((c in r) and (c.name = n))

            and

        (*
         * A multi-card output list is sorted in ascending order by card id.
         *)
        forall (i:integer | (i >= 1) and (i < #cl))
            cl[i].id < cl[i+1].id;

  end Find;

  operation Change
    inputs: r:Rolodex, oldc:Card, newc:Card;
    outputs: r':Rolodex;

    description: (*
        Change the given old card to the given new card in the given rolodex.
    *);

    precondition:
        (*
         * The given old card is in the input rolodex.
         *)
        (oldc in r)

	    and

        (*
         * There is no card in the input rolodex with the same id as the given
         * new card.
         *)
        not CardAlreadyThere(newc, r)

            and

        (*
         * The values of the given new card fields are valid.
         *)
        CardIsValid(newc);

    postcondition:
        (*
         * A card is in the output rolodex iff it is in the input rolodex and
         * is not the old card, or it's the new card.
         *)
        forall (c':Card)
            (c' in r') iff (((c' in r) and (c' != oldc)) or (c' = newc));

  end Change;

  operation Delete
    inputs: r:Rolodex, c:Card;
    outputs: r':Rolodex;

    description: (*
        Delete the given card from the given rolodex.
    *);

    precondition: 
        (*
         * The given card is in the input rolodex.
         *)
        c in r;

    postcondition:
        (*
         * A card is in the output rolodex iff it is in the input rolodex and
         * it is not the given card to be deleted.
         *)
        forall (c':Card)
            (c' in r') iff ((c' in r) and (c' != c));

  end Delete;

  function CardAlreadyThere(c:Card, r:Rolodex)->boolean =
    not (exists (c' in r) c'.id = c.id);

  function CardIsValid(c: Card)->boolean =

    (*
     * The length of the name is <= 30 characters.
     *)
    (#(c.name) <= 30)

	and

    (*
     * The length (i.e, numer of digits) of the id is 9.
     *)
    (#(c.id) = 9)

	and

    (*
     * The age is a reasonable range.
     *)
    ((c.age >= 0) and (c.age <= 200))

	and

    (*
     * The length of the address is <= 40 chars.
     *)
    (#(c.addr) < 40);

end Rolodex;