Concept Flat_File_System_Template;
	uses Std_Boolean_Fac, Std_Char_Facility, Std_Char_String_Fac, String_Theory;
	
	Definition Max_Disk_Space: N;
		constraints Max_Disk_Space > 0;

	Var FS: Str(Character) -> Cart_Prod
			Is_Creared: B;
			Is_Open: B;
			Is_Read_Only: Boolean;
			Contents: Str(Character);
		end;
		Definition var Total_File_Length: N = 
		   (Summation, For all Name: Str(Character), 
			where FS(Name).Is_Created  ( |FS(Name).Contents| ));
		constraints (For all Name: Str(Character), 
			FS(Name).Is_Open implies FS(Name).Is_Created) and
			Total_File_Length <= Max_Disk_Space;

	Type Family File_Accessor is modeled by 
		Cart_Prod
			Name: Str(Character);
			Position: Integer;
			Trans_Contents: Str(Character);
		end;
		exemplar F;
		constraints (F.Trans_Contents /= empty_string 
						implies F.Position = 0) and
		   (For all Name: Str(Character), 
			FS(F.Name).Is_Created implies 
				F.Position <= |FS(F.Name).Contents|) and
				FS(F.Name).Is_Read_Only implies F.Trans_Contents = empty_string;
		initialization 
			ensures F.Name = empty_string and F.Position = 0 and 
				F.Trans_Contents = empty_string;

	Operation Give_Name (evaluates Name: Char_String; updates F: File_Accessor);
		requires Name /= empty_string;
		ensures F.Name = Name and F.Position = #F.Position and 
				F.Trans_Contents = #F.Trans_Contents;

	Operation Create(preserves F: File_Accessor);
		affects FS;
		requires not FS(F.Name).Is_Created;
		ensures FS(F.Name).Is_Created;

	Operation Open_for_Reading(preserves F: File_Accessor);
		affects FS;
		requires FS(F.Name).Is_Created and not FS(F.Name).Is_Open;
		ensures FS(F.Name).Is_Open and FS(F.Name).Is_Read_Only;







	Operation Read (replaces c: Character; updates F: File_Accessor);	
		requires FS(F.Name).Is_Open and FS(F.Name).Is_Read_Only and 
		   F.Position < |FS(F.Name).Contents| which_entails
			Prt_Btwn(F.Position, F.Position + 1, FS(F.Name).Contents): Prime;
		ensures c = Destring(Prt_Btwn(F.Position, F.Position + 1, FS(F.Name).Contents)) and
			F.Position = #F.Position + 1 and
			F.Name = #F.Name and F.Trans_Contents = #F.Trans_Contents;

	Operation Is_at_End (preserves F: File_Accessor): Boolean;	
		ensures Is_at_End = (F.Position = |FS(F.Name).Contents|);

	Operation Open_for_Writing(preserves F: File_Accessor);
		affects FS;
		requires FS(F.Name).Is_Created and not FS(F.Name).Is_Open;
		ensures FS(F.Name).Is_Open and not FS(F.Name).Is_Read_Only;

	Operation Write (evaluates C: Character; updates F: File_Accessor);	
		requires FS(F.Name).Is_Open and not FS(F.Name).Is_Read_Only;
		ensures F.Trans_Contents = #F.Trans_Contents o <C> and
			F.Name = #F.Name and F.Position = #F.Position; 

	Operation Write_Commit (updates F: File_Accessor);	
		affects FS, Total_File_Length;
		requires FS(F.Name).Is_Open and not FS(F.Name).Is_Read_Only and 
			Total_File_Length + |F.Trans_Contents| <= Max_Disk_Space;
		ensures FS(F.Name).Contents = #FS(F.Name).Contents o #F.Trans_Contents and
			F.Trans_Contents = empty_string and 
			F.Name = #F.Name and F.Position = #F.Position;

	Operation Is_Created(evaluates Name: Char_String): Boolean;
		ensures Is_Created = (FS(Name).Is_Created);

	Operation Is_Open(preserves F: File_Accessor): Boolean;
		ensures Is_Open = (FS(Name).Is_Open);

	Operation Is_Read_Only(preserves F: File_Accessor): Boolean;
		ensures Is_Read_Only = (FS(Name).Is_Read_Only);

	Operation Is_Commit_Permissible(preserves F: File_Accessor): Boolean;
		ensures Is_Commit_Permissible = 
			(Total_File_Length + |F.Trans_Contents| <= Max_Disk_Space);

	Operation Is_Full_Disk (): Boolean;
		Is_Full_Disk = (Total_File_Length = Max_Disk_Space);
end Flat_File_System_Template;

