(**** * * Module Admin defines the objects and operations related to maintaining the * 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. *) module Admin; import Schedule.ScheduledItem, Schedule.Title, Schedule.StartTime, Schedule.Duration, Schedule.StartOrDueDate, Schedule.EndDate, Schedule.WeeklyDetails; import CalendarDB.AdminWorkSpace, CalendarDB.UserCalendar; import MultiUserEnvir.Server, MultiUserEnvir.HostId, MultiUserEnvir.ScheduledToStopIn, MultiUserEnvir.ConnectedUsers, MultiUserEnvir.Network, MultiUserEnvir.NotificationQueue; import File.File, File.FileSize; export UserDB, GroupDB, LocationDB, UserId, AdminPassword, AdminEmailAddress, IsRunning, NotificationMessage; 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:UserName and id:UserId and password:UserPassword and email:EmailAddress and phone:Phone and limit:CalendarSizeLimit and notification_queue:NotificationQueue; description: (* A UserRecord is the information stored about a registered user of the 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 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. 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. *); end UserRecord; object UserName = last:LastName and first:FirstName and middle:MiddleName description: (* The name of a registered user. *); end; object LastName = string description: (* User last name. This component of the user name is required; first and middle are optional. *); end LastName; object FirstName = string description: (* Optional first name in a user record. *); end FirstName; object MiddleName = string description: (* Optional middle name in a user record. *); end MiddleName; object UserId = string description: (* The unique id of a registered Calendar Tool user. *); end; object EmailAddress = string description: (* The electronic mail address of a registered user. *); end; object Phone = area:Area and number:Number description: (* A phone number consists of a three-digit area code and seven-digit number. *); end; object Area = integer description: (* The three-digit area code component of a user phone number. *); end Area; object Number = integer description: (* The seven-digit number component of a user phone number. *); end Number; object HostComputer = 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 = string description: (* The user's identification on the host computer. *); end ComputerUserID; object HomeDirectory = string description: (* The file directory (i.e., folder) assigned as the user's home directory on the host computer. *); end HomeDirectory; object CalendarSizeLimit = 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 = EncryptedString description: (* The user password. *); end AdminPassword; object EncryptedString = string description: (* 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. *); end EncryptedString; 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 SearchByName inputs: udb:UserDB, n:UserName; outputs: url:UserRecord*; description: (* Search for a user or users by name. If more than one is found, the output list is sorted by id. *); precondition: ; postcondition: (* * A record is in the output list if and only it is in the input UserDB * and the record name equals the UserName being searched for. *) (forall (ur: UserRecord) (ur in url) iff (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 SearchByName; operation SearchById inputs: udb:UserDB, id:UserId; outputs: ur':UserRecord; description: (* Search for 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 SearchById; operation ChangeUser inputs: udb:UserDB, uc:UserCalendar, old_ur:UserRecord, new_ur:UserRecord; outputs: udb':UserDB, uc':UserCalendar, cscn:CalendarSizeChangeNotification; 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. 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.

If the user record id is changed, then change all occurrences of the 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. *); 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 (* * 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 (* * 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 changed 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_ur.limit * 1000000 > uc.file.size then uc' = ChangeCalendarSize(uc); end ChangeUser; 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 = 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; 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 a search 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. *); 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:GroupId) (id in lgw) iff ((#(gr.leaders) = 1) and (gr.leaders[1] = ur.id))); end DeleteUser; object LeaderlessGroupsWarning components: GroupId*; description: (* LeaderlessGroupsWarning is an secondary output of the Change and DeleteUser operations, indicating the IDs 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:GroupName and id:GroupId and limit:CalendarSizeLimit and members:Members and leaders:Leaders; 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 GroupName = string description: (* The name of a registered group. *); end GroupName; object GroupId = string description: (* The unique id of a registered group. *); end GroupId; object Leaders = UserId* description: (* List of user ids for the zero or more leaders of a group. *); end; object Members = 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 SearchByName 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: (* * A record is in the output list if and only it is in the input GroupDB * and the record name equals the GroupName being searched for. *) (forall (gr: GroupRecord) (gr in grl) iff (gr in gdb) and (gr.name = n)) and (* * The output list is sorted alphabetically by id. *) (forall (i:integer | (i >= 1) and (i < #grl)) grl[i].id < grl[i+1].id); end SearchByName; operation SearchById inputs: gdb:GroupDB, id:GroupId; outputs: gr':GroupRecord; description: (* Search for a group 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 (gr in gdb) (gr.id = id) and (gr' = gr)) or (not (exists (gr in gdb) (gr.id = id)) and (gr' = nil)); end SearchById; 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 a search 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 a search 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:LocationName and num:LocationNumber and bookings:Bookings and remarks: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; object LocationName = 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 = 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 = 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 administrator 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 scheduled item. The Days component is the same as the WeeklyDetails of a recurring item. *); end UnscheduledBooking; object Use = string description: (* The Use of an unscheduled booking is what ever description of the booking the user want to provide. *); end Use; object Days = WeeklyDetails; object StartDate = StartOrDueDate; obj Remarks = string description: (* Remarks are any information the user chooses to enter about a booking. *); end Remarks; operation AddLocation 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 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: (* * A record is in the output list if and only it is in the input * LocationDB and the record name equals the LocationName being * searched for. *) (forall (lr: LocationRecord) (lr in lrl) iff (lr in ldb) and (lr.name = n)) and (* * The output list is sorted alphabetically by id. *) (forall (i:integer | (i >= 1) and (i < #lrl)) lrl[i].num < lrl[i+1].num); end SearchByName; operation SearchByNumber 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 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 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 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 = boolean description: (* True if the server program is running. *); end IsRunning; object NumUsers = integer description: (* Number of users connected to a server. *); end NumUsers; operation CheckHostStatus 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 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 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 = 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 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 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 components: HostGoingDownPart1 and host_id:HostId and HostGoingDownPart2 and confirm:StopServerConfirmation and HostGoingDownPart3; description: (* *); end HostGoingDownMessage; value HostGoingDownPart1 = "The Calendar Tool server on central host " description: (* The first text part of the host-going-down message. *); end HostGoingDownPart1; value HostGoingDownPart2 = "will stop operating in" description: (* The second text part of the host-going-down message. *); end HostGoingDownPart2; value 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 components: HostIsDownPart1 and host_id:HostId and HostIsDownPart2; description: (* *); end HostIsDownMessage; value HostIsDownPart1 = "The Calendar Tool server on central host " description: (* The first text part of the host-is-down message. *); end HostIsDownPart1; value 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 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 = string description: (* The string value that when encrypted must match the current admininstrator password. *); end CurrentPassword; object NewPassword = string description: (* The string value of the new password; *); end NewPassword; object NewPasswordReentered = string description: (* The reentered string value of the new password; *); end NewPasswordReentered; object AdminPassword = EncryptedString description: (* The password used to gain entry to the Calendar Tool administration program. *); end AdminPassword; operation SetAdminPassword 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 = string description: (* Administrator email address. *); end AdminEmailAddress; operation SetAdminEmailAddress 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 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 = string description: (* A notification message is a free-form text string. *); end NotificationMessage; object DeliverHow components: screen:OnScreen and email:ViaEmail; description: (* *); end DeliverHow; object OnScreen = boolean description: (* Deliver a notification on the screen of every user. *); end OnScreeen; object ViaEmail = boolean description: (* Deliver a notification via email to every user. *); end ViaEmail; operation NotifyUsers 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 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. *) end Admin;