object Monday
    description: (* One of the seven days of the week. *);
  end;

  object Tuesday
    description: (* One of the seven days of the week. *);
  end;

  object Wednesday
    description: (* One of the seven days of the week. *);
  end;

  object Thursday
    description: (* One of the seven days of the week. *);
  end;

  object Friday
    description: (* One of the seven days of the week. *);
  end;

  object Saturday
    description: (* One of the seven days of the week. *);
  end;

  object MonthName = jan:January or feb:February or mar:March or apr:April or
        may:May or jun:June or jul:July or aug:August or sep:September or
        oct:October or nov:November or dec:December
    description: (*
        The twelve months of the year.
    *);
  end MonthName;

  object January
    description: (* One of the twelve months of the year. *);
  end;

  object February
    description: (* One of the twelve months of the year. *);
  end;

  object March
    description: (* One of the twelve months of the year. *);
  end;

  object April
    description: (* One of the twelve months of the year. *);
  end;

  object May
    description: (* One of the twelve months of the year. *);
  end;

  object June
    description: (* One of the twelve months of the year. *);
  end;

  object July
    description: (* One of the twelve months of the year. *);
  end;

  object August
    description: (* One of the twelve months of the year. *);
  end;

  object September
    description: (* One of the twelve months of the year. *);
  end;

  object October
    description: (* One of the twelve months of the year. *);
  end;

  object November
    description: (* One of the twelve months of the year. *);
  end;

  object December
    description: (* One of the twelve months of the year. *);
  end;

  object Year = integer
    description: (*
        The four-digit year number.  (Yes, this Calendar Tool has a Y10K
        problem.)
    *);
  end Year;

  object StartTime = Time
    description: (*
        StartTime is the starting time of a scheduled appointment or meeting.
    *);
  end StartTime;

  object DueTime = Time
    description: (*
        DueTime is the time a task is due.
    *);
  end StartTime;

  object Duration
    components: hours:Hours and minutes:Minutes;
    description: (*
        Duration is the time length of a scheduled item, in hours and minutes.
        The minimum duration value is 1 minute.  The maximum is 999 hours.
    *);
  end Duration;

  object Hours = integer
    description: (*
        Hours component of a scheduled item duration, between 0 and 999.
    *);
  end;

  object Minutes = integer
    description: (*
        Minutes component of a scheduled item duration, between 0 and 60*999.
    *);
  end;

  object Time = hour:Hour and minute:Minute and am_or_pm:AmOrPm
    description: (*
        A Time consists of an hour, minute, and AM or PM indicator.  A time
        value is expressed using a 12-hour or 24-hour clock style.  The clock
        style is set as an option by the user.  If the clock style is 24-hour,
        the AmOrPm indicator is nil.
    *);
  end Time;

  object Hour = integer
    description: (*
        The hour component of a time value, between 1 and 12 or 0 and 24 based
        on the clock style in use.  
    *);
  end Hour;

  object Minute = integer
    description: (*
        The minute component of a time value, between 0 and 59.
    *);
  end Minute;

  object AmOrPm = AM or PM
    description: (*
        Standard suffix used in 12-hour time value.
    *);
  end AmOrPm;

  object AM
    description: (* The 12-hour time suffix indicating a morning time. *);
  end;

  object PM
    description: (* The 12-hour time suffix indicating an afternoon time. *);
  end;

  (**
   * Something's gotta get fixed in this vicinity given that recurring
   * information is different for Meetings versus MeetingRequests.
   *)
  object RecurringInfo
    components: is_recurring:IsRecurring and interval:Interval and
        details:IntervalDetails;
    description: (*
        RecurringInfo has components to specify the nature of a recurring item.
        IsRecurring is an on/off flag that indicates whether an item recurs.
        Interval is one of Weekly, Biweekly, Monthly, or Yearly.  The
        IntervalDetails component defines the precise means to define
        recurrence for the different interval levels.
    *);
  end RecurringInfo;

  object IsRecurring = boolean
    description: (*
        True of a scheduled item is recurring.
    *);
  end IsRecuring;

  object Interval
    components: weekly:Weekly or biweekly:Biweekly or monthly:Monthly or
        yearly:Yearly;
    description: (*
        Interval specifies the granularity at which recurring items are
        defined.  The Weekly and Biweekly settings allow the user to specify
        recurrence on one or more days of the week.  The Monthly setting allows
        the user to specify recurrence on one or more days in one or more weeks
        of each month.  The Yearly setting allows the user to specify
        recurrence on one or more specific dates in the year.
    *);
  end Interval;

  object Weekly
    description: (* Indicates a scheduled item recurs weekly. *);
  end;

  object Biweekly
    description: (* Indicates a scheduled item recurs bi-weekly. *);
  end;

  object Monthly
    description: (* Indicates a scheduled item recurs monthly. *);
  end;

  object Yearly
    description: (* Indicates a scheduled item recurs yearly. *);
  end;

  object IntervalDetails
    components: weekly:WeeklyDetails or monthly:MonthlyDetails;
    description: (*
        IntervalDetails are either weekly or monthly.
    *);
  end IntervalDetails;

  object WeeklyDetails
    components: sun:OnSun and mon:OnMon and tue:OnTue and wed:OnWed and
        thu:OnThu and fri:OnFri and sat:OnSat;
    description: (*
        WeeklyDetails has an on/off setting for each day of the week on which
        an item recurs.  These details are also used for the BiWeekly setting
        of the recurrence interval.
    *);
  end WeeklyDetails;

  object MonthlyDetails
    components: MonthlyDayDetails or MonthlyDateDetails;
    description: (*
        MonthlyDetails can be specified on a day-of-the-week basis or on
        specific date(s) basis.  The two components contain the specific
        details for these two types of settings.
    *);
  end MonthlyDetails;

  object MonthlyDayDetails
    components: FirstWeekDetails and SecondWeekDetails and ThirdWeekDetails and
        FourthWeekDetails and FifthWeekDetails and LastWeekDetails;
    description: (*
        MonthlyDayDetails contains a weekly details component for each possible
        week of a month.  The First- through ThirdWeekDetails are distinct for
        all possible months.  Depending on the configuration of a particular
        month in a particular year, there is potential conflict in specifying
        recurrence in the fourth, fifth, or last weeks.  The conflicts are
        resolved as follows:
                                                                            <p>
        For months with 4 weeks only, the settings in FifthWeekDetails do not
        apply, and the settings in LastWeekDetails, if present, override any
        settings in FourthWeekDetails.  For months with 5 weeks only, the
        settings in LastWeekDetails, if present, override any settings in
        FifthWeekDetails.  (For months with 6 weeks, the LastWeekDetails
        component applies to the 6th week, and there are no conflicts.)
    *);
  end MonthlyDayDetails;

  object MonthlyDateDetails
    components: DateNumber*;
    description: (*
        MonthlyDateDetails is a list of zero or more specific dates in a month
        on which an item recurs.
    *);
  end MonthlyDateDetails;

  object DateNumber = integer
    description: (*
        The numeric value of the date in a month, between 1 and 31.
    *);
  end DateNumber;

  object OnSun = boolean
    description: (* Indicates that an item recurs on Sunday. *);
  end;

  object OnMon = boolean
    description: (* Indicates that an item recurs on Monday. *);
  end;

  object OnTue = boolean
    description: (* Indicates that an item recurs on Tuesday. *);
  end;

  object OnWed = boolean
    description: (* Indicates that an item recurs on Wednesday. *);
  end;

  object OnThu = boolean
    description: (* Indicates that an item recurs on Thursday. *);
  end;

  object OnFri = boolean
    description: (* Indicates that an item recurs on Friday. *);
  end;

  object OnSat = boolean
    description: (* Indicates that an item recurs on Saturday. *);
  end;


  object FirstWeekDetails = WeeklyDetails
    description: (*
        Scheduling details for the first week of a month.
    *);
  end;

  object SecondWeekDetails = WeeklyDetails
    description: (*
        Scheduling details for the second week of a month.
    *);
  end;

  object ThirdWeekDetails = WeeklyDetails
    description: (*
        Scheduling details for the third week of a month.
    *);
  end;

  object FourthWeekDetails = WeeklyDetails
    description: (*
        Scheduling details for the fourth week of a month.
    *);
  end;

  object FifthWeekDetails = WeeklyDetails
    description: (*
        Scheduling details for the fifth week of a month.
    *);
  end;

  object LastWeekDetails = WeeklyDetails
    description: (*
        Scheduling details for the last week of a month.
    *);
  end;

  object RecurringId = integer
    description: (*
        RecurringId is the unique identifier shared by all instances of a
        recurring item or multi-day event.  When a recurring item is scheduled,
        a collection of separate instances is created for each recurrence.
        When an instance is subsequently changed, the system may need to access
        all other instances in the collection.  The RecurringId is used for
        this purpose.  Viz., all instances in the same recurring collection
        have the same value for RecurringId.  Recurring Id is used in the same
        way for the multiple days of a multi-day event.
                                                                            <p>
        Using an integer representation for RecurringId is reasonable, since
        the exact representation is not directly visible to the user.  From the
        user's perspective, the requirements say that "the system keeps track
        of instance collections as a whole, for the purposes of change and
        delete."  In this sense, a simple integer tag is a perfectly fine
        representation.
    *);
  end RecurringId;

  object Category
    components: name:Name and color:StandardColor;
    description: (*
        A Category has a Name and StandardColor, which serve to distinguish it
        from other categories.  Colored-coded categories serve as visual cues
        to the user when viewing lists of scheduled items in some form.
        Categories can also be used in filtered viewing.
    *);
  end Category;

  object StandardColor
    components: Black or Brown or Red or Orange or Yellow or Green or Blue or
        Purple;
    description: (*
        A StandardColor is one of a fixed set of possibilities.
    *);
  end StandardColor;

  object Black
    description: (* One of the built-in category colors. *);
  end;

  object Brown
    description: (* One of the built-in category colors. *);
  end;

  object Red
    description: (* One of the built-in category colors. *);
  end;

  object Orange
    description: (* One of the built-in category colors. *);
  end;

  object Yellow
    description: (* One of the built-in category colors. *);
  end;

  object Green
    description: (* One of the built-in category colors. *);
  end;

  object Blue
    description: (* One of the built-in category colors. *);
  end;

  object Purple
    description: (* One of the built-in category colors. *);
  end;

  object Location = string
    description: (*
        Location is a free-form string indicating in what physical location an
        item is scheduled.
    *);
  end Location;

  object Security
    components: Public or TitleOnly or Confidential or Private;
    description: (*
        Security is one of four possible levels, from Public to Private.  The
        levels specify the degree of visibility an appointment or meeting has
        to other users.
    *);
  end Security;

  object Public
    description: (*
        Public security means other users can see the scheduled item and all of
        its component information.
    *);
  end Public;

  object TitleOnly
    description: (*
        TitleOnly security means other users can see title, time, and date
        components only.  TitleOnly security applies only to appointments and
        meetings.
    *);
  end Public;

  object Confidential
    description: (*
        Confidential security means other users can only see that a user is
        unavailable for the time period of a scheduled item; no other
        information about the scheduled item is visible.  Confidential security
        applies only to appointments and meetings.
    *);
  end;

  object Private
    description: (*
        Private security means other users see no information at all about a
        scheduled item, not even that the item is scheduled.  Note that private
        security hides a scheduled item from the ScheduleMeeting operation,
        q.v., so that a meeting may be scheduled at the same time as a private
        appointment.  It is up to the user to handle this situation by
        accepting or refusing the scheduled meeting.
    *);
  end;

  object SimpleSecurity
    components: Public or Private;
    description: (*
        Simple security has only two levels -- public or private.  It applies
        to tasks and events.  Cf. Security.
    *);
  end SimpleSecurity;

  object Priority
    components: Must or Optional;
    description: (*
        Priority indicates whether an appointment is a must or if it is
        optional.  This information is used to indicate the general importance
        of an appointment to the user.  The operational use of Priority is in
        the ScheduleMeeting operation, where the meeting scheduler can elect to
        consider optional appointments as allowable times for a meeting.
    *);
  end Priority;

  object Must = "Must"
    description: (*
        Indicates a scheduled item is 'Must' priority.
    *);
  end;

  object Optional
    description: (*
        Indicates a scheduled item is 'Optional' priority.
    *);
  end;

  object TaskPriority = integer
    description: (*
        A TaskPriority is a positive integer that defines the priority of one
        task relative to others.  The priority value range is 0 to 10, with a
        higher value indicating a higher priority.
    *);
  end TaskPriority;

  axiom TaskPriorityNonNegative = forall (tp: TaskPriority) tp >= 0;

  object RemindInfo
    components: IsReminded and RemindWhen and RemindWhere;
    description: (*
        RemindInfo defines if, when, and where a scheduled item reminder is
        sent to the user.
    *);
  end RemindInfo;

  object IsReminded = boolean
    description: (*
        True of a reminder is to be sent for a scheduled item.
    *);
  end IsReminded;

  object RemindWhen
    components: integer and ReminderTimeUnit;
    description: (*
        RemindWhen defines how soon before a scheduled item the reminder is to
        be sent.  The time units are minutes, hours, or days.
    *);
  end RemindInfo;

  object ReminderTimeUnit
    components: MinutesBefore or HoursBefore or DaysBefore;
    description: (*
        Reminders can come minutes, hours, or days before the start time of a
        scheduled item.
    *);
  end ReminderTimeUnits;

  object MinutesBefore
    description: (*
        Indicates that a reminder occurs a specified number of minutes before a
        scheduled item.
    *);
  end MinutesBefore;

  object HoursBefore
    description: (*
        Indicates that a reminder occurs a specified number of hours before a
        scheduled item.
    *);
  end HoursBefore;

  object DaysBefore = real
    description: (*
        Indicates that a reminder occurs a specified number of days before a
        scheduled item.
    *);
  end DaysBefore;

  object RemindWhere = OnScreen or BeepOnly or Email
    description: (*
        RemindWhere defines one of three ways that the user is alerted when a
        scheduled event is to occur.  OnScreen means the user is reminded with
        a pop-up alert on her computer screen.  BeepOnly means the user
        reminded with a simple audible tone on the computer.  Email means the
        user is sent an electronic mail message reminder.
    *);
  end RemindWhere;

  object OnScreen
    description: (*
        Indicates that reminders are displayed in an on-screen pop-up window.
    *);
  end OnScreen;

  object BeepOnly
    description: (*
        Indicates that reminders are signaled with an audible beep only, with
        no pop-up window.
    *);
  end BeepOnly;

  object Email
    description: (*
        Indicates that reminders are send as email messages.
    *);
  end Email;  

  object Details = string
    description: (*
        Details is a plain text string describing any details about a scheduled
        item the user may care to add.
    *);
  end Details;

  object Attendees
    components: Name*;
    description: (*
        Attendees is a list of names of those who attend a meeting.
    *);
  end Attendees;

  object Name = string
    description: (*
        The name of a category or a meeting attendee.
    *);
  end;

  object MeetingMinutesLocation = string
    description: (*
        MeetingMinutes is a plain text string that records the file or URL
        location of the minutes taken for a meeting.  The syntax of the
        location string is presumed to be compatible with the program that is
        used to view meeting minutes, as specified in the system options.  This
        syntax has no specific meaning to the Calendar Tool.
    *);
  end MeetingMinutes;

  object ScheduledBy = UserId
    description: (*
       ScheduledBy is the id of user who scheduled the meeting, i.e., the user
       who executed the ScheduleMeeting operation that led to the meeting being
       scheduled.
    *);
  end ScheduledBy;

  object ScheduledOn
    components: Date and Time;
    description: (*
       ScheduledOn is the date and time on which a meeting is scheduled.
    *);
  end ScheduledOn;

  object FieldEditDates
    components: FieldEditDate*;
    description: (*
       List of dates for meeting fields that have been editied since the last
       time the meeting was saved.
    *);
  end FieldEditDates;

  object FieldEditDate
    components: FieldName and Date;
    description: (*
       A FieldEditDate is the name of a meeting field and the date it was last
       edited.  This information is used to merge the changes made
       independently by the scheduler and attendee of a meeting.  The policy
       is to merge changes, such that the merge value for each field is the
       value most recently edited by either the scheduler or attendee.
    *);
  end FieldEditDate;

  object FieldName = string
    description: (*
        The string name of a meeting field.
    *);
  end;

  object CompletedFlag = boolean
    description: (*
        CompletedFlag is true if a Task has been completed, false if not.  The
        system does not enforce any specific constraints on the setting of a
        task's CompletedFlag.  That is, the user may set or clear it at will.
        Hence the meaning of the CompletedFlag is subject to user
        interpretation, particularly for recurring tasks.
    *);
  end CompletionDate;

  object CompletionDate
    components: Date;
    description: (*
        CompletionDate is date on which as task is completed.  The system does
        not enforce any specific constraints on the setting of a task's
        CompletionDate (other than it being a legal Date value).  The meaning
        of the CompletionDate value is up to user interpretation, particularly
        for recurring tasks.
    *);
  end CompletionDate;

  operation ScheduleAppointment
    inputs: cdb:CalendarDB, appt:Appointment;
    outputs: cdb':CalendarDB;
    description: (*
        ScheduleAppointment adds the given Appointment to the current Calendar
        in the UserWorkSpace of the given CalendarDB.  In the case of a
        recurring appointment, a separate appointment instance is added per
        the recurring information.
                                                                           <p>
        The addition is only made if an appointment of the same time, duration,
        and title is not already scheduled.  In the case of a recurring
        appointment, this means that none of recurring instances to be added
        can have the same time, duration, and title as an already scheduled
        appointment.
                                                                           <p>
        If the addition is made, the RequiresSaving flag of the calendar is set
        to true.
    *);
    precondition: 
        (*
         * The StartOrDueDate field is not empty and a valid date value.
         *)
        (appt.start_or_due_date != nil) and DateIsValid(appt.start_or_due_date)

            and

        (*
         * If non-empty, the EndDate field is a valid date value.
         *)
        (appt.end_date != nil) or DateIsValid(appt.end_date)

            and

        (*
         * The duration is between 1 minute and 999 hours, inclusive.
         *)
        DurationInRange(appt.duration)

            and

        (*
         * If weekly recurring is selected, at least one of the day checkboxes
         * must be selected.
         *)
        if appt.recurring.is_recurring and appt.recurring.interval?.weekly
        then appt.recurring.details.weekly.sun or
             appt.recurring.details.weekly.mon or
             appt.recurring.details.weekly.tue or
             appt.recurring.details.weekly.wed or
             appt.recurring.details.weekly.thu or
             appt.recurring.details.weekly.fri or
             appt.recurring.details.weekly.sat

            and

        (*
         * No appointment or meeting extends the same StartTime, Duration,
         * and Title is in the current workspace calendar of the given
         * CalendarDB.  The current calendar is
         *
         *     cdb.workspace.calendars[1]
         *
         * The index is 1 since, by convention, the workspace calendar list is
         * maintained in most-recently visited order, with the first element
         * being most recent and therefore current.
         *)
        not (exists (item in cdb.workspace.calendars[1].items)
            (item.start_or_due_date = appt.start_or_due_date) and
            (item.<Appointment.duration = appt.duration) and
            (item.title = appt.title))
        ;
    postcondition:
        (*
         * A scheduled item is in the output calendar if and only if it is the
         * new appointment to be added or it is in the input calendar.  As
         * noted in the precond, the current calendar is
         *
         *     DB.workspace.calendars[1]
         *
         * where here in the postcond, DB is either cdb or cdb'.
         *)
        -- NOTE: This must be updated to reflect separate instances being added
        -- for recurring appointments.
        (forall (item:ScheduledItem)
            (item in cdb'.workspace.calendars[1].items) iff
                ((item.<Appointment = appt) or
                 (item in cdb'.workspace.calendars[1].items)))

            and

        (cdb'.workspace.calendars[1].requires_saving = true);

  end ScheduleAppointment;

  operation ScheduleMeeting
    inputs: CalendarDB, MeetingRequest;
    outputs: CalendarDB;
    components: ListMeetingTimes, SetMeetingOptions, ConfirmMeeting;
    description: (*
        ScheduleMeeting adds a Meeting to the current Calendar in the
        UserWorkSpace of the given CalendarDB, based on the the given
        MeetingRequest.  The work is done by the three suboperations, which
        determine a list of possible meetings times, set meeting-scheduling
        options, and confirm the scheduling of a specific meeting selected from
        the possibles list. *);
    precondition: (* User must be group leader *);
    postcondition: ;
  end ScheduleMeeting;

  (**
   * Something's gotta get fixed in this vicinity given that recurring
   * information is different for Meetings versus MeettingRequests.  In order
   * for a where clause sub of RecurringInfo to work, we gotta do some work to
   * distinguish recurring info for meetings versus meeting requests.
   *)
  object MeetingRequest extends Meeting
    where: StartDate = EarliestStartDate, EndDate=LatestEndDate,
        StartTime=EarliestStartTime;
    components: LatestStartDate and LatestEndDate and LatestStartTime;
    description: (*
        A meeting request has all the components of a meeting plus three
        additional components to specify the latest dates and time at which the
        meeting can be scheduled.  A meeting request is used to specify a range
        of possible meeting times, to allow scheduling alternatives to be
        considered.  The description of the ScheduleMeeting operation has
        further details on how meeting requests are handled.
    *);
  end MeetingRequest;

  object EarliestStartDate = Date
    description: (*
        In a meeting request, the earliest possible start date for the meeting
        to be scheduled.
    *);
  end;

  object LatestStartDate = Date
    description: (*
        In a meeting request, the latest possible start date for the meeting to
        be scheduled.
    *);
  end;

  object EarliestEndDate = Date
    description: (*
        In a meeting request, the earliest possible end date for a recurring
        meeting to be scheduled.
    *);
  end;

  object LatestEndDate = Date
    description: (*
        In a meeting request, the latest possible end date for a recurring
        meeting to be scheduled.
    *);
  end;

  object EarliestStartTime = Time
    description: (*
        In a meeting request, the earliest possible start time for the meeting
        to be scheduled.
    *);
  end;

  object LatestStartTime = Time
    description: (*
        In a meeting request, the latest possible start time for the meeting to
        be scheduled.
    *);
  end;

  object PossibleMeetingTimes = (StartTime and Date)*;

  operation ListMeetingTimes
    inputs: CalendarDB, MeetingRequest;
    outputs: PossibleMeetingTimes;
    description: (*
        Produce the list of possible meeting times that satisfy the given
        MeetingRequest.
    *);
  end;

  operation SetMeetingOptions
    inputs: CalendarDB, MeetingSchedulingOptions;
    outputs: CalendarDB;
    description: (*
        Set the meeting scheduling options in the given CalendarDB to those
        given.
    *);
  end;

  object MeetingSchedulingOptions
    components: DaysPerWeek and AllowableDays and MinDaysBetween and
        MaxDaysBetweeen;
  end;

  object DaysPerWeek = integer
    description: (*
       
    *);
  end DaysPerWeek;

  object AllowableDays = WeeklyDetails
    description: (*
       
    *);
  end AllowableDays;

  object MinDaysBetween = integer;

  object MaxDaysBetweeen = integer;

  operation ConfirmMeeting
    inputs: CalendarDB, MeetingRequest, PossibleMeetingTimes, SelectedTime;
    outputs: CalendarDB;
    description: (*
        ConfirmMeeting takes a CalendarDB, MeetingRequest, list of
        PossibleMeetingTimes, and a Selected time from the list.  It outputs a
        new CalendarDB with the given request scheduled at the selected time.
        Further details of output constraints are forthcoming.
    *);
    precondition: ;
    postcondition: ;
  end ConfirmMeeting;

  object SelectedTime = integer;

  operation ScheduleTask
    inputs: CalendarDB, Task;
    outputs: ;
    description: (*
        ScheduleTask adds the given Task to the given CalendarDB, if a task of
        the same time, duration, and title is not already scheduled.
    *);
    precondition: ;
    postcondition: ;
  end ScheduleTask;

  operation ScheduleEvent
    inputs: cdb:CalendarDB, e:Event;
    outputs: cdb':CalendarDB;
    description: (*
        ScheduleEvent adds the given Event to the given CalendarDB, if an event
        of the same start date and title is not already scheduled.
    *);
    precondition: 
        (*
         * The Title field is at least one character long.
         *)
        (#(e.title) >= 1)

            and

        (*
         * The StartOrDueDate field is not empty and a valid date value.
         *)
        (e.start_or_due_date != nil) and DateIsValid(e.start_or_due_date)

            and

        (*
         * If non-empty, the EndDate field is a valid date value.
         *)
        (e.end_date != nil) or DateIsValid(e.end_date)

            and

        (*
         * The current workspace is not nil.
         *)
        (cdb.workspace.calendars != nil)

            and

        (*
         * No event of same StartDate and Title is in the current workspace
         * calendar of the given CalendarDB.  The current calendar is
         *
         *     cdb.workspace.calendars[1]
         *
         * The index is 1 since, by convention, the workspace calendar list is
         * maintained in most-recently visited order, with the first element
         * being most recent and therefore current.
         *)
        not (exists (item in cdb.workspace.calendars[1].items)
            (item.start_or_due_date = e.start_or_due_date) and
            (item.title = e.title))
        ;
    postcondition:
        (*
         * A scheduled item is in the output calendar if and only if it is the
         * new event to be added or it is in the input calendar.  As noted in
         * the precond, the current calendar is
         *
         *     DB.workspace.calendars[1]
         *
         * where here in the postcond, DB is either cdb or cdb'.
         *)
        (forall (item:ScheduledItem)
            (item in cdb'.workspace.calendars[1].items) iff
                ((item.<Event = e) or
                 (item in cdb'.workspace.calendars[1].items)))

            and

        (cdb'.workspace.calendars[1].requires_saving = true);
  end ScheduleEvent;


  (* NOTE: We need to separate ChangeItem into ChangeAppointment, etc., since
   *       the pre and postconds need to be specialized for each. *)
  operation ChangeItem
    inputs: cdb:CalendarDB, si_old:ScheduledItem, si_new:ScheduledItem;
    outputs:  cdb':CalendarDB;
    description: (*
        ChangeItem changes the given old item to the given new item in the
        current calendar of the given CalendarDB.
    *);
    precondition: ;
    postcondition: ;
  end ChangeItem;

  operation DeleteItem
    inputs: cdb:CalendarDB, si:ScheduledItem;
    outputs: cdb':CalendarDB;
    description: (*
        DeleteItem deletes the given item from the current calendar of the
        given CalendarDB.
    *);
    precondition: ;
    postcondition: ;
  end DeleteItem;


  (**
   * Auxiliary functions.
   *)
  function DateIsValid(date:Date)->boolean = (

    (*
     * The date number is between one and the proper month-specific upper
     * bound.
     *)
    (date.number >= 1) and DateNumUpperBoundIsValid(
        date.number, date.month, date.year)

        and

    (*
     * The year is between 1 and 9999.
     *)
    (date.year >= 1) and (date.year <= 9999);

    )
    description: (*
        Auxiliary function that specifies date validity.
    *);
  end;

  function DateNumUpperBoundIsValid(num:DateNumber, month:MonthName,
        year:Year)->boolean = (

    (*
     * 30 days has September, and all that ... .
     *)

    (*
     * Upper bound for jan, mar, may, jul,aug, oct, and dec is 31 days.
     *)
    if (month?.jan or month?.mar or month?.may or month?.jul or month?.aug or
        month?.oct or month?.dec)
    then num <= 31
    else

        (*
         * Upper bound for apr, jun, sep, and nov is 30 days.
         *)
        if (month?.apr or month?.jun or month?.sep or month?.nov)
        then num <= 30
        else (* Month is feb *)

            (*
             * Upper bound for feb is 29 if leap year, 28 if not.
             *)
            if IsLeapYear(year)
            then num <= 29
            else num <= 28;
    )
    description: (*
        Auxiliary function that specifies valid upper bound for day number 
        component of a date.
    *);
  end;

  function IsLeapYear(year:Year)->boolean = (

    (year mod 4 = 0) and ((year mod 100 = 0) implies (year mod 400 = 0)))

    description: (*
        Auxiliary function that specifies leap year definition, viz., the year
        is divisible by 4, and if it's divisible by 100 then it's also
        divisible 400.
    *);
  end;

  function DurationInRange(duration:Duration)->boolean = (

    (*
     * Both the hours and minutes fields must be non-negative.
     *)
    (duration.hours > 0) and (duration.minutes > 0)

        and

    (*
     * The maximum duration is 999 hours.
     *)
    (duration.hours + duration.minutes/60 <= 999);

    (*
     * Note that there is no specific upper bound on the minutes field.
     *)

    )
    description: (*
        Auxiliary function that specifies range criteria for the duration of a
        scheduled item.
    *);
  end;


  (**
   * Category-related objects and operations.
   *)
  object Categories
    components: Category*;
    description: (*
       
    *);
  end CategoryList;

  operation AddCategory
    inputs: cs:Categories, c:Category;
    outputs: cs':Categories;
    description: (*
        AddCategory adds the given Category to the given Categories.  No
        category of the same name can be in the list already.  Category names
        are compared on a character-by-character, case sensitive basis.
    *);

    precondition:
        not (exists (c' in cs) (c'.name = c.name));

    postcondition:
        forall (c':Category)
            (c' in cs') iff (c' in cs) or (c' = c);

  end AddCategory;

  operation ChangeCategory
    inputs: cs:Categories, old_cat:Category, new_cat:Category;
    outputs: cs':Categories;
    description: (*
        ChangeCategory replaces the given old Category with the given new
        Cateogry in the given Cateogries.
    *);
    precondition: ;
    postcondition: ;
  end ChangeCategory;

  operation DeleteCategory
    inputs: cs:Categories, n:Name;
    outputs: cs':Categories;
    description: (*
        DeleteCategory removes the category of the give name from the given
        Categories.
    *);
    precondition: ;
    postcondition: ;
  end ChangeCategory;

  operation OK
    inputs: cdb:CalendarDB, appt:Appointment;
    outputs: cdb':CalendarDB;
    description: (*
        Simply invoke ScheduleAppointment.  This operation is unnecessary in
        the model unless we want to model the enable/disable state of the OK
        button using a precondition.  At present, we do not.  I.e., we model
        the appointment scheduling preconds only in ScheduleAppointment itself,
        which allows for non-incremental implementation of precondition
        checking.
    *);
    precondition: ;
    postcondition: cdb' = ScheduleAppointment(cdb, appt);
  end OK;

  operation Clear
    inputs: old_appt:Appointment, new_appt:Appointment, cdb:CalendarDB;
    outputs: appt':Appointment;
    description: (*
        If the given old and new appointments differ, output an appointment
        object that contains the default values defined in the given
        CalendarDB.
    *);
    precondition: old_appt != new_appt;
    postcondition:
        appt' = cdb.workspace.calendars[1].settings.options.sched.defaults.appt;
  end Clear;

end Schedule;