obj FileSpace =  Rolodex*;
obj Rolodex =  name:Name and cards:Card*;
obj Card =  ...;
obj Name =  string;

operation New()->r':Rolodex
    post: r' = nil;
end New;

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

operation Save(fs:FileSpace, r:Rolodex)->fs':FileSpace
    post:
        (* The given rolodex is in the output filespace *)
        (r in fs')

            and

        (* No rolodexes of the same name are in the filespace. *)
        forall (r':Rolodex | r' != r)
            (r' in fs') iff (r' in fs) and (r'.name != r.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.
    *);
end Save;

operation SaveAs(fs: FileSpace, r:Rolodex, n:Name)->fs':FileSpace

    pre: ;
        (* Note there is no precondition that prevents unintentional
         * overwriting of a rolodex of the same name in the input fs.  This
         * could be added if necessary. *)

    post:
	(* There is a rolodex, with the same cards as the input rolodex and the
         * given name, in the output filespace. *)
        exists (r' in fs') (r'.name = n) and (r'.cards = r.cards)

            and

        (* No other rolodexes of the same name are in the filespace. *)
        forall (r':Rolodex | r' != r)
            (r' in fs') iff (r' in fs) and (r'.name != r.name);

    description: (*
        SaveAs differs from Save in that the name of the saved rolodex must be
        that given, rather than the original name of the input rolodex.  This
        difference is reflected in the first clause of the postcondition of
        SaveAs vis a vis Save.  The second postcondition clause is the same in
        both Save and SaveAs.
    *);
end SaveAs;

operation Print(r:Rolodex)->r':Rolodex
    post: SortedByName(r');
    description: (*
        Printing produces a sorted rolodex.  It could be augmented with an
        Options input that would specify different sorting orders.  Note that
        this abstract view of printing does not formally specify print
        formatting details.  This issue is addressed in the more concrete level
        of file operation specification.
    *);
end Print;