(****
 *
 * Module File defines the objects and operations related to file processing
 * in the scheduler system.
 *
 *)

module File;

object CurrentSchedule;

object FileSpace is File*;

(*  Needed??   *)
(*
from ScheduleDB import ScheduleDB, UserSchedule, UserWorkSpace, RequiresSaving;
from Options import Options;
export File;
*)

object File is
	components: name:FileName and permissions:FilePermissions and
		file_type:FileType and data:FileData;
	description: (*
		A File is an abstraction of a file stored in the file space.  It has a
		quarter, year, and Schedule.  These are the components sufficient
		to specify the behavior of Schedule Tool file operations.
	*);
end File;


object FileName is string
	description: (*
	The name of a file.  The string representation here is an abstraction
	of file names used in specific operating environments.  Implementations
	may obey any syntactic or semantic constraints imposed by a particular
	environment.
	*);
end FileName;


object FilePermissions is is_readable:IsReadable and is_writable:IsWritable
	description: (*
		FilePermissions indicate whether a file is readable and/or writable.
	*);
end;


object IsReadable is boolean
	description: (*
		Flag indicating whether a file is readable, which is required to be
		true by the FileOpen operation.
	*);
end;


object IsWritable is boolean
	description: (*
		Flag indicating whether a file is writable, which is required to be
		true by the FileSave operation.
	*);
end;


object FileType is schedule_type:ScheduleType or other_type:OtherType
	description: (*
		The type of file data is either ScheduleType data (which we care about)
		or any other type of data that can be stored in a file, which we don't
		care about.
	*);
end FileType;


object ScheduleType
	description: (*
		File data typing tag indicating that a file contains schedule data
		created by the Scheduler Tool.
	*);
end ScheduleType;


object OtherType
	description: (*
		File data typing tag indicating that a file contains data other than
		calendar data created by the Schedule Tool.
	*);
end OtherType;


object FileData is CurrentSchedule
	description: (*
		The abstract representation of schedule-type FileData is a UserSchedule
		object.  Scheduler Tool implementors may use any concrete file data
		representation that accurately holds all UserSchedule components.
	*);
end FileData;



operation FileNew is
	inputs: cs:CurrentSchedule;
	outputs: f:File;

	description: (*
		Add a new empty schedule to the workspace.
	*);

	precondition: (cs != nil);

	postcondition: (*
                        *The file exists on the user's hard drive
                        *);


end FileNew;


operation FileOpen is
	inputs: f:File, cs:CurrentSchedule, st:ScheduleType;
	outputs: cs':CurrentSchedule;

	description: (*
		Open an existing schedule file of the given name and put the data from
		that file in the current schedule.
	*);

	precondition:
	(*
	 * The file is readable, and the file's data are of type scheduler.
	 *)
	f.permissions.is_readable and
	f.file_type = st;

	postcondition:
	(*
	 * The given file is in the current schedule
	 *);

end FileOpen;


operation FileSave is
	inputs: cs:CurrentSchedule, fs:FileSpace, st:ScheduleType;
	outputs: fs':FileSpace;

	description: (*
		save the current schedule in the
		given file space.
	*);

	precondition:
        (*
         * There is a writable
         * file of the current workspace filename in the given FileSpace.  Note
         * that the only way the current file could be unwritable is through an
         * external change to the file space since the file was opened by the
         * Schedule Tool.  Note further that this precondition disallows the
         * case where the current calendar file has been externally deleted
         * since it was opened by the calendar tool.  That is, the file must
         * both exist and be writable at the time the save is attempted.
         *)

        (exists (file in fs)
            (file.permissions.is_writable));

	postcondition:
        (*
         * There is a scheduler-type file in the resulting FileSpace containing
         * the current workspace calendar as its file data.  In the resulting
         * workspace, the requires saving indicator is false.
         *)
        (exists (file in fs')
            (file.permissions.is_writable) and
            (file.file_type = st)
        );
	end FileSave;

end File;