(******
******  OBJECTS
******)


object UserCal is
    components: yearList:Year*;
    operations: ;
    description: (*
        A calendar for a user can be broken down into a list of years.
    *);
end UserCal;

object Year is
    components: yr:YearNum, monthList:Month*;
    operations: ;
    description: (*
        As with any calendar, a Year can be broken into twelve months.
    *);
end Year;

object Month is
    components: mon:MonthNum, dayList:Day*;
    operations: ;
    description: (*
        Months are broken down into days.
    *);
end Month;

object Day is
    components: day:DayName, mmddyy:Date,
		daySched:DaySchedule, rem:Remark, daynum:DayNum;
    operations: ;
    description: (*
        The individually scheduled events are stored at the Day level.
        A Day contains a list of all of the ScheduledItems planned 
        for the day.
    *);
end Day;

object DaySchedule is
    components: schedList:ScheduledItemList;
    operations: AddSchedItem, DelSchedItem, EditSchedItem, FindSchedItem;
    description: (*
        A DaySchedule contains a set of items scheduled for a day.
    *);
end DaySchedule;

object MonthNum is number;
object DayName is
    components: Mon or Tue or Wed or Thu or Fri or Sat or Sun;
    operations: ;
    description: (*
        DayName is a string naming the day of a week.
    *);
end DayName;
object Mon = "Monday";
object Tue = "Tuesday";
object Wed = "Wednesday";
object Thu = "Thursday";
object Fri = "Friday";
object Sat = "Saturday";
object Sun = "Sunday";

object YearNum is number;
object DayNum is number;
object Remark is string;

object ScheduledItem is
    components: startTime:Time, endTime:Time, sum:Summary, desc:Description, 
        details:ScheduleDetails;
    operations: ;
    description: (*
        A ScheduledItem contains all of the information pertaining
        to an individual appointment scheduled in a user's calendar.
        The Summary is a brief title description of the ScheduledItem,
        and the Description is a much longer and more detailed decription
        of what is planned.  By letting ScheduledItem contain AlarmInfo
        and ScheduleDetails, it is possible to adjust and customize the 
        behavior of each event.
    *);
end ScheduledItem;

object ScheduledItemList is ScheduledItem*;

object ScheduleDetails is
    components: alarm:AlarmInfo, repeat:RepeatInfo, priv:Privacy;
    operations: ;
    description: (*
        ScheduleDetails contains other miscellaneous ScheduledItem  
        details.  Having AlarmInfo as part of ScheduleDetails allows
        alarm settings to be adjusted individually for scheduled
        appointments. RepeatInfo helps ease scheduling by allowing
        the user to schedule personal events daily, weekly, monthly,
        or yearly.  Privacy is an enumerated type which shows whether
        the scheduled item is public, unavailable, or private.
    *);
end ScheduleDetails;

object RepeatInfo is
    components: timeval:TimeValue, intertimeval:TimeUnit;
    operations: ;
    description: (*
        RepeatInfo provides a convenient way for the user to schedule
        personal appointments repeatedly.  The TimeUnit is an enumerated
        type showing if the ScheduledItem is repeated daily, weekly, monthly 
        or yearly, and the TimeValue represents how many times the user
        would like it repeated.
    *);
end RepeatInfo;

object Privacy is
    components: Public | Unavailable | Private;
    description: (*
        Privacy is an enumerated type which determines
        whether the scheduled appointment is public, unavailable,
        or private 
    *);
end Privacy;

object Public is
    description: (*
        Public is an opaque type representing a kind of scheduled
        appointment.
    *);
end Public;

object Unavailable is
    description: (*
        Unavailable is an opaque type representing a kind of scheduled
        appointment.
    *);
end Unavailable;

object Private is
    description: (*
        Private is an opaque type representing a kind of scheduled
        appointment.
    *);
end Private;

object Summary is string;
object Description is string;
object TimeValue is number; 
object Active is boolean;

object TimeUnit is
    components: Daily | Weekly | Monthly | Yearly;
    description: (*
        TimeUnit is an enumerated type which determines whether the a 
        calendar view is daily, weekly, monthly, or yearly. 
    *);
end TimeUnit;

object AlarmTimeUnit is
    components: Minutely | Hourly | Daily;
    description: (*
        AlarmTimeUnit is an enumerated type which determines
        whether the TimeValue is in minutes, hours, or days. 
    *);
end AlarmTimeUnit;

object Minutely is
    description: (*
        Minutely is an opaque object representing a unit of time.
    *);
end Minutely;

object Hourly is
    description: (*
        Hourly is an opaque object representing a unit of time.
    *);
end Hourly;

object Daily is
    description: (*
        Daily is an opaque object representing a unit of time.
    *);
end Daily;

object Weekly is
    description: (*
        Weekly is an opaque object representing a unit of time.
    *);
end Weekly;

object Monthly is
    description: (*
        Monthly is an opaque object representing a unit of time.
    *);
end Monthly;

object Yearly is
    description: (*
        Yearly is an opaque object representing a unit of time.
    *);
end Yearly;

object AlarmType is
    components: timeval:TimeValue, unit:AlarmTimeUnit, on:Active;
    operations: ;
    description: (*
        AlarmType contains a time value which is a number representing
        how many time units before an alarm occurs, where a time unit
        is an enumerated type representing minutes, hours, days, etc.
    *);
end AlarmType;

object AlarmInfo is
    components: beepAlarm:AlarmType, flashAlarm:AlarmType,
        popupAlarm:AlarmType, mailAlarm:AlarmType;
    operations: ;
    description: (*
        AlarmInfo contains the various alarms which can be set for
        each scheduled event in a user calendar.
    *);
end AlarmInfo;

object UserOptions is
    components: range:DayBoundaries, defView:TimeUnit, 
        alarm:AlarmInfo, showRem:ShowRemarks;
    operations: ;
    description: (*
        Options contains all of the preferences for the user's
        personal calendar.
    *);
end UserOptions;

object ShowRemarks is boolean;

object DayBoundaries is
    components: startHour:Hour, endHour:Hour;
    operations: ;
    description: (*
        DayBoundaries determines what range of hours appear by default when
        the user is in the day view of his/her calendar.
    *);
end DayBoundaries;


object InitialOptions:UserOptions = [ InitialDayBoundaries, InitialView, 
        InitialAlarmInfo, InitialAddr ] is
    description: (*
        InitialOptions is a predefined object representing what the
        original options are set to for a new user.  A user can also
        choose to restore his or her options to their original defaults.
    *);
end InitialOptions;

object InitialDayBoundaries:DayBoundaries = [ BeginDay, EndDay ] is
    description: (*
        InitialDayBoundaries are the default day boundaries set for
        a new user's options.  A user can also choose to restore his
        or her day boundaries to these original defaults.
    *);
end InitialDayBoundaries;

object BeginDay:Time = [ 7, 0 ] is
    description: (*
        BeginDay represents the default begin time for a day boundary.
    *);
end BeginDay;

object EndDay:Time = [ 19, 0 ] is
    description: (*
        EndDay represents the default end time for a day boundary.
    *);
end EndDay;

object InitialView = Yearly;

object InitialAlarmInfo:AlarmInfo = [ InitialAlarm, InitialAlarm,
        InitialAlarm, InitialAlarm ] is
    description: (*
        InitialAlarmInfo represents the default alarm configuration
        for a user.  All four of the alarm types (beep, flash, popup,
        mail) are set to the same initial condition as described in
        InitialAlarm.
    *);
end InitialAlarmInfo;

object InitialAlarm:AlarmType = [ 10, Minutely, false ] is
    description: (*
        InitialAlarm describes a default alarm type for a user.
        In this case, the alarm is set to go off 10 minutes prior to
        an appointment, but the 'false' indicates the alarm is turned 
        off.  A user can change an alarm setting at any time and for 
        any scheduled event, or he or she can restore an alarm to these 
        initial defaults.
    *);
end InitialAlarm;
        
object PersonalViewMenu is
    components: ;
    operations: ChangeToMonthlyView, ChangeToYearlyView,
                ChangeToWeeklySummary, ChangeToWeeklyModel;
    description: (*
        The PersonalViewMenu lists the calendar view changing
        options available when viewing one's own personal calendar.
    *);
end PersonalViewMenu;

object ViewMenu is
    components: ;
    operations: ChangeToDailyView, ChangeToMonthlyView, ChangeToYearlyView,
                ChangeToWeeklySummary, ChangeToWeeklyModel;
    description: (*
        The ViewMenu lists the calendar view changing options available when 
        viewing another user's calendar.  A ChangeToDailyView option for
        changing to a daily summary window is included here because a user 
        browsing another individual's calendar cannot use the daily appoint
        editor.
    *);
end ViewMenu;

object EditMenu is
    components: ;
    operations: EditDailyAppts, ChangeOptions;
    description: (*
        The EditMenu is available when a user is viewing his or her
        own calendar.  The two operations allow the user to edit
        his or her calendar or change preferences.
    *);
end EditMenu;

object BrowseMenu is
    components: ;
    operations: UserBrowse, GroupBrowse;
    description: (*
        The BrowseMenu enables the user to begin browsing other user
        calendars and various group meeting information.
    *);
end BrowseMenu;


object UserDB is
    components: userList:User*;
    operations: MaintainUserDB;
    description: (*
        The UserDB is the repository for all users of the calendar
        system.
    *);
end UserDB;

object User is
    components: name:UserName, pwd:UserPassword, opt:UserOptions, 
       id:UserId, groups:GroupName*, cal:UserCal, m_alias:MailAlias;
    operations: ;
    description: (*
       The User object defines the information each individual
       will have.  Every user has a UserName, ..., and a Calendar.
    *);
end User;

object UserName is string;
object UserPassword is string;
object UserId is string;
object MailAlias is string;
object Message is string;
object GroupName is string;

object Time is
    components: hr:Hour, min:Minutes;
    operations: ;
    description: (*
        Time is made up of an Hour and Minutes.
    *);
end Time;

object Hour is number;
object Minutes is number;
object Date is
    components: mn:MonthNum, dn:DayNum, yn:YearNum;
    operations: ;
    description: (*
        Date contains the month, day, and year in numerical form.
    *);
end Date;
(*
object Date is string;        (* The date is kept in the form mm/dd/yy *)

object AlarmThreshold is number;
object RepeatThreshold is number;
object MaxDescLength is number;
object MaxSumLength is number;

object DefaultsDB is
    components: at:AlarmThreshold, rt:RepeatThreshold, defMeetingDuration:Time,
                defStartTime:Time, defEndTime:Time, defLocation:RoomId,
                maxDesc:MaxDescLength, maxSummary:MaxSumLength, maxDate:Date,
		maxRepeats:number;
    operations: ChangeDefaults;
    description: (*
        The DefaultsDB contains all of the tunable parameter for the
        calendar system.  The global administrator can adjust these
        using the ChangeDefaults operation.  A breakdown of the default
        settings is as follows:

           The alarm threshold value is the maximum interval that a
           user can assign to any of the alarm values for a scheduled item.

           The maximum number of times a scheduled item can repeated
           is contained in the repeat threshold.

           The default meeting duration is the length of time used when
           the amount isn't specified by the global or group administrator
           attempting to schedule a meeting.

           The default start and end times indicate the range of times
           that the calendar program uses when they aren't specified
           during meeting scheduling.

           Similarly, the default location serves as the primary
           location when it isn't specified in the search parameters
           for scheduling a meeting.

           The maximum description length indicates the maximum number
           of characters that can be used for the description of a scheduled
           item.

           The maximum description length indicates the maximum number
           of characters that can be used for the topic summary of each
           scheduled item.

           maxDate is the farthest date into the future that an appointment
           can be scheduled.
    *);
end DefaultsDB;


object GroupDB is
  components: committee:Group*;
  operations: ;
  equations: 
    var g: GroupDB; 
    var e, e':Group;
    FindInGroupDB(EmptyDB(), e) == false;
    FindInGroupDB(AddtoGroupDB(g, e), e') == 
      if e = e' then true else Find(s,e');
    DeletefromGroupDB(EmptyDB(), e) == Empty;
    DeleteFromGroupDB(AddToGroup(g, e), e') ==
      if e = e' then DeleteFromGroupDB(g, e') 
      else AddToGroupDB(DeleteFromGroupDB(g , e'), e);
  description: (*This holds all the group names and a list of users that
                belong to each gorup.  This database will be updated whenever                   group or user is added or deleted *);
end GroupDB;


object Group is
  components: CommitteeName:GroupName, Member:User, size:number,
	GroupAdmin:User;
  operations: ;
  description: (**);
end Group;

object SchedulingSpec is
  components: meetinginfo:SchedulingInfo;
  operations: Search, Cancel;
  description: (* This screen is used to search for common location, time and
                 date for a meeting.*);
end SchedulingSpec;

object SchedulingInfo is
  components: CommitteeName:GroupName, subject:Topic, Member:User,
              starttime:Time, endtime:Time, startdate:Date, enddate:Date,
              location:RoomId;
  operations: Search, Cancel;
  description: (* This screen is used to search for common location, time and
                 date for a meeting.*);
end SchedulingInfo;

object RoomDB is
  components: room:RoomInfo*;
  operations: ;
  equations: 
    var g: RoomDB;
    var e, e':RoomInfo; 
    FindInRoomDB(EmptyDB(), e) == false;
    FindInRoomDB(AddtoRoomDB(g, e), e') == 
      if e = e' then true else Find(s,e');
    DeletefromRoomDB(EmptyDB(), e) == Empty;
    DeleteFromRoomDB(AddToRoomDB(g, e), e') ==
      if e = e' then DeleteFromRoomDB(g, e') 
      else AddToRoomDB(DeleteFromRoomDB(g , e'), e);
  description: (*
	Collection of rooms that the scheduler has direct access to, which
	we'll refer to as ``local rooms''.  If room is not on this list, then
	its managed by some other agency than that running the calendar system
	(e.g., some campus room guru).
  *);
end RoomDB;

object RoomInfo is
  components: location:RoomId, maximum:MaxOccupants, 
              lists:UnavailabilityList;
end RoomInfo;

object UnavailabilityList  is
  components: dandt:DateAndTime*;
  description: (*List of time slots in which a room is not available*);
end UnavailabilityList ;

object DateAndTime is
  components: mmddyy:Date, t:Time;
  operations: ;
  description: (**);
end DateAndTime;

object RoomId is string;

object MaxOccupants is number;
 
object Priority is boolean;

object SetBrowseParam is
  components: subject:Topic, meetmin:MeetingMinutes, outcome:Decision,
              misc:Miscellaneous;
  operations: ;
  description: (**);
end SetBrowseParam;

object Topic is string;

object MeetingMinutes is string;

object Decision is string;

object Miscellaneous is string;
 
object conflict is
  components: startime:Time, mmddyy:Date, location:RoomId;
  operations: ;
  description: (**);
end conflict; 
 
object CommitteeName is string;
object size is number;







object SearchResults is
	components: d:Date,st:Time,et:Time,u:UserConflictInfo,m:MemberConflict*;
	operations: ;
	description:(**Gives a list of the location, date, time and users with
						the conflicts, with the least conflicts occurring first.
					**);
end SearchResults;

object MemberConflict is
	components: name:User,meetinginfo:SchedulingInfo*,endtime:Time,
					starttime:Time;

	description: (**Gives a list of the users with time conflicts pf meeting.
						It will also list the meeting time.
					**);
end MemberConflict;

object UserConflictInfo is
	components: t:Total, u:UserName*;
	operations: ;
	description:(**A list of the users with conflicts 
					**);
end UserConflictInfo;

object MinuteRecord is
	components: d:Date, st:Time,et:Time,Attendees:User*,m:MeetingMinutes;
	description:(**This is a list of the fields in the minute record, it will
						keep a record of the date, time both starting and ending
						as well as the attendess for the meeting database
					**);
end MinuteRecord;

object MeetingDB is
	components: m:MinuteRecord*;
	operations: ;
	description: ;
end MeetingDB;

object Total is integer;
object filesystem is string;
object dir is string;

object MeetingToBeScheduled is
   components: starttime:Time,endtime:Time, attendees:User*,
               CommitteeName:GroupName,subject:Topic,date:Date,location:RoomId;
   description: (** This object contains the information about a meeting that
                     has been scheduled but not yet taken place.
                  **);
end MeetingToBeScheduled;

object ConflictData is
   components: dateofconflict:Date, timeofconflict:Time, countofconflict:CountofConflict;
end ConflictData;

object ConflictList is
   components: cd:ConflictData*;
end ConflictList;

object CountofConflict is number;


(******
******  OPERATIONS
******)

function IsAlarmValid(alarm:AlarmInfo, ddb:DefaultsDB) -> (boolean) =
        ( alarm.beepAlarm.timeval >= 0) and
        ( alarm.beepAlarm.timeval <= ddb.at)
             and
        ( alarm.mailAlarm.timeval >= 0) and
        ( alarm.mailAlarm.timeval <= ddb.at)
             and
        ( alarm.flashAlarm.timeval >= 0) and
        ( alarm.flashAlarm.timeval <= ddb.at)
             and
        ( alarm.popupAlarm.timeval >= 0) and
        ( alarm.popupAlarm.timeval <= ddb.at);

function IsApptValid(appt:ScheduledItem, ddb:DefaultsDB) -> (boolean) = 
        (appt.startTime <= appt.endTime)
             and
        (#(appt.sum) <= ddb.maxSummary) (* num of characters allowed for a summary *)
             and
        (#(appt.desc) <= ddb.maxDesc) (* num of chars allowed for a description *)
             and
        IsAlarmValid(appt.details.alarm, ddb)
             and
        (appt.details.repeat.timeval >= 0)
	     and
	(appt.details.repeat.timeval <= ddb.maxRepeats);

operation EditDailyAppts is
    components: AddSchedItem, DelSchedItem, EditSchedItem;
    description: ;
end EditDailyAppts;

operation AddSchedItem is
    inputs: ds:DaySchedule, appt:ScheduledItem, ddb:DefaultsDB;
    outputs: ds':DaySchedule;
    precondition: 
        IsApptValid(appt,ddb)
             and
        not IsApptInSchedList(ds, appt);
    postcondition: IsApptInSchedList(ds, appt);
    description: (*
        AddSchedItem inserts an appointment into the list of scheduled
        items for a day in a user calendar.
    *);
end AddSchedItem;

operation DelSchedItem is
    inputs: ds:DaySchedule, appt:ScheduledItem;
    outputs: ds':DaySchedule;
    precondition: IsApptInSchedList(ds, appt) = true;
    postcondition: IsApptInSchedList(ds, appt) = false;
    description: (*
        DelSchedItem deletes an appointment from the list of scheduled
        items for a day in a user calendar.  
    *);
end DelSchedItem;

operation IsApptInSchedList is
    components: ;
    inputs: sl:ScheduledItemList, si:ScheduledItem;
    outputs: b:boolean;
    precondition: ;
    postcondition: si in sl;
    description: (*
        IsApptInSchedList determines if a scheduled item is in the
        list of scheduled items for a day.
    *);
end IsApptInSchedList;

operation EditSchedItem is
    inputs: ds:DaySchedule, appt:ScheduledItem, ddb:DefaultsDB;
    outputs: ds':DaySchedule;
    precondition: 
        IsApptValid(appt,ddb)
           and
        IsApptInSchedList(ds, appt);
    postcondition: IsApptInSchedList(ds, appt);
    description: (*
        EditSchedItem edits an appointment in the list of scheduled
        items for a day in a user calendar.  
    *);
end EditSchedItem;

operation FindSchedItem is
    inputs: ds:DaySchedule, t:Time;
    outputs: apptList:ScheduledItemList;
    precondition: ;
    postcondition:
        forall (si:ScheduledItem) (
            if (si in apptList) then (
                (si in ds) and (si.startTime = t) 
            )
        );
    description: (*
        FindSchedItem returns a scheduled item if there is an appointment
        at the given time and day, returns a null scheduled item otherwise.
        Note, it is possible to have more than one scheduled item for a
        given time.  This may happen when a high priority meeting has been
        penciled in by the meeting scheduler.
    *);
end FindSchedItem;

operation ChangeOptions is
    components: ChangeDayBoundaries, ChangeDefaultView, ChangeAlarmInfo; 
    inputs: u:User, uo:UserOptions;
    outputs: u':User;
    precondition: ;
    postcondition: 
        (u'.opt = uo) and
        (u'.name = u.name) and
        (u'.pwd = u.pwd) and
        (u'.id = u.id) and
        (u'.groups = u.groups) and
        (u'.cal = u.cal) and
        (u'.m_alias = u.m_alias);
    description: (*
        ChangeOptions allows options for a user to be modified, reset,
        or restored to their defaults.
    *);
end ChangeOptions; 

operation ChangeDayBoundaries is
    inputs: uo:UserOptions, bound:DayBoundaries;
    outputs: uo':UserOptions;
    precondition: 
        (bound.startHour >= 0) and (bound.startHour <= 23)
            and
        (bound.endHour >= 0) and (bound.endHour <= 23)
            and
        (bound.startHour <= bound.endHour);
    postcondition:
        uo'.range = bound;
    description: (*
        ChangeDayBoundaries modifies the day boundaries for a user's
        daily calendar view.
    *);
end ChangeDayBoundaries;

operation ChangeDefaultView is
    inputs: uo:UserOptions, tu:TimeUnit;
    outputs: uo':UserOptions;
    precondition: ;
    postcondition:
        uo'.defView = tu;
    description: (*
        ChangeDefaultView sets the default opening calendar view
        seen by a user to either daily, weekly, monthly, or yearly.
    *);
end ChangeDefaultView;

operation ChangeAlarmInfo is
    inputs: uo:UserOptions, ai:AlarmInfo, ddb:DefaultsDB;
    outputs: uo':UserOptions;
    precondition: 
        IsAlarmValid(ai,ddb);
    postcondition: 
        uo'.alarm = ai;
    description: (*
        ChangeAlarmInfo modifies the four types of alarms available
        to a user for reminding him or her of scheduled appointments.
        The four alarm types are: beep, flash, popup, and mail.
    *);
end ChangeAlarmInfo;

operation ChangeToYearlyView is
    inputs: yrnum:YearNum, cal:UserCal;
    outputs: y:Year;
    precondition: ;
    postcondition: (y in cal) and (y.yr = yrnum);
    description: (*
        ChangeToYearlyView changes the current calendar view for the
        user to the yearly view.
    *);
end ChangeToYearlyView;

operation ChangeToMonthlyView is
    inputs: mn:MonthNum, y:Year;
    outputs: m:Month;
    precondition: ;
    postcondition: (m in y.monthList) and (m.mon = mn);
    description: (*
        ChangeToMonthlyView changes the current calendar view for the
        user to the montly view.
    *);
end ChangeToMonthlyView;

operation ChangeToDailyView is
    inputs: dnum:DayNum, m:Month;
    outputs: d:Day;
    precondition: ;
    postcondition: (d in m.dayList) and (d.daynum = dnum);
    description: (*
        ChangeToDailyView changes the current calendar view for the
        user to the daily view.
    *);
end ChangeToDailyView;

operation ChangeToWeeklyModel is
    inputs: date:Date, cal:UserCal;
    outputs: week:Day*;
    precondition: ;
    postcondition: ;
    description: (*
        ChangeToWeeklyModel changes the current calendar view for
        the user to the 7-day model week corresponding to the Date input.
        The week that is displayed begins on the on the closest Monday
        on or before the inputted Date.  A model week contains a quick
        reference which shades busy hours during the week.
    *);
end ChangeToWeeklyModel;

operation ChangeToWeeklySummary is
    inputs: yn:YearNum, mn:MonthNum, dn:DayNum, cal:UserCal;
    outputs: week:Day*;
    description: (*
        ChangeToWeeklySummary changes the current calendar view for
        the user to the 7-day summary of the week corresponding to the
        Date input.  The week that is displayed begins on the on the
        closest Monday on or before the inputted Date.  A weekly summary
        contains a listing of the day summaries for the week.
    *);
end ChangeToWeeklySummary;

operation NextYear is
    inputs: y:Year, uc:UserCal;
    outputs: y':Year;
    precondition: y in uc;
    postcondition: (y' in uc) and (y'.yr = y.yr + 1);
    description: ;
end NextYear;

operation PrevYear is
    inputs: y:Year, uc:UserCal;
    outputs: y':Year;
    precondition: y in uc;
    postcondition: (y' in uc) and (y'.yr = y.yr - 1);
    description: ;
end PrevYear;

operation NextMonth is
    inputs: month:Month, year:Year, uc:UserCal;
    outputs: month':Month;
    precondition: (month in year.monthList) and (year in uc);
    postcondition:  if (month.mon < 12 ) then
                       (month'.mon = month.mon + 1) and
                       (month' in year.monthList)
                    else
                       (month'.mon = 1) and
                       exists (m:Month)
                          (m in (NextYear(year, uc)).monthList) and
                          (month' = m);
    description: (*
        NextMonth obtains the month which directly follows the
        inputted month.
    *);
end NextMonth;

operation PrevMonth is
    inputs: m:Month, y:Year, uc:UserCal;
    outputs: m':Month;
    precondition: (m in y.monthList) and (y in uc);
    postcondition:  if (m.mon > 1 ) then
                       (m'.mon = m.mon - 1) and
                       (m' in y.monthList)
                    else
                       (m'.mon = 12) and
                       exists (m'':Month)
                          (m'' in (PrevYear(y, uc)).monthList) and
                          (m' = m'');
    description: (*
        PrevMonth obtains the month which directly precedes the
        inputted month.
    *);
end PrevMonth;

operation NextDay is
    inputs: day:Day, month:Month, year:Year, uc:UserCal;
    outputs: day':Day;
    precondition:(day in month.dayList) and (month in year.monthList) and
                 (year in uc);
    postcondition: if (day.mmddyy.dn = LastDayOfTheMonth(month.mon)) then
                      (day'.mmddyy.dn = 1) and (day' in
                       (NextMonth(month,year,uc).dayList))
                   else
                      (day'.mmddyy.dn = day.mmddyy.dn + 1) and
                      (day' in month.dayList);
    description: (*
	NextDay obtains the next day which directly follows the
	inputted day.
    *);
end NextDay;

operation PrevDay is
    inputs: day:Day, month:Month, year:Year, uc:UserCal;
    outputs: day':Day;
    precondition:(day in month.dayList) and (month in year.monthList) and
                 (year in uc);
    postcondition: if (day.mmddyy.dn > 1) then
                      (day'.mmddyy.dn = day.mmddyy.dn - 1) and
                      (day' in month.dayList)
                   else
                      (day' in PrevMonth(month, year, uc).dayList) and
                      (day'.mmddyy.dn = LastDayOfTheMonth(day'.mmddyy.mn));
    description: (*
        PrevDay obtains the day which directly precedes the
        inputted day.
    *);
end PrevDay;

function LastDayOfTheMonth(mn:MonthNum) -> (n:number) =
    if ((mn = 1) or (mn = 3) or (mn = 5) or (mn = 7) or (mn = 8) or
     (mn = 10) or (mn = 12)) then
       31
    else if (mn = 2) then
       28  (* This isn't really true because it should be 29 for
              leap years. *)
    else
       30;

operation ImportExportMailAliases is
	inputs: udb:UserDB,gdb:GroupDB,ma:MailAlias,fs:filesystem,d:dir;
	outputs: ma':MailAlias;
	precondition: FindInFileSystem(fs,d)=true; 
						(*We are assuming that a mail alias file in a UNIX based
						file system. In which case we are relying on this file to 
						update the mailing system for the calendar.  *)
	postcondition:  
						(** All modifications to the UNIX based file will affect mail
							aliases 
						**);
end ImportExportMailAliases;

function FindInFileSystem(fs:filesystem,d:dir)->boolean
    description: (*
	Opaque function assumed to be supplied by underlying operating system.
    *);
end FindInFileSystem;


operation MaintainUserDB is
	components:AddUsr,DelUsr,ModifyUsr,Cancel;
	inputs: udb:UserDB,id:UserId,u:User;
	outputs: udb':UserDB;
	description:(** Global Admin will be able to add and delete users from
						the user database 
					**);
end MaintainUserDB;

operation ModifyUsr is
	components: ;
	inputs: member:User, gdb:UserDB,committee:User;
	outputs: gdb':UserDB;
	precondition: FindInUserDB(gdb,committee) = true;
						(** We must find a user in order to modify.
						**)
	postcondition:FindInUserDB(gdb',committee) = false;
						(** A member of the group changes status to group administrator
							and the previous group administrator changes status to 
							a member. 
						**)
end ModifyUsr;
	
operation AddUsr is
	inputs: udb:UserDB, u:User;	
	outputs: udb':UserDB;
	precondition:	FindInUserDB(udb,u) = false;
						(** Searches the user database for a particular user as
							indicated in the second parameter, u, if it finds
							a match then you cannot add the same person twice to
							the user database.
						**)
	postcondition: FindInUserDB(udb',u)=true;
						(** The user now exists in the user database 
						**)
end AddUsr;

operation DelUsr is
	inputs: udb:UserDB, u:User;	
	outputs: udb':UserDB;
	precondition:	FindInUserDB(udb,u)=true;
		(** Searches the user database for a particular user as
		indicated in the second parameter, u, if it finds a
		match then that user can be deleted from the user
		database.
		**)	
	postcondition: FindInUserDB(udb',u)=false;
		(** The user no longer exists in the user database. 
		**)
end DelUsr;

operation UpdateGroupDatabase is
	components:AddGrp,DelGrp,ModifyGrp,Cancel;
	inputs: g:GroupDB,gr:Group;
	outputs: g':GroupDB;
	description:(** The UpdateUserGroupDatabase will add groups, delete groups
			and modify group administrators from the group database.
	**);
end UpdateGroupDatabase;	

operation AddGrp is
   inputs: d:GroupDB, g:Group;
   outputs: d' :GroupDB;
   precondition:FindInGroupDB(d, g) = false;
	(** Searches the group database for a particular group as
	indicated in the second parameter, g, if it finds
	a match then you cannot add the same group, twice to
	the group database.
	**)
   postcondition: FindInGroupDB(d',g)=true;
	(** The group now exists in the group database 
	**)
end AddGrp;


operation DelGrp is
   inputs: d:GroupDB, g:Group;
   outputs: d' :GroupDB;
   precondition: FindInGroupDB(d, g) = true;
	(** Searches the group database for a particular group as
	indicated in the second parameter, u, if it finds a
	match then that group can be deleted from the group
	database.
	**)

   postcondition: FindInGroupDB(d',g)=false;
	(** The group no longer exists in the group database. 
	**)
end DelGrp;

operation ModifyGrp is
	inputs: member:User, gdb:GroupDB,committee:Group;
	outputs: gdb':GroupDB,committee':Group;
	precondition: FindInGroupDB(gdb,committee) = true
						and 
		(committee.GroupAdmin != member)
			(** Seaches the committee for the existing group as
			well as verifies that the member is not currently the
			group admin for that group (INCORRECT, ACTUALLY.)
			**);
	postcondition: committee'.GroupAdmin = member;
			(**	The member is now the group administrator for a
			particular group.  (IBID.)
			**)
end ModifyGrp;

operation ChangeDefaults is
    components: ;
    inputs: systemDefaults:DefaultsDB, newSettings:DefaultsDB, rdb:RoomDB;
    outputs: systemDefaults':DefaultsDB;
    precondition:
          (newSettings.at >= 0) and
          (newSettings.rt >= 0) and
          (newSettings.defMeetingDuration.hr >= 0) and
          (newSettings.defMeetingDuration.min >= 0) and
          (newSettings.defStartTime.hr >= 0) and
          (newSettings.defStartTime.hr <= 23) and
          (newSettings.defStartTime.min >= 0) and
          (newSettings.defStartTime.min <= 59) and
          (newSettings.defEndTime.hr >= 0) and
          (newSettings.defEndTime.hr <= 23) and
          (newSettings.defEndTime.min >= 0) and
          (newSettings.defEndTime.min <= 59) and
          (newSettings.maxDate >= GetCurrentDate()) and
          (newSettings.maxSummary >= 0) and
          (newSettings.maxDesc >= 0) and
          (exists (r:RoomInfo)
             ((r in rdb) and (r.location = newSettings.defLocation)));
    postcondition: systemDefaults' = newSettings;
    description: (*
          ChangeDefaults allows the global administrator to update
          the tunable parameters for the calendar system.
    *);
end ChangeDefaults;

operation GetCurrentDate is
    components: ;
    inputs: ;
    outputs: mmddyy:Date;
    precondition: ;
    postcondition: ;
    description: (*
        GetCurrentDate returns the current date.
    *);
end GetCurrentDate;

operation Cancel is
  inputs: info:SchedulingInfo;
  precondition: ;
  postcondition: (*the meeting screen is canceled*);
end Cancel;

operation SetAlarm is
  inputs: alarm:AlarmInfo;
  outputs: alarm':AlarmInfo, member:User;
  precondition: (*A meeting must have been scheduled*);
  postcondition: (*Alarms for the members of the group are set.*);
end SetAlarm;

operation SetPriority is
  inputs: p:Priority;
  outputs: p':Priority;
  precondition: p = false; 
                 (* A meeting has to have been scheduled *)
  postcondition: p = false 
                    or
                  p = true;
                 (* The priority of the meeting has been set for the members
                    of the group *)
end SetPriority;

operation AddToGroup is
  inputs: gdb:GroupDB, member:User, committee:Group;
  outputs: gdb':GroupDB;
  precondition: FindInGroupDB(gdb, committee) = false;
                 (* The user is not in the database *)
  postcondition: (* FindInGroupDB(gdb', committee.Member) = true
                  and
                   committee.size' = committee.size + 1; *)
                  (* the user has been added as a member of a group *)
	(* Pre and post are both INCORRECT.  Erroneous postcond is particularly
         * interesting. *);
end AddToGroup;

operation DeleteFromGroupDB is
  inputs: gdb:GroupDB, member:User, committee:Group;
  outputs: gdb':GroupDB;
  precondition: FindInGroupDB(gdb, committee) = true;
                 (* User name must be in the group database *)
  postcondition: (FindInGroupDB(gdb', committee) = false)
                  (*and
                  (committee.size' = committee.size - 1)*);
                  (* User name is removed from the database. *)
end DeleteFromGroupDB;

operation AddToRoomDB is
  inputs: rdb:RoomDB, room:RoomInfo, location:RoomId;
  outputs: rdb':RoomDB;
  precondition: (FindInRoomDB(rdb, room) = false);
                 (* The room is not in the database *)
  postcondition: (FindInRoomDB(rdb', room) = true);
                  (* The room is added to the room database *)
end AddToRoomDB;

operation DeleteFromRoomDB is
  inputs: rdb:RoomDB, room:RoomInfo, location:RoomId;
  outputs: rdb':RoomDB;
  precondition: FindInRoomDB(rdb, room) = true;
                 (* Room must be in the RoomDB *)
  postcondition: FindInRoomDB(rdb', room) = false;
                  (* Room is removed from the RoomDB *)
end DeleteFromRoomDB;

operation ModifyRoomInfo is
  inputs: rdb:RoomDB, room:RoomInfo;
  outputs: room':RoomInfo, rdb':RoomDB;
  precondition: FindInRoomDB(rdb, room) = true;
                 (* Room must be in the RoomDB *)
  postcondition: exists (r in rdb') (r = room);
                  (* RoomInfo has been modified and placed back in RoomDB *)
end ModifyRoomInfo;

operation FindInRoomDB is
  inputs: rdb:RoomDB, room:RoomInfo;
  outputs: b:boolean;
  precondition: ;
  postcondition: room in rdb;
end FindInRoomDB;
 
operation FindInGroupDB is
  inputs: gdb:GroupDB, committee:Group;
  outputs: b:boolean;
  precondition: ;
  postcondition: committee in gdb;
end FindInGroupDB;

operation FindInUserDB is
  inputs: udb:UserDB, u:User;
  outputs: b:boolean;
  precondition: ;
  postcondition: b = (u in udb);
end FindInUserDB;


 (**SCHEDULER STUFF **)

operation Schedule is
  inputs:meetinginfo:SchedulingInfo, rdb:RoomDB, mdb:MeetingDB,
         committeename:GroupName, users:User, defaults:DefaultsDB,
         mwc:MemberConflict;
  outputs: results:SearchResults, room:RoomDB, mdb':MeetingDB, members:User;
  precondition: forall (attendee:User) (
		(attendee in udb.userList) and
                (meetinginfo.starttime < meetinginfo.endtime) and
                (meetinginfo.startdate < meetinginfo.enddate) and
                (meetinginfo.location in room));

   (* Attendees must all be registered users
      If given, start time must be before end time
      Ditto for start/end dateD
      If given, loc must be in Cal room db
    *)
   postcondition: 
      if (  UsersCanAttend(results,meetinginfo) and
         StartTimeAndDateAreNearest(results,users) and
         AttendeesCorrect(results,meetinginfo,MtgTbSched) and
         TimeRangeMet(results,meetinginfo) and
         DateRangeMet(results,meetininfo) and
         LocationMet(results,meetinginfo))then true
      else
         FindUserTimeConflict(results,meetinginfo,MtgTbSched);

  description: (*
   Among other constraints, if a room cannot be found for a meeting, but a
   time can, then the location field of the outputs is left as ``call for
   room'', meaning the that human scheulder needs to ask for a room
   through some other agency.  The idea is that we'll schedule a meeting
   if a time can be found, whether or not we can find a local room.
  *);
end Schedule;

function FindUserTimeConflict(meetinginfo:SchedulingInfo,results:SearchResults,
                         MtgTbSched:MeetingToBeScheduled) -> (MemberConflict) =
 
 
  forall (meetinginfo: SchedulingInfo) 

     if(meetinginfo.attendees.cal.yearList.monthList.dayList.daySched.schedList.
         startTime != empty) then
       if (meetinginfo.attendees.cal.yearList.monthList.dayList.daySched.
           schedList.starttime <= MtgTbSched.starttime) and
          (meetinginfo.attendees.cal.yearList.monthList.dayList.daySched.
           schedList.starttime > MtgTbSched.starttime) then

         mc.uname.name = meetinginfo.attendees.name and
         mc.mi.startdate = meetinginfo.startdate and
         mc.mi.edddate = meetinginfo.enddate and
         mc.st = meetinginfo.cal.yearList.monthList.dayList.daySched.schedList.
               starttime and
         mc.et = meetinginfo.cal.yearList.monthList.dayList.daySched.
                 schedList.endtime
      
      else if (meetinginfo.attendees.cal.yearList.monthList.dayList.daySched.
          schedList.endtime > MtgTbSched.starttime) and 
         (meetinginfo.attendees.cal.yearList.monthList.dayList.daySched.
          schedList.endtime <= MtgTbSched.endtime) then

         mc.uname.name = meetinginfo.attendees.name and
         mc.mi.startdate = meetinginfo.startdate and
         mc.mi.edddate = meetinginfo.enddate and
         mc.st = meetinginfo.cal.yearList.monthList.dayList.daySched.schedList.
               starttime and
         mc.et = meetinginfo.cal.yearList.monthList.dayList.daySched.
                 schedList.endtime;
         

function TimeRangeMet(results:SearchResults, meetinginfo:SchedulingInfo,
                      defaults:DefaultsDB) -> (boolean) =


   if (results.starttime != empty) then
      results.starttime >= meetinginfo.starttime
   else if (results.starttime = empty) then
      results.starttime >= defaults.endtime
   else if (results.endtime != empty) then
      results.endtime <= meetinginfo.endtime
   else if (results.endtime = empty) then
      results.endtime >= defaults.endtime 
      
   else true;

function DateRangeMet(results:SearchResults,meetinginfo:SchedulingInfo,
                      defaults: DefaultsDB) -> (boolean) =

   if (results.startdate != empty) then
      results.startdate >= meetinginfo.startdate
   else if (results.startdate = empty) then
         results.startdate >= defaults.startdate 
   else if (results.enddate != empty) then
      results.startdate <= results.enddate
   else if (results.enddate = empty) then
         results.enddate >= defaults.startdate 
   else true;


function LocationMet(results:SearchResults,meetinginfo:SchedulingInfo,
                     defaults:DefaultsDB) -> (boolean) =

(* Checks to see if the room is exists in the room database, and returns
true  if it does. If a room is not specified, true is returned in case
the scheduler wants to know if people can meet
*)

   if (results.location !=  empty) then
       results.location = meetinginfo.location
   else  
       true;
   

function AttendeesCorrect(results:SearchResults,meetinginfo:SchedulingInfo,
                  udb:UserDB,MtgTbSched:MeetingToBeScheduled) -> (boolean) =

(* Checks to see that the attendees are valid by verification with the 
user database 
*)
                           
   forall (MtgTbSched:MeetingToBeScheduled) 
      (MtgTbSched.attendees in udb) and
      (MtgTbSched.attendees in meetinginfo.Members);



function UsersCanAttend(results:SearchResults,
                        MtgTbSched:MeetingToBeScheduled,users:User,
                        meetinginfo:SchedulingInfo) -> (boolean) =

(* Checking to see if the start time and stop times are valid *)
   
   forall (MtgTbSched: MeetingToBeScheduled)
         if((MtgTbSched.attendees.cal.yearList.monthList.dayList.daySched.schedList.
            startTime) != empty) then

               (MtgTbSched.attendees.cal.yearList.monthList.dayList.daySched.   
                     schedList.starttime < meetinginfo.starttime and
                MtgTbSched.attendees.cal.yearList.monthList.dayList.daySched.   
                     schedList.endtime <= meetinginfo.starttime)

                             or 

         if((attendees.cal.yearList.monthList.dayList.daySched.schedList.
            startTime) != empty) then

               (attendees.cal.yearList.monthList.dayList.daySched.   
                     schedList.starttime >= meetinginfo.starttime and
                   attendees.cal.yearList.monthList.dayList.daySched.   
                     schedList.endtime > meetinginfo.starttime);