(****
 *
 * Module File contains objects for an abstract file space and operations to
 * store and retrieve rolodex files.  The file space is highly abstract, in
 * that each file contains Rolodex data directly.  There is no specification of
 * the concrete datafile representation for the Rolodex data.  This means that
 * an implementation is free to store Rolodex data in any concrete form.
 *
 *)

module File;

  from Rolodex import Rolodex, Card, Name;

  obj FileSpace is File*;
  obj File is n:Name and fd:FileData;
  obj FileData is Rolodex;

  operation New()->r':Rolodex
    description: (*
        Create a new empty rolodex.
    *);
    post: r' = nil;
  end New;

  operation Open(fs:FileSpace, n:Name)->r':Rolodex
    description: (*
        Open an existing rolodex file of the given name.  Create a rolodex
        containing the data of the opened file.
    *);

    pre:
        (*
         * There is a file of the given Name in the given FileSpace.
         *)
        exists (f in fs) f.n = n;

    post:
        (* 
         * The output Rolodex is that stored on the file of the given name.
         *)
        exists (f in fs)
            (f.n = n) and (f.fd = r');
  end Open;        

  operation Save(fs:FileSpace, r:Rolodex)->fs':FileSpace
    description: (*
        Save the given rolodex in the given filesapce.

        Save is essentially an add operation.  It should be foramally specified
        in a comparable manner.
    *);
  end Save;

  operation SaveAs(fs: FileSpace, r:Rolodex, n:Name)->fs':FileSpace
    description: (*
        Save the given rolodex in the given filesapce under the given name.
    *);
    post: ;  (* Comparable change to Save. *)

  end SaveAs;

  operation Print(r:Rolodex)->rp:RolodexPrintout
    description: (*
        Print the given Rolodex in textual format.
    *);
    post: 
        exists (r':Rolodex, 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.

        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;

  operation Quit is
    inputs: ;
    outputs: ;
    description: (*
	Quit the rolodex system.
    *);
  end Quit;

  obj RolodexPrintout;

  (**
   * The following auxiliary functions should be defined as discussed in the
   * formal spec primer.
   *)
  function ParseRolodexText(ASCIIData)->Card*;
  function GeneratePrint(Rolodex)->RolodexPrintout;
  function SortedByName(Card*)->boolean;

end File;