(**** * * Module File contains objects for an abstract file space and operations to * store and retrieve rolodex files. * * NOTE: We're trying here to figure out about how precislely to spec the * operational-feeling offer-to-save behavior of the file ops. What's in this * file around the New op almost certainly cannot be right, since it has a call * to OfferToSave in both the pre- and postconds of New. Per the 3 and 5 Mar * 00 discussions in se-book/formal-spec, we need to stick with either, not * both. See that discussion for guidance about how this bogus version of the * spec will be turned into a non-bogus version, which will reside in the file * file.rsl. * *) module File; from Rolodex import Rolodex, Card, Name; export File, FileSpace; obj FileSpace is fs:File* and cur:FileName; obj File is type:FileType and n:FileName and fd:FileData; obj FileType is at:ASCIIType or bt:BinaryType or rt:RolodexType; obj FileName is Name; obj FileData is ad:ASCIIData or bd:BinaryData or rd:RolodexData; obj ASCIIData is string*; obj BinaryData is number*; obj RolodexData is Rolodex; obj ASCIIType; obj BinaryType; obj RolodexType; operation New(fs:FileSpace, r:Rolodex)->(fs':FileSpace, r':Rolodex) description: (* Offer to save the currently open rolodex if necessary, and create a new empty rolodex. *); pre: (* * If OfferToSave returns Saved or Discarded, then proceed else not. *) OfferToSave(fs, r, nil).result = true; post: if OfferToSave(fs, r, nil).result then (fs' = OfferToSave(fs, r, nil).fs') and (r' = OfferToSave(fs, r, nil).r') and (fs'.cur = ChooseFile()) else (fs' = fs) and (r' = r) and (fs'.cur = fs.cur); 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. *); 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.fs) (* File and rolodex names are the same. *) -- (r'.n = f.n) (* Assumes roldexes have names, which they dont *) -- (* in the current definition of Rolodex. This *) -- and (* is fixed in the good version of file.rsl. *) (* File data are the same as rolodex cards, parsed if ASCII *) if (f.fd?ad) then r' = ParseRolodexText(f.fd.ad) else if (f.fd?rd) then r' = f.fd.rd else false; (* Neither ascii nor Rolodex file format *) description: (* Open is essentially a find operation, with the same underlying form of postcondition 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 precisely the correspondence between the textual and abstract representations of rolodex card data. *); 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. 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; 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; operation OfferToSave (fs:FileSpace, r:Rolodex, s:Selection) -> (fs':FileSpace, r':Rolodex, result:boolean) preconditions: ; postconditions: ; description: (* Offer to save the given rolodex on the given file space. If the selection is Save, then do the save and return a true result. If the selection is Discard, then don't do the save but still return a true result. If the selection is Cancel, then don't do the save and return a false result. *); end OfferToSave; operation ChooseFile() -> string; obj Selection is Save or Discard or Cancel; obj Save; obj Discard; obj Cancel; end File;