obj FileSpace =  File*;
obj File =  type:FileType and name:FileName and data:FileData;
obj FileType =  a:ASCIIType or b:BinaryType or rolo:RolodexType or ... ;
obj FileName =  Name;
obj FileData =  ascii:ASCIIData or bin:BinaryData or rolo:RolodexData or ... ;
obj ASCIIData =  string*;
obj BinaryData =  number*;
obj RolodexData =  Rolodex;
obj ASCIIType;
obj BinaryType;
obj RolodexType;

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:
	(* 
         * There is a file of the given name in either ASCII or Rolodex format
         * in the given file space.  If the latter, then the cards of the
         * output rolodex contain the converted ASCII data.  If the former
         * (i.e., file is in Rolodex format), then the cards of the output are
         * those in the file.
         *)
        exists (f in fs)
            (* File and rolodex names are the same *)
	    r'.name = f.name

                and

            (* File data are the same as rolodex cards, parsed if ASCII *)
            if (f?.ascii) then
                r'.data = ParseRolodexText(f.ascii)
            else if (f?.rolo) then
                r'.data = f.rolo
            else false; (* Neither ascii nor Rolodex file format *)

    description: (*
        Open is essentially a find operation, with the same underlying form of
        poscondition as a basic find.  This more concrete version of Open must
        parse ASCII text data files, if that is format in which a rolodex was
        saved.

        The postcondition relies on a non-trivial auxiliary function,
        ParseRolodexText, that would specify preciely the correspondence
        between the textual and abstract representations of rolodex card data.
    *);
end Open;        

operation Save(fs:FileSpace, r:Rolodex, type:FileType)->fs':FileSpace
    description: (*
        Save operates the same as the more abstract version of save, except
        that it uses the FileType input to determine the format of the file
        in the output filespace.
    *);

end Save;

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

    post: ... ;  (* Comparable change to Save. *)

end SaveAs;

operation Print(r:Rolodex)->rp:RolodexPrintout
    post: 
	exists (r':Rolodex) exists (c:Card)
            (c in r') iff (c in r) and SortedByName(r') and
                rp = GeneratePrint(r');

    description: (*
        Printing produces the ASCII text for a sorted Rolodex.  The
        postcondition here relies on a non-trivial auxiliary function,
        GeneratePrintText, that would define textual formatting details
        precisely.  GeneratePrintText is the complement of the earlier
        ParseRolodexText function.

        Note that the postcondition specifies sorting on the rolodex, rather
        than on the printout, as would be the case with the following logic:

            forall (c in r)
                (GenerateCardPrint(c) in rp) and SortedByName(rp)

        This logic for sorting a printout would be considerably more tedious,
        since it would have to perform parsing to extract the name field from
        the text representation of a card.
    *);

end Print;