obj FileSpace has File*;
obj File has name:FileName and data:FileData;
obj FileName is Name;

obj WorkSpace has name:Name and r:Rolodex
    description: (*
        A workspace models the use work area, which can contain at most one
        open rolodex file.
    *);
end;

operation New()->w':WorkSpace
    post: w'.name = "Untitled" and w'.r = nil;
end New;

operation Open(fs:FileSpace, n:Name)->w':Workspace
    post:
        exists (f in fs) (f.name = n) and (w'.r = f);
    description: (*
        Open is essentially a find operation, with the same form of 
        poscondition as a basic find.
    *);
end Open;        

operation Save(fs:FileSpace, w:Workspace)->fs':FileSpace
    post:
        (* The rolodex in the given worksapce is in the output filespace *)
        exists (f in fs') (
            (f.name = w.name) and (f.data = w.r)

            and

	    (* No files of the same name are in the filespace. *)
	    forall (f':File | f' != f)
		(f' in fs') iff (f' in fs) and (f'.name != w.name)
        );

    description: (*
        Save is essentially a change operation, with the same form of
        postcondition as a basic change.  There is no precondition, since a
        file for the given rolodex need not already exist in the file space.

        NOTE: in this workspace version of Save, there is a subtle scoping
        change in postcondition compared to the earlier versions of Save.
        Specifically, the universal quanification is nested within the
        existential quantification.  This is because the File variable f is
        defined in the scope of the exists, not as an input parameter.
    *);
end Save;