(****
 *
 * Module Admin defines the objects and operations related to maintaining the
 * user, group, room, and global options databases of the Calendar Tool.
 *
 *)
module Admin;

  export UserDB, GroupDB, RoomDB, Id;

  object UserDB is
    components: UserRecord*;
    description: (*
        UserDB is the repository of registered user information.
    *);
  end UserDB;

  object UserRecord is
    components: name:Name and id:Id and email:EmailAddress and
        phone:PhoneNumber;
    description: (*
        A UserRecord is the information stored about a registered user of the
        Calendar Tool.  The Name component is the user's real-world name.  The
        Id is the unique identifier by which the user is known to the Calendar
        Tool.  The EmailAddress is the electronic mail address used by the
        Calendar Tool to contact the user when necessary.  The PhoneNumber is
        for information purposes; it is not used by the Calendar Tool for
        contacting the user.
    *);
  end UserRecord;

  object Name is string
    description: (* The name of a registered user. *);
  end;

  object Id is string
    description: (* The unique id of a registered user. *);
  end;

  object EmailAddress is string
    description: (* The electronic mail address of a registered user. *);
  end;

  object PhoneNumber is area:Area and number:Number
    description: (*
        A phone number consists of a three-digit area code and seven-digit
        number.
    *);
  end;

  object Area is integer
    description:  (*
        The three-digit area code component of a user phone number.
    *);
  end Area;

  object Number is integer
    description:  (*
        The seven-digit number component of a user phone number.
    *);
  end Number;

  operation AddUser is
    inputs: udb:UserDB, ur:UserRecord;
    outputs: udb':UserDB;

    precondition:
        (*
         * There is no user record in the input UserDB with the same id as the
         * record to be added.
         *)
        (not (exists (ur' in udb) ur'.id = ur.id))

            and

        (*
         * The id of the given user record is not empty and 8 characters or
         * less.
         *)
        (ur.id != nil) and (#(ur.id) <= 8)

            and

        (*
         * The email address is not empty.
         *)
        (ur.email != nil)

            and

        (*
         * If the phone area code and number are present, they must be 3 digits
         * and 7 digits respectively.
         *)
        (if (ur.phone.area != nil) then (#(ur.phone.area) = 3)) and
        (if (ur.phone.number != nil) then (#(ur.phone.number) = 7));

    postcondition:
        (*
         * A user record is in the output db if and only if it is the new
         * record to be added or it is in the input db.
         *)
        forall (ur':UserRecord)
            (ur' in udb') iff ((ur' = ur) or (ur' in udb));

    description: (*
        Add the given UserRecord to the given UserDB.  The Id of the given user
        record must not be the same as a user record already in the UserDB.
        The Id component is required and must be eight characters or less.  The
        email address is required.  The phone number is optional; if given, the
        area code and number must be 3 and 7 digits respectively.
    *);
  end AddUser;

  operation FindUser is
    inputs: udb:UserDB, id:Id;
    outputs: ur':UserRecord;

    precondition: ;

    postcondition:
        (*
         * If there is a record with the given id in the input db, then the
         * output record is equal to that record, otherwise the output record
         * is empty.
         *)
        (exists (ur in udb) (ur.id = id) and (ur' = ur))
            or
        (ur' = nil);

    description: (*
        Find a user by unique id.
    *);
  end FindUser;

  operation FindUser is
    inputs: udb:UserDB, n:Name;
    outputs: url:UserRecord*;

    precondition: ;

    postcondition:
        (*
         * The output list consists of all records of the given name in the
         * input db.
         *)
        (forall (ur' in url) (ur' in udb) and (ur'.name = n))

            and

        (*
         * The output list is sorted alphabetically by id.
         *)
        (forall (i:integer | (i >= 1) and (i < #url))
            url[i].id < url[i+1].id);


    description: (*
        Find a user or users by real-world name.  If more than one is found,
        the output list is sorted by id.
    *);
  end FindUser;

  operation FindUser is
    inputs: udb:UserDB, id:Id, n:Name;
    outputs: ur':UserRecord;

    precondition: ;

    postcondition:
        (*
         * If there is a record with the given name and id in the input db,
         * then the output record is equal to that record, otherwise the output
         * record is empty.
         *)
        (exists (ur in udb) (ur.name = n) and (ur.id = id) and (ur' = ur))
            or
        (ur' = nil);

    description: (*
        Find a user by both name and id.  This overload of FindUser is
        presumably used infrequently.  Its utility is to confirm that a
        particular user name and id are paired as assumed.
    *);
  end FindUser;

  operation ChangeUser is
    inputs: udb:UserDB, gdb:GroupDB, old_ur:UserRecord, new_ur:UserRecord;
    outputs:  udb':UserDB, gdb':GroupDB;

    precondition:
        (*
         * The old and new user records are not the same.
         *)
        (old_ur != new_ur)

            and

        (*
         * The old record is in the given db.
         *)
        (old_ur in udb)

            and

        (*
         * There is no user record in the input UserDB with the same id as the
         * new record to be added.
         *)
        (not (exists (new_ur' in udb) new_ur'.id = new_ur.id))

            and

        (*
         * The id of the new record is not empty and 8 characters or less.
         *)
        (new_ur.id != nil) and (#(new_ur.id) <= 8)

            and

        (*
         * The email address is not empty.
         *)
        (new_ur.email != nil)

            and

        (*
         * If the phone area code and number are present, they must be 3 digits
         * and 7 digits respectively.
         *)
        (if (new_ur.phone.area != nil) then (#(new_ur.phone.area) = 3)) and
        (if (new_ur.phone.number != nil) then (#(new_ur.phone.number) = 7));

    postcondition:
        (*
         * A user record is in the output db if and only if it is the new
         * record to be added or it is in the input db, and it is not the old
         * record.
         *)
        forall (ur':UserRecord)
            (ur' in udb') iff (((ur' = new_ur) or (ur' in udb)) and
                                   (ur' != old_ur))

            and

        (*
         * If new id is different than old id, then all occurrences of old id
         * in the GroupDB are replaced by new id.
         *)
        if (old_ur.id != new_ur.id)
        then
            ... (* Logic left as exercise for the reader. *) ;

    description: (*
        Change the given old UserRecord to the given new record.  The old and
        new records must not be the same.  The old record must already be in
        the input db.  The new record must meet the same conditions as for the
        input to the AddUser operation.  Typically the user runs the FindUser
        operation prior to Change to locate an existing record to be changed.

        If the user record id is changed, then change all occurrences of the
        old id in the group db to the new id.
    *);
  end ChangeUser;

  operation DeleteUser is
    inputs: udb:UserDB, gdb:GroupDB, ur:UserRecord;
    outputs: udb':UserDB, gdb':GroupDB, lgw:LeaderlessGroupsWarning;

    precondition: 
        (*
         * The given UserRecord is in the given UserDB.
         *)
        ur in udb;

    postcondition: 
        (*
         * A user record is in the output db if and only if it is not the
         * existing record to be deleted and it is in the input db.
         *)
        (forall (ur':UserRecord)
            (ur' in udb') iff ((ur' != ur) and (ur' in udb)))

            and

        (*
         * The id of the deleted user is not in the leader or member lists of
         * any group in the output GroupDB.  (NOTE: This clause is not as
         * strong as a complete "no junk, no confusion" spec.  Why not?  Should
         * it be?)
         *)
        (forall (gr in gdb')
            (not (ur.id in gr.leaders)) and (not (ur.id in gr.members)))

            and

        (*
         * The LeaderlessGroupsWarning list contains the ids of all groups
         * whose only leader was the user who has just been deleted.
         *)
        (forall (gr in gdb)
            forall (id:Id)
                (id in lgw) iff ((#(gr.leaders) = 1) and
                                   (gr.leaders[1] = ur.id)));

    description: (*
        Delete the given user record from the given UserDB.  The given record
        must already be in the input db.  Typically the user runs the FindUser
        operation prior to Delete to locate an existing record to delete.

        In addition, delete the user from all groups of which the user is a
        member.  If the deleted user is the only leader of a one more groups,
        output a warning indicating that those groups have become leaderless.
    *);
  end DeleteUser;

  object LeaderlessGroupsWarning is
    components: Name*;
    description: (*
        LeaderlessGroupsWarning is an secondary output of the Change and
        DeleteUser operations, indicating the names of zero or more groups that
        have become leaderless as the result of a user having been deleted.
    *);
  end LeaderlessGroupsWarning;

  object GroupDB is
    components: GroupRecord*;
    description: (*
        UserDB is the repository of user group information.
    *);
  end GroupDB;

  object GroupRecord is
    components: name:Name and leaders:Leaders and members:Members;
    description: (*
        A GroupRecord is the information stored about a user group.  The Name
        component is a unique group name of any length.  Leaders is a list of
        zero or more users designated as group leader.  Members is the list of
        group members, including the leaders.  Both lists consist of user id's.
        Normally a group is required to have at least one leader.  The only
        case that a group becomes leaderless is when its leader is deleted as a
        registered user.
    *);
  end GroupRecord;

  object Leaders is Id*
    description: (*
        List of user ids for the zero or more leaders of a group.
    *);
  end;

  object Members is Id*
    description: (*
        List of user ids for the zero or more members of a group.
    *);
  end;

  operation AddGroup is
    inputs: gdb:GroupDB, udb:UserDB, gr:GroupRecord;
    outputs: gdb':GroupDB;

    precondition:
        (*
         * All group members are registered users.
         *)
        (forall (id in gr.members) exists (ur in udb) ur.id = id)

            and

        (*
         * All group leaders are members of the group.
         *)
        (forall (id in gr.leaders) id in gr.members);

    postcondition:
        (*
         * A group record is in the output db if and only if it is the new
         * record to be added or it is in the input db.
         *)
        forall (gr':GroupRecord)
            (gr' in gdb') iff ((gr' = gr) or (gr' in gdb));

    description: (*
        Add the given GroupRecord to the given GroupDB.  The name of the given
        group must not be the same as a group already in the GroupDB.  All
        group members must be registered users.  The leader(s) of the group
        must be members of it.
    *);
  end AddGroup;

  operation FindGroup is
    inputs: gdb:GroupDB, n:Name;
    outputs: gr':GroupRecord;

    precondition: ;

    postcondition:
        (*
         * If there is a record with the given name in the input db, then the
         * output record is equal to that record, otherwise the output record
         * is empty.
         *)
        (exists (gr in gdb) (gr.name = n) and (gr' = gr))
            or
        (gr' = nil);

    description: (*
        Find a group by unique name.
    *);
  end FindGroup;

  operation ChangeGroup is
    inputs: gdb:GroupDB, udb:UserDB, old_gr:GroupRecord, new_gr:GroupRecord;
    outputs: gdb':GroupDB;

    precondition:
        (*
         * The old and new group records are not the same.
         *)
        (old_gr != new_gr)

            and

        (*
         * All group members are registered users.
         *)
        (forall (id in new_gr.members) exists (ur in udb) ur.id = id)

            and

        (*
         * All group leaders are members of the group.
         *)
        (forall (id in new_gr.leaders) id in new_gr.members);

    postcondition:
        (*
         * A group record is in the output db if and only if it is the new
         * record to be added or it is in the input db, and it is not the old
         * record.
         *)
        forall (gr':GroupRecord)
            (gr' in gdb') iff (((gr' = new_gr) or (gr' in gdb)) and
                                   (gr' != old_gr));

    description: (*
        Change the given old GroupRecord to the given new record.  The old and
        new records must not be the same.  The old record must already be in
        the input db.  The new record must meet the same conditions as for the
        input to the AddGroup operation.  Typically the user runs the FindGroup
        operation prior to Change to locate an existing record to be changed.
    *);
  end ChangeGroup;

  operation DeleteGroup is
    inputs: gdb:GroupDB, gr:GroupRecord;
    outputs: gdb':GroupDB;

    precondition: 
        (*
         * The given GroupRecord is in the given GroupDB.
         *)
        gr in gdb;

    postcondition: 
        (*
         * A group record is in the output db if and only if it is not the
         * existing record to be deleted and it is in the input db.
         *)
        (forall (gr':GroupRecord)
            (gr' in gdb') iff ((gr' != gr) and (gr' in gdb)));

    description: (*
        Delete the given group record from the given GroupDB.  The given record
        must already be in the input db.  Typically the user runs the FindGroup
        operation prior to Delete to locate an existing record to delete.
    *);
  end DeleteGroup;

  object RoomDB is
    components: RoomRecord*;
    description: (*
        
    *);
  end RoomDB;

  object RoomRecord is
    components: ;
    description: (*
        
    *);
  end RoomRecord;


  (*
   * Global options TBD.
   *)

end Admin;