library FileSystem


%% Techniken zur Entwicklung korrekter Software II
%% Spezifikation eines Dateisystems in CASL
%% Walid und Katja Abu-Dib, Sonja Gröning, Wiebke Herding
%% 14. Mai 2002

from Basic/StructuredDatatypes get String, List, FiniteSet
from Basic/SimpleDatatypes get Boolean 

spec FS1 = 

sorts File, Name, Content, Fs

ops
  [] : Content;
  __ ++ __ : Content * Content -> Content;
  getContent: File -> Content;
  setContent: File * Content -> File;
  getName: File -> Name;
  setName: File * Name-> File;
  newFile: Name -> File;  

forall f,f1,f2:File; c,c1,c2,c3:Content; n:Name
. getContent(setContent(f,c)) = c 
. getName(setContent(f,c)) = getName(f)
. getName(setName(f,n)) = n
. getContent(setName(f,n)) = getContent(f)
. getName(newFile(n)) = n
. getContent(newFile(n)) = []
. c1 ++ (c2 ++ c3) = (c1 ++ c2) ++ c3		%%Associativity

ops
  empty: Fs;
  add: Fs * File -> Fs;
  getFile:  Fs * Name ->? File;

pred
  __?__:  Fs * Name;  %%ExistsFile
  __ isIn __: File * Fs

forall fs,fs1,fs2:Fs; n,n1,n2:Name; f,f1:File
. not (f isIn empty)
. (f isIn (add(fs,f1)) ) <=> ((f = f1) \/ (f isIn fs))

. (fs1 = fs2) <=> (forall f1:File . f1 isIn fs1 <=> f1 isIn fs2)

. def getFile(fs,n) <=> fs?n
. getFile(fs,n) =e= f <=> getName(f) = n /\ f isIn fs

%% User-Ops ----------------------

ops 
  create: Fs * Name -> Fs;
  read: Fs * Name ->? Content;
  write: Fs * Name * Content -> Fs;
  copy: Fs * Name * Name -> Fs;
  rename: Fs * Name * Name -> Fs;
  remove: Fs * Name -> Fs;
  append: Fs * Name * Content -> Fs;

%% -------------------------------

forall fs,fs1:Fs; n,n1,n2,n3:Name; c:Content; f:File

%% create:
%% After creating a file, it exists in the fs.
. create(fs,n) ? n	

%% All other files (than the newly created)  are not affected
%% (neither their existence nor their content).
. not (getName(f)=n) => (f isIn fs <=> f isIn (create(fs,n)))

%% The content of a newly created file remains unspecified.
%% What happens, if a file is created with a name of an  
%% existing file, remains unspecified.

%% ------------------------------------
%% read:
. read(fs,n) = getContent(getFile(fs,n))

%% ------------------------------------
%% write:
%% After writing a content to a file, the content is in the file.
. fs?n => getFile(write(fs,n,c),n) = setContent(getFile(fs,n),c)

%% All other files (than the one written)  are not affected
%% (neither their existence nor their content).
. not (getName(f)=n) => (f isIn fs <=> f isIn (write(fs,n,c)))

%% Writing a non-existent file remains unspecified.


%% ------------------------------------
%% append:
%% After appending a content to file, the new content of the file 
%% is the concatenation of the old and the appended content.
. fs?n => getFile(append(fs,n,c),n) = setContent(getFile(fs,n),
          getContent(getFile(fs,n)) ++ c)

%% All other files (than the one written)  are not affected
%% (neither their existence nor their content).
. not (getName(f)=n) => (f isIn fs <=> f isIn (append(fs,n,c)))

%% Appending something to a non-existent file remains unspecified.

%% ------------------------------------
%% copy: 
%% After copying a file the new file exists.
%% The copied files are equal except for the name
. fs?n1 => getFile(fs,n1) = setName(getFile(copy(fs,n1,n2),n2), n1)

%% Copying a non-existent file does not change the fs.
. not fs?n1 => copy(fs,n1,n2) = fs

%% All other files (than the one copied)  are not affected
%% (neither their existence nor their content).
. (  not (getName(f) = n2) ) => (f isIn fs <=> f isIn (copy(fs,n1,n2)))

%% ------------------------------------
%% rename:
%% After renaming a file the file with the old name does not exist 
%% and the file with the new name exists.
. fs?n1 => getFile(fs,n1) = setName(getFile(rename(fs,n1,n2),n2), n1)
. fs?n1 => ((rename(fs,n1,n2) ? n1) => (n1 = n2))

%%. (fs?n1 /\ not (n1 = n2) ) => ( (rename(fs,n1,n2) ? n2) /\ 
%%				  not (rename(fs,n1,n2) ? n1) )

%% Renaming a non-existent file does not change the fs.
. not fs?n1 => rename(fs,n1,n2) = fs

%% all other files (than the one renamed)  are not affected
%% (neither their existence nor their content)
. (not (n1 = getName(f)) /\ not (n2 = getName(f))) =>
		(f isIn fs <=> f isIn (rename(fs,n1,n2)))

%% ------------------------------------
%% remove:
%% after removing a file, it does not exist in the fs
. not remove(fs,n) ? n

%% all other files (than the one removed)  are not affected
%% (neither their existence nor their content)
. not (getName(f)=n) => (f isIn fs <=> f isIn (remove(fs,n)))

then %implies
forall n,n1,n2: Name; fs:Fs; c:Content 
%% removing a non-existent file does not change the fs
. not fs?n => remove(fs,n) = fs
. read(write(fs,n,c),n) = c
. getFile(fs,n1) =e= getFile(fs,n2) => n1 = n2

end