DEFINITION MODULE StreamFile; (* Independent sequential data streams *) 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 Open (VAR cid : ChanId; name : ARRAY OF CHAR; flags : FlagSet; VAR res : OpenResults); (* Attempts to obtain and open a channel connected to a sequential stream file without the write flag, read is implied; the read flag implies old; without the raw flag, text is implied. If successful, assigns to the parameter cid the identity of a channel open to a source/destination of the given name and assigns the value opened to the parameter res. If a channel cannot be opened as required, the value of the parameter res indicates the reason and cid identifies the bad channel. *) PROCEDURE IsStreamFile (cid : ChanId) : BOOLEAN; (* Tests if the channel is open to a sequential stream *) PROCEDURE Close (VAR cid : ChanId); (* If the channel is not open to a sequential stream, the exception wrongDevice is raised. Otherwise, the channel is closed and the value identifying the bad channel is assigned to the parameter cid. *) END StreamFile.