17,19c17,18
<  * user, group, and location databases.  It also has objects and operations for
<  * the other administrative functionality related to remote hosts and
<  * communicating between regular users and administrators.
---
>  * user, group, location, and global options databases of the Calendar Tool.
>  *
24,31c23,24
<        StartOrDueDate, EndDate, WeeklyDetails;
<   from CalendarDB import AdminWorkSpace, UserCalendar;
<   from MultiUserEnvir import Server, HostId, ScheduledToStopIn, ConnectedUsers,
<           Network, NotificationQueue;
<   from File import File, FileSize;
< 
<   export UserDB, GroupDB, LocationDB, UserId, AdminPassword, AdminEmailAddress,
<          IsRunning, NotificationMessage;
---
>         StartOrDueDate, EndDate, WeeklyDetails;
>   export UserDB, GroupDB, LocationDB, UserId;
42,44c35,38
<     components: name:UserName and id:UserId and password:UserPassword and
<         email:EmailAddress and phone:Phone and limit:CalendarSizeLimit and
<         notification_queue:NotificationQueue;
---
>     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;
47,48c41,43
<         Calendar Tool.  The UserName component is the user's real-world name.
<         The UserId is the unique identifier by which the user is known to 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
52,55c47
<         contacting the user.  The CalendarSizeLimit is the maximum size of the
<         user's calendar on the central host.  The NotificationQueue contains
<         messages sent to the user from the administrator or Calendar Tool
<         server program.
---
>         contacting the user.
59c51
<   object UserName is last:LastName and first:FirstName and middle:MiddleName
---
>   object Name is string
63,81d54
<   object LastName is string
<     description: (*
<         User last name.  This component of the user name is required; first
<         and middle are optional.
<     *);
<   end LastName;
< 
<   object FirstName is string
<     description: (*
<        Optional first name in a user record.
<     *);
<   end FirstName;
< 
<   object MiddleName is string
<     description: (*
<       Optional middle name in a user record.
<     *);
<   end MiddleName;
< 
83,85c56
<     description: (*
<         The unique id of a registered Calendar Tool user.
<     *);
---
>     description: (* The unique id of a registered user. *);
92c63
<   object Phone is area:Area and number:Number
---
>   object PhoneNumber is area:Area and number:Number
133,142c104
<   object CalendarSizeLimit is integer
<     description: (*
<         The maximum size in megabytes of the user calendar on the central host
<         computer.  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 CalendarSizeLimit;
< 
<   object UserPassword is EncryptedString
---
>   object ItemLimit is integer
144c106,109
<         The user password.
---
>         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.
146c111
<   end AdminPassword;
---
>   end ItemLimit;
148c113
<   object EncryptedString is string
---
>   object AdminPrivileges is boolean
150,152c115
<         As a data type, an encrypted string is the same as a plain string.  The
<         point of this definition is to emphasize its encrypted value.  The
<         operations SetUserPassword and SetAdminPassword perform the encryption.
---
>        Indicates if the user has administrative privileges.
154c117
<   end EncryptedString;
---
>   end AdminPrivileges;
217,218c180,202
<   operation SearchByName is
<     inputs: udb:UserDB, n:UserName;
---
>   operation FindUser is
>     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 is
>     inputs: udb:UserDB, n:Name;
221,222c205,206
<         Search for a user or users by name.  If more than one is found, the
<         output list is sorted by id.
---
>         Find a user or users by real-world name.  If more than one is found,
>         the output list is sorted by id.
242c226
<   end SearchByName;
---
>   end FindUser;
244,245c228,229
<   operation SearchById is
<     inputs: udb:UserDB, id:UserId;
---
>   operation FindUser is
>     inputs: udb:UserDB, id:UserId, n:Name;
248c232,234
<         Search for a user by unique id.
---
>         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.
255,257c241,243
<          * 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.
---
>          * 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.
259c245
<         (exists (ur in udb) (ur.id = id) and (ur' = ur))
---
>         (exists (ur in udb) (ur.name = n) and (ur.id = id) and (ur' = ur))
261c247,248
<         (not (exists (ur in udb) (ur.id = id)) and (ur' = nil));
---
>         (not (exists (ur in udb) (ur.name = n) and (ur.id = id)) and
>                 (ur' = nil));
263c250
<   end SearchByName;
---
>   end FindUser;
266,268c253,254
<     inputs: udb:UserDB, uc:UserCalendar, old_ur:UserRecord, new_ur:UserRecord;
<     outputs:  udb':UserDB, uc':UserCalendar,
<               cscn:CalendarSizeChangeNotification;
---
>     inputs: udb:UserDB, gdb:GroupDB, old_ur:UserRecord, new_ur:UserRecord;
>     outputs:  udb':UserDB, gdb':GroupDB;
273,276c259,260
<         input to the AddUser operation.  Also, the ID in the new record must be
<         the same as in the old recordd, i.e., the ID cannot be changed.
<         Typically the user runs a search operation prior to Change to locate an
<         existing record to be changed.
---
>         input to the AddUser operation.  Typically the user runs the FindUser
>         operation prior to Change to locate an existing record to be changed.
279,282c263
<         old id in the group db to the new id.  If the calendar size limit is
<         changed, and current calendar size is greater than the changed-to size,
<         then reduce the size per the requirements in Section 2.6.5.5 and notify
<         the user of the change.
---
>         old id in the group db to the new id.
309,316d289
<          * There is no group record in the input GroupDB with the same id as
<          * new record.
<          *)
<         (not (exists (gr' in udb) gr'.id = new_ur.id))
< 
<             and
< 
<         (*
340c313
<          * record to be changed or it is in the input db, and it is not the old
---
>          * record to be added or it is in the input db, and it is not the old
349,350c322,328
<         if new_ur.limit * 1000000 &gt; uc.file.size
<         then uc' = ChangeCalendarSize(uc);
---
>         (*
>          * 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. *) ;
354,380d331
<   function ChangeCalendarSize(uc:UserCalendar)->(uc':UserCalendar) = ...
<     description: (*
<         Change the calenar size per the requirements in Section 2.6.5.5.
<         This'll be a piece of work.
<     *);
<   end ChangeCalendarSize;
< 
<   object CalendarSizeChangeNotification is string
<     description: (*
<         Notification sent to the user when the calendar size is reduced when
<         the new size limit is less than the current size.
<     *);
<   end CalendarSizeChangeNotification;
< 
<   function ReplaceUID(uil:UserId*, old_id:UserId, new_id:UserId)->UserId* =
<         if #uil = 0
<         then []
<         else
<             if uil[1] = old_id
<             then new_id + ReplaceUID(uil[2:#uil], old_id, new_id)
<             else uil[1] + ReplaceUID(uil[2:#uil], old_id, new_id)
< 
<     description: (*
<         Replace the old_id with the new_id in the given user ID list.
<     *);
<   end ReplaceUID;
< 
386c337
<         must already be in the input db.  Typically the user runs a search
---
>         must already be in the input db.  Typically the user runs the FindUser
426c377
<             forall (id:GroupId)
---
>             forall (id:UserId)
433c384
<     components: GroupId*;
---
>     components: Name*;
436c387
<         DeleteUser operations, indicating the IDs of zero or more groups that
---
>         DeleteUser operations, indicating the names of zero or more groups that
449,450c400,401
<     components: name:GroupName and id:GroupId and limit:CalendarSizeLimit and
<         members:Members and leaders:Leaders;
---
>     components: name:Name and id:GroupId and leaders:Leaders and
>         members:Members;
462,465d412
<   object GroupName is string
<     description: (* The name of a registered group. *);
<   end GroupName;
< 
515,543c462,463
<   operation SearchByName is
<     inputs: gdb:GroupDB, n:GroupName;
<     outputs: grl:GroupRecord*;
<     description: (*
<         Search for a group or groups by 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 (gr' in grl) (gr' in gdb) and (gr'.name = n))
< 
<             and
< 
<         (*
<          * The output list is sorted alphabetically by id.
<          *)
<         (forall (i:integer | (i &gt;= 1) and (i &lt; #grl))
<             grl[i].id &lt; grl[i+1].id);
< 
<   end SearchByName;
< 
<   operation SearchById is
<     inputs: gdb:GroupDB, id:GroupId;
---
>   operation FindGroup is
>     inputs: gdb:GroupDB, n:Name;
546c466
<         Search for a group by unique id.
---
>         Find a group by unique name.
553c473
<          * If there is a record with the given id in the input db, then the
---
>          * If there is a record with the given name in the input db, then the
557c477
<         (exists (gr in gdb) (gr.id = id) and (gr' = gr))
---
>         (exists (gr in gdb) (gr.name = n) and (gr' = gr))
559c479
<         (not (exists (gr in gdb) (gr.id = id)) and (gr' = nil));
---
>         (not (exists (gr in gdb) (gr.name = n)) and (gr' = nil));
561c481
<   end SearchById;
---
>   end FindGroup;
570c490
<         input to the AddGroup operation.  Typically the user runs a search
---
>         input to the AddGroup operation.  Typically the user runs the FindGroup
611c531
<         must already be in the input db.  Typically the user runs a search
---
>         must already be in the input db.  Typically the user runs the FindGroup
640,641c560
<     components: name:LocationName and num:LocationNumber and
<         bookings:Bookings and remarks:Remarks;
---
>     components: Name and Number and Bookings and Remarks;
652,670c571
<   object LocationName is string
<     description: (*
<         Possibly optional location name.  It is only required if the location
<         ID is empty.  The names for all empty-ID locations must be unique.
<     *);
<   end LocationName;
< 
<   object LocationNumber is string
<     description: (*
<        The number in some form of location in the location database.  Typically
<        it will be in some numeric form such as bldg-room, but there are no
<        specific requirements for the format.  Since such numbers may well
<        contain non-numeric characters, the representation is as a string.  As
<        noted in the specs for the AddLocation, this means that LocationNumbers
<        are sorted as strings, which may not give ideal results in all cases.
<     *);
<   end LocationNumber;
< 
<   object Bookings is Booking*
---
>   obj Bookings is Booking*
689c590
<         An unscheduled booking allows an administrator to set times during
---
>         An unscheduled booking allows an adiminstratot to set times during
692c593
<         StartTime, Duration, StartDate and EndDate are as for a scheduled
---
>         StartTime, Duration, StartDate and EndDate are as for a scheculed
713,1227d613
<   operation AddLocation is
<     inputs: ldb:LocationDB, lr:LocationRecord;
<     outputs: ldb':LocationDB;
<     description: (*
<         Add the given LocationRecord to the given LocationDB.  At least one of
<         the Name or Number components of the given record must be non-empty.
<         If the Name of the given record is the same as an existing record, its
<         Number component must be different than any existing record of the same
<         name.  If the Number of the given record is non-empty, it must be
<         different than the number of any existing record.
<     *);
<     precondition:
<         (*
<          * At least one of the Name or Number components of the input record is
<          * non-nil.
<          *)
<         (lr.name != nil) or (lr.num != nil)
< 
<             and
< 
<         (*
<          * There is no location record in the input LocationDB with the same
<          * name and number as the input record.
<          *
<          *)
<         (not (exists (lr' in ldb) (lr'.name = lr.name) and (lr'.num = lr.num)))
< 
<             and
< 
<         (*
<          * There is no location record in the input LocationDB with a non-empty
<          * number equal to the the Number of the input record
<          *)
<         (not (exists (lr' in ldb) if lr'.num != nil then lr'.num != lr.num));
< 
<     postcondition:
<         (*
<          * A location 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 (lr':LocationRecord)
<             (lr' in ldb') iff ((lr' = lr) or (lr' in ldb));
< 
<   end AddLocation;
< 
<   operation SearchByName is
<     inputs: ldb:LocationDB, n:LocationName;
<     outputs: lrl:LocationRecord*;
<     description: (*
<         Find a location or locations by name.  If more than one is found,
<         the output list is sorted by number.  The input name cannot be empty.
<     *);
< 
<     precondition: n != nil;
< 
<     postcondition:
<         (*
<          * The output list consists of all records of the given name in the
<          * input db.
<          *)
<         (forall (lr' in lrl) (lr' in ldb) and (lr'.name = n))
< 
<             and
< 
<         (*
<          * The output list is sorted alphabetically by id.
<          *)
<         (forall (i:integer | (i &gt;= 1) and (i &lt; #lrl))
<             lrl[i].num &lt; lrl[i+1].num);
< 
<   end SearchByName;
< 
<   operation SearchByNumber is
<     inputs: ldb:LocationDB, num:LocationNumber;
<     outputs: lr':LocationRecord;
<     description: (*
<         Find a location by unique number.  Since location number is only unique
<         if non-empty, the given input Number must be non-empty.  I.e., there
<         can be one or more location records with an empty number component in a
<         location database.
<     *);
< 
<     precondition: num != nil;
< 
<     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 (lr in ldb) (lr.num = num) and (lr' = lr))
<             or
<         (not (exists (lr in ldb) (lr.num = num)) and (lr' = nil));
< 
<   end SearchByNumber;
< 
<   operation ChangeLocation is
<     inputs: ldb:LocationDB, old_lr:LocationRecord, new_lr:LocationRecord;
<     outputs:  ldb':LocationDB;
<     description: (*
<         Change the given old LocationRecord 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 AddLocation operation.  Typically the user runs a
<         search operation prior to Change to locate an existing record to be
<         changed.
<     *);
< 
<     precondition:
<         (*
<          * The old and new user records are not the same.
<          *)
<         (old_lr != new_lr)
< 
<             and
< 
<         (*
<          * The old record is in the given db.
<          *)
<         (old_lr in ldb)
< 
<             and
< 
<         (*
<          * At least one of the Name or Number components of the new record is
<          * non-nil.
<          *)
<         (new_lr.name != nil) or (new_lr.num != nil)
< 
<             and
< 
<         (*
<          * There is no location record in the input LocationDB with the same
<          * name and number as the new record.
<          *
<          *)
<         (not (exists (lr' in ldb) (lr'.name = new_lr.name) and
<                                   (lr'.num = new_lr.num)))
< 
<             and
< 
<         (*
<          * There is no location record in the input LocationDB with a non-empty
<          * number equal to the the Number of the input record
<          *)
<         (not (exists (lr' in ldb) if lr'.num != nil
<                                   then lr'.num != new_lr.num));
< 
<     postcondition:
<         (*
<          * A location record is in the output db if and only if it is the new
<          * record to be changed or it is in the input db, and it is not the old
<          * record.
<          *)
<         forall (lr':LocationRecord)
<             (lr' in ldb') iff (((lr' = new_lr) or (lr' in ldb)) and
<                                    (lr' != old_lr));
< 
<   end ChangeLocation;
< 
<   operation DeleteLocation is
<     inputs: ldb:LocationDB, lr:LocationRecord;
<     outputs: ldb':LocationDB;
<     description: (*
<         Delete the given location record from the given LocationDB.  The given
<         record must already be in the input db.  Typically the user runs a
<         search operation prior to Delete to locate an existing record to
<         delete.
<     *);
< 
<     precondition:
<         (*
<          * The given LocationRecord is in the given LocationDB.
<          *)
<         lr in ldb;
< 
<     postcondition:
<         (*
<          * A location 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 (lr':LocationRecord)
<             (lr' in ldb') iff ((lr' != lr) and (lr' in ldb)));
< 
<   end DeleteLocation;
< 
< 
<   (**
<    * Objects and operations for other privileged admin commands.
<    *)
< 
<   object HostStatusInfo is
<     components: is_running:IsRunning and num_users:NumUsers;
<     description: (*
<        Information about a host, consisting of its running status and how many
<        users are connected.
<     *);
<   end HostStatusInfo;
< 
<   object IsRunning is boolean
<     description: (*
<        True if the server program is running.
<     *);
<   end IsRunning;
< 
<   object NumUsers is integer
<     description: (*
<        Number of users connected to a server.
<     *);
<   end NumUsers;
< 
<   operation CheckHostStatus is
<     inputs: aws:AdminWorkSpace;
<     outputs: hs:HostStatusInfo;
<     description: (*
<         Check the status of the given host server.
<     *);
<     precondition: ;
<     postcondition:
<         hs.is_running = aws.server.is_running and
<         hs.num_users = #aws.server.users;
<   end HostStatus;
< 
<   operation StartServer is
<     inputs: aws:AdminWorkSpace;
<     outputs: aws':AdminWorkSpace;
<     description: (*
<         Start the server designated in the given admin workspace.  In the
<         model, this is defined simply as setting the ser'vers is_running
<         component to true.  Implementors must perform whatever actions are
<         necessary to accomplish the actual invocation of the server program.
<     *);
<     precondition: not aws'.server.is_running;
<     postcondition: aws'.server.is_running;
<   end StartServer;
< 
<   operation StopServer is
<     inputs: aws:AdminWorkSpace, confirm:StopServerConfirmation;
<     outputs: aws':AdminWorkSpace, msg:StopServerMessage;
<     description: (*
<         Stop the server designated in the given admin workspace, or schedule it
<         to be stopped in a number of minutes.  In the model, this is defined
<         simply as setting the server's is_running to false or stop_scheduled
<         component to true.  Implementors must perform whatever actions are
<         necessary to accomplish the actual stoppage of the server program.  The
<         scheduling of stoppage would require temporal logic to specify fully;
<         this aspect is not specified here.
<     *);
<     precondition: aws'.server.is_running;
<     postcondition:
<         if confirm = 0
<         then aws'.server.is_running = false (* and
<              msg = HostIsDownMessage({HostIsDownPart1,
<                  aws.server.id,HostIsDownPart2}) *)
<         else aws' = ScheduleServerStopage(aws, confirm) (* and
<              msg = HostGoingDownMessage(HostGoingDownPart1,
<                  aws.server.id,HostIsDownPart2,confirm,
<                  HostGoingDownPart3) *);
<   end StartServer;
< 
<   object StopServerConfirmation is integer
<     description: (*
<        The amount of time in minutes before a server is scheculed to stop.  If
<        the value is zero, the server stops immediately.
<     *);
<   end StopServerConfirmation;
< 
<   function ScheduleServerStopage is
<     inputs: aws:AdminWorkSpace, confirm:StopServerConfirmation;
<     outputs: aws':AdminWorkSpace;
<     description: (*
<         Schedule the server in the given workspace to stop in the number of
<         minutes specified in the TimeToStop.  This is modeled here only as the
<         setting of a flag.  The temporal logic aspect of the postcondition is
<         not modeled; rather, it is defined as the postcondition comment about
<         starting a count-down timer.
<     *);
<     precondition: ;
<     postcondition:
<         aws'.server.stop_in = confirm
<         (*
<          * and
<          *
<             start a count-down timer to make the stoppage happen in the number
<             of minutes specified in the given confirmation.  When the timer
<             expires, aws'.is_running is set to false and the server is stopped.
<          *
<          *);
<   end ScheduleServerStopage;
< 
<   object StopServerMessage is
<     components: going_down:HostGoingDownMessage or is_down:HostIsDownMessage;
<     description: (*
<        Message output by StopServer operation that host is scheduled to go down
<        or has gone down, based on whether the stoppage is immediate or in some
<        number of minutes.
<     *);
<   end StopServerMessage;
< 
<   object HostGoingDownMessage  is
<     components: HostGoingDownPart1 and host_id:HostId and
<         HostGoingDownPart2 and confirm:StopServerConfirmation and
<         HostGoingDownPart3;
<     description: (*
< 
<     *);
<   end HostGoingDownMessage;
< 
<   object HostGoingDownPart1 = "The Calendar Tool server on central host "
<     description: (*
<        The first text part of the host-going-down message.
<     *);
<   end HostGoingDownPart1;
< 
<   object HostGoingDownPart2 = "will stop operating in"
<     description: (*
<        The second text part of the host-going-down message.
<     *);
<   end HostGoingDownPart2;
< 
<   object HostGoingDownPart3 =
<         "minutes." +
<         "At that time, you will be disconnected from this host and" +
<         "all meeting scheduling, viewing, and administrative commands" +
<         "for this host will be terminated and disabled."
<     description: (*
<        The third text part of the host-going-down message.
<     *);
<   end HostGoingDownPart3;
< 
<   object HostIsDownMessage is
<     components: HostIsDownPart1 and host_id:HostId and HostIsDownPart2;
<     description: (*
< 
<     *);
<   end HostIsDownMessage;
< 
<   object HostIsDownPart1 = "The Calendar Tool server on central host "
<     description: (*
<        The first text part of the host-is-down message.
<     *);
<   end HostIsDownPart1;
< 
<   object HostIsDownPart2 =
<         "has stopped." +
<         "" +
<         "You have been disconnected from this host and" +
<         "all meeting scheduling, viewing, and administrative commands" +
<         "for this host have been terminated and disabled."
<     description: (*
<        The second text part of the host-is-down message.
<     *);
<   end HostIsDownPart2;
< 
<   object ChangePasswordInfo is
<     components: current:CurrentPassword and new:NewPassword and
<         new_reentered:NewPasswordReentered;
<     description: (*
<        Information for entering a new password -- the current, the new, and the
<        new again.
<     *);
<   end ChangePasswordInfo;
< 
<   object CurrentPassword is string
<     description: (*
<         The string value that when encrypted must match the current
<         admininstrator password.
<     *);
<   end CurrentPassword;
< 
<   object NewPassword is string
<     description: (*
<         The string value of the new password;
<     *);
<   end NewPassword;
< 
<   object NewPasswordReentered is string
<     description: (*
<         The reentered string value of the new password;
<     *);
<   end NewPasswordReentered;
< 
<   object AdminPassword is EncryptedString
<     description: (*
<         The password used to gain entry to the Calendar Tool administration
<         program.
<     *);
<   end AdminPassword;
< 
<   operation SetAdminPassword is
<     inputs: info:ChangePasswordInfo, aws:AdminWorkSpace;
<     outputs: aws':AdminWorkSpace;
<     description: (*
<         Set the administrator password in the given workspace to the
<         information in the given ChangePasswordInfo.
<     *);
<     precondition:
<         Encrypt(info.current) = aws.password and
<         info.new = info.new_reentered;
<     postcondition:
<         aws' ~= aws except (aws'.password = Encrypt(info.new));
<   end SetAdminPassword;
< 
<   function Encrypt(s:string)->ep:EncryptedString
<     description: (*
<         Encrypt the given password string, using a suitable encryption
<         technique.  There are no specific requirements on the strength of the
<         encryption.
<     *);
<   end;
< 
<   object AdminEmailAddress is string
<     description: (*
<        Administrator email address.
<     *);
<   end AdminEmailAddress;
< 
<   operation SetAdminEmailAddress is
<     inputs: aea:AdminEmailAddress, aws:AdminWorkSpace;
<     outputs: aws':AdminWorkSpace;
<     description: (*
<         Set the admin email address in the given workspace.
<     *);
<     precondition: ValidateEmailAddress(aea);
<     postcondition: aws' ~= aws except (aws'.email = aea);
<   end SetAdminEmailAddress;
< 
<   function ValidateEmailAddress(AdminEmailAddress)->boolean
<     description: (*
<         Perform whatever form of email address validation is available in a
<         given operating environment.
<     *);
<   end ValidateEmailAddress;
< 
<   object UserNotification is
<     components: message:NotificationMessage and deliver_how:DeliverHow;
<     description: (*
<        The UserNotfiation contains a notifcation message text and an indication
<        of how to deliver the notification -- on-screen and/or via email.
<     *);
<   end NotificationMessage;
< 
<   object NotificationMessage is string
<     description: (*
<        A notification message is a free-form text string.
<     *);
<   end NotificationMessage;
< 
<   object DeliverHow is
<     components: screen:OnScreen and email:ViaEmail;
<     description: (*
< 
<     *);
<   end DeliverHow;
< 
<   object OnScreen is boolean
<     description: (*
<        Deliver a notification on the screen of every user.
<     *);
<   end OnScreeen;
< 
<   object ViaEmail is boolean
<     description: (*
<        Deliver a notification via email to every user.
<     *);
<   end ViaEmail;
< 
<   operation NotifyUsers is
<     inputs: udb:UserDB (* net:Network *), un:UserNotification;
<     outputs: udb':UserDB (*, net':Network *);
<     description: (*
<         Deliver a notification on-screen and/or via email to every user.  For
<         on-screen notification, put the message in the host notification queue
<         for each user, for access from local computers via a pull (blah, blah,
<         blah, including non-necessity for a Network parm).  For email
<         notifications, send them immediately.
<     *);
<     precondition: ;
<     postcondition:
< 
<         forall (ur in udb)
< 
<             (if un.deliver_how.screen
<              then
<                 exists (ur' in udb')
<                     ur' ~= ur except
<                         (ur'.notification_queue =
<                             ur.notification_queue + un.message)
<                     and
<                 #udb' = #udb)
< 
<                 and
< 
<             (if un.deliver_how.email
<              then
<                 SendEmail(ur.email, un.message));
< 
<   end NotifyUsers;
< 
<   function SendEmail(addr:EmailAddress, nm:NotificationMessage) -> boolean
<     description: (*
<         Using a mailing agent of the underlying operating environment, send an
<         email message to the given EmailAddress, with a body containing the
<         given NotificationMessage.  The return value of the function is
<         intended to be an indication of the success or failure of the mail
<         delivery, but a return value of always true is acceptable if necessary.
<     *);
<   end SendEmail;
< 
< 
<   (**
<    * Objects and operations for regular-user admin commands.
<    *)
< 
<