DEFINITION MODULE RndFile; (* Random access 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 OpenOld (VAR cid : ChanId; name : ARRAY OF CHAR; flags : FlagSet; VAR res : OpenResults); (* Attempts to obtain and open a channel connected to a stored random access file The old flag is implied; without the write flag, read is implied; without the text flag, raw is implied. If successful, assigns to the parameter cid the identity of a channel open to a random access file of the given name and assigns the value opened to the parameter res. The read and/or write position is at the start 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 OpenClean (VAR cid : ChanId; name : ARRAY OF CHAR; flags : FlagSet; VAR res : OpenResults); (* Attempts to obtain and open a channel connected to a stored random access file The write flag is implied; without the text flag, raw is implied. If successful, assigns to the parameter cid the identity of a channel open to a random access file of the given name and assigns the value opened to the parameter res. The file is of zero length. If a channel cannot be opened as required, the value of the parameter res indicates the reason and cid identifies the bad channel. *) PROCEDURE IsRndFile (cid : ChanId) : BOOLEAN; (* Tests if the channel is open to a random access file *) PROCEDURE IsRndFileException () : BOOLEAN; (* Returns TRUE if the current coroutine is in the exceptional execution state because of the raising of a RndFile exception; otherwise returns FALSE. *) CONST FilePosSize = SIZE(CARDINAL); TYPE FilePos = CARDINAL; (* ARRAY [1..FilePosSize] OF LOC *) PROCEDURE StartPos (cid : ChanId) : FilePos; (* If the channel is not open to a random access file, the exception wrongDevice is raised. Otherwise, returns the position of the start of the file. *) PROCEDURE CurrentPos (cid : ChanId) : FilePos; (* If the channel is not open to a random access file, the exception wrongDevice is raised. Otherwise, returns the current read/write position. *) PROCEDURE EndPos (cid : ChanId) : FilePos; (* If the channel is not open to a random access file, the exception wrongDevice is raised. Otherwise, returns the first position at or after which there have been no writes. *) PROCEDURE NewPos (cid : ChanId; chunks : INTEGER; chunkSize : CARDINAL; from : FilePos) : FilePos; (* If the channel is not open to a random access file, the exception wrongDevice is raised. Otherwise, returns the position chunks*chunkSize relative to the parameter from or raises the exception posRange if the required position cannot be represented as a value of type FilePos. *) PROCEDURE SetPos (cid : ChanId; pos : FilePos); (* If the channel is not open to a random access file, the exception wrongDevice is raised. Otherwise, sets the read/write position to the value given by the parameter pos. *) PROCEDURE Close (VAR cid : ChanId); (* If the channel is not open to a random access 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 RndFile.