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

  from Schedule import ScheduledItem, Title, StartTime, Duration,
        StartOrDueDate, EndDate, WeeklyDetails;
  export UserDB, GroupDB, LocationDB, UserId;

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

  object UserRecord
    components: name:Name and id:UserId and
        phone:PhoneNumber and email:EmailAddress and host:HostComputer and
        uid:ComputerUserID and home_dir:HomeDirectory and
        item_limit:ItemLimit and privileges:AdminPrivileges;
    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
        nickname is an indvidualizable short-hand name for the user.  The
        UserId 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 UserId 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 has 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;

  object HostComputer is string
    description: (*
        The unique identifier of the host computer on which the user runs the
        Calendar Tool. The format of the identifier is platform-dependent,
        based on the type of network to which host computers are attached.  IP
        address is a typical format.
    *);
  end HostComputer;

  object ComputerUserID is string
    description: (*
       The user's identification on the host computer.
    *);
  end ComputerUserID;

  object HomeDirectory is string
    description: (*
        The file directory (i.e., folder) assigned as the user's home directory
        on the host computer.
    *);
  end HomeDirectory;

  object ItemLimit is integer
    description: (*
        The maximum number of scheduled items that can be stored for the user
        in the Calendar Tool central repository.  The limit value is optional.
        If it is absent, there is no limit.  The item limit can be zero, in
        which case the user has an empty calendar in the central repository.
    *);
  end ItemLimit;

  object AdminPrivileges is boolean
    description: (*
       Indicates if the user has administrative privileges.
    *);
  end AdminPrivileges;

  operation AddUser
    inputs: udb:UserDB, gdb:GroupDB, ur:UserRecord;
    outputs: udb':UserDB;
    description: (*
        Add the given UserRecord to the given UserDB.  The UserId of the given
        user record must not be the same as a user record already in the UserDB
        or any group record in the GroupDB.  The UserId 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.
    *);

    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

        (*
         * There is no group record in the input GroupDB with the same id as
         * the record to be added.
         *)
        (not (exists (gr' in udb) gr'.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));

  end AddUser;

  operation FindUser
    inputs: udb:UserDB, id:UserId;
    outputs: ur':UserRecord;
    description: (*
        Find a user by unique id.
    *);

    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
        (not (exists (ur in udb) (ur.id = id)) and (ur' = nil));

  end FindUser;

  operation FindUser
    inputs: udb:UserDB, n:Name;
    outputs: url:UserRecord*;
    description: (*
        Find a user or users by real-world name.  If more than one is found,
        the output list is sorted by id.
    *);

    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);

  end FindUser;

  operation FindUser
    inputs: udb:UserDB, id:UserId, n:Name;
    outputs: ur':UserRecord;
    description: (*
        Find a user by both name and id.  This overload of FindUser
        presumably used infrequently.  Its utility is to confirm that a
        particular user name and id are paired as assumed.
    *);

    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
        (not (exists (ur in udb) (ur.name = n) and (ur.id = id)) and
                (ur' = nil));

  end FindUser;

  operation ChangeUser
    inputs: udb:UserDB, gdb:GroupDB, old_ur:UserRecord, new_ur:UserRecord;
    outputs:  udb':UserDB, gdb':GroupDB;
    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.
                                                                            <p>
        If the user record id is changed, then change all occurrences of the
        old id in the group db to the new id.
    *);

    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. *) ;

  end ChangeUser;

  operation DeleteUser
    inputs: udb:UserDB, gdb:GroupDB, ur:UserRecord;
    outputs: udb':UserDB, gdb':GroupDB, lgw:LeaderlessGroupsWarning;
    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.
                                                                            <p>
        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.
    *);

    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:UserId)
                (id in lgw) iff ((#(gr.leaders) = 1) and
                                   (gr.leaders[1] = ur.id)));

  end DeleteUser;

  object LeaderlessGroupsWarning
    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
    components: GroupRecord*;
    description: (*
        UserDB is the repository of user group information.
    *);
  end GroupDB;

  object GroupRecord
    components: name:Name and id:GroupId 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 GroupId is string
    description: (* The unique id of a registered group. *);
  end GroupId;

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

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

  operation AddGroup
    inputs: gdb:GroupDB, udb:UserDB, gr:GroupRecord;
    outputs: gdb':GroupDB;
    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.
    *);

    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));

  end AddGroup;

  operation FindGroup
    inputs: gdb:GroupDB, n:Name;
    outputs: gr':GroupRecord;
    description: (*
        Find a group by unique name.
    *);

    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
        (not (exists (gr in gdb) (gr.name = n)) and (gr' = nil));

  end FindGroup;

  operation ChangeGroup
    inputs: gdb:GroupDB, udb:UserDB, old_gr:GroupRecord, new_gr:GroupRecord;
    outputs: gdb':GroupDB;
    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.
    *);

    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));

  end ChangeGroup;

  operation DeleteGroup
    inputs: gdb:GroupDB, gr:GroupRecord;
    outputs: gdb':GroupDB;
    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.
    *);

    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)));

  end DeleteGroup;

  object LocationDB
    components: LocationRecord*;
    description: (*
        The LocationDB contains the location records that provide information
        about the locations at which items are scheduled.
    *);
  end LocationDB;

  object LocationRecord
    components: Name and Number and Bookings and Remarks;
    description: (*
        A LocationRecord has a Name and Number which serve to identify where
        the location is.  Both fields are free-form strings and the Calendar
        Tool enforces no constraints on their values.  The Bookings component
        is a list of the items or other that are scheduled in the
        location.  The Remarks component is a free-form text that can be used
        to describe any other pertinent information about the room.
    *);
  end LocationRecord;

  obj Bookings has Booking*
    description: (*
        Bookings define all of the times that a location is in use, i.e.,
        "booked". 
    *);
  end Bookings;

  object Booking
    components: ScheduledItem or UnscheduledBooking;
    description: (*
        A location booking is either a scheduled item or an unscheduled
        booking.
    *);
  end Booking;

  object UnscheduledBooking
    components: Use and StartTime and Duration and Days and StartDate and
        EndDate;
    description: (*
        An unscheduled booking allows an adiminstratot to set times during
        which a location is booked from some other purpose than a scheduled
        calendar tool item.  The Use component describes the booking.  The
        StartTime, Duration, StartDate and EndDate are as for a scheculed
        item.  The Days component is the same as the WeeklyDetails of a
        recurring item.
    *);
  end UnscheduledBooking;

  object Use is string
    description: (*
        The Use of an unscheduled booking is what ever description of the
        booking the user want to provide.
    *);
  end Use;
  object Days is WeeklyDetails;
  object StartDate is StartOrDueDate;

  obj Remarks is string
    description: (*
        Remarks are any information the user chooses to enter about a booking.
    *);
  end Remarks;

end Admin;