DEFINITION MODULE SeqFile; (* Rewindable sequential files *) IMPORT IOChan, ChanConsts; FROM ChanConsts IMPORT ChanFlags; TYPE ChanId = IOChan.ChanId; FlagSet = ChanConsts.FlagSet; OpenResults = ChanConsts.OpenResults; (* Accept singleton values of FlagSet *) CONST read = FlagSet{readFlag}; (* input operations are requested/available *) write = FlagSet{writeFlag};(* output operations are requested/available *) old = FlagSet{oldFlag}; (* file may/must/did exist before channel was opened *) text = FlagSet{textFlag}; (* text operations are requested/available *) raw = FlagSet{rawFlag}; (* raw operations are requested/available *) PROCEDURE OpenWrite (VAR cid : ChanId; name : ARRAY OF CHAR; flags : FlagSet; VAR res : OpenResults); (* Attempts to obtain and open a channel connected to a stored rewindable file The write flag is implied; without the raw flag, text is implied. If successful, assigns to the parameter cid the identity of a channel open to a stored file of the given name and assigns the value opened to the parameter res. The file is truncated to zero length. Output mode is selected. If a channel cannot be opened as required, the value of the parameter res indicates the reason and cid identifies the bad channel. *) PROCEDURE OpenAppend (VAR cid : ChanId; name : ARRAY OF CHAR; flags : FlagSet; VAR res : OpenResults); (* Attempts to obtain and open a channel connected to a stored rewindable file The write and old flags are implied; without the raw flag, text is implied. If successful, assigns to the parameter cid the identity of a channel open to a stored file of the given name and assigns the value opened to the parameter res. Output mode is selected and the write position corresponds to the length of the file. If a channel cannot be opened as required, the value of the parameter res indicates the reason and cid identifies the bad channel. *) PROCEDURE OpenRead (VAR cid : ChanId; name : ARRAY OF CHAR; flags : FlagSet; VAR res : OpenResults); (* Attempts to obtain and open a channel connected to a stored rewindable file The read and old flags are implied; without the raw flag, text is implied. If successful, assigns to the parameter cid the identity of a channel open to a stored file of the given name and assigns the value opened to the parameter res. Input mode is selected. The read position is at start of file. If a channel cannot be opened as required, the value of the parameter res indicates the reason and cid identifies the bad channel. *) PROCEDURE IsSeqFile (cid : ChanId) : BOOLEAN; (* Tests if the channel is open to a rewindable sequential file *) PROCEDURE Reread (cid : ChanId); (* If the channel is not open to a rewindable file, the exception wrongDevice is raised. Otherwise, if successful, sets the read position to the start of the file and selects input mode. If the operation cannot be performed, perhaps because of insufficient permissions, neither input nor output mode is selected. *) PROCEDURE Rewrite (cid : ChanId); (* If the channel is not open to a rewindable file, the exception wrongDevice is raised. Otherwise, if successful, truncates the file to zero length and selects output mode. If the operation cannot be performed, perhaps because of insufficient permissions, neither input nor output mode is selected. *) PROCEDURE Close (VAR cid : ChanId); (* If the channel is not open to a rewindable file, the exception wrongDevice is raised. Otherwise, the channel is closed and the value identifying the bad channel is assigned to the parameter cid. *) END SeqFile.