markh@csd4.milw.wisc.edu (Mark William Hopkins) (06/17/88)
A notation is developed here to aid in representing the actions underlying the
basic file operations:
$ ~~~ READ buffer
# ~~~ WRITE buffer
@ ~~~ EOF
& ~~~ EOLN for text
A file can be in one of two modes, which I refer to here as the READ and WRITE
modes. In the read mode a file will generally look like:
A$ B@
where A and B denote a (possibly empty) string of file components. For example,
in the text file T:
'The end'& 'of the '$ 'line'& 'and file'&@
The file has the format:
The end
of the line
and file
with the file window located immediately after the $ (T^ = 'l')
A file in the WRITE mode has one of the two general forms:
<Buffer empty> A#
<Buffer full> A# x
where A is a (possibly empty) string of file components and x the file buffer.
--------------------------------------------------------------------------------
For convenience, the file operations are "functionalized":
get(F) becomes F := GET(F)
put(F) becomes F := PUT(F)
F^ := x becomes F := ADD(F, x)
write(F, x) becomes F := WRITE(F, x) ( or PUT(ADD(F, x)) )
read(F, x) becomes x := F^; F := PUT(F)
reset(F) becomes F := RESET(F)
rewrite(F) becomes F := REWRITE
Multiple read's and write's for text files are converted appropriately, e.g.
read(textA, X1, X2, X3)
becomes
read(textA, X1); read(textA, X2); read(textA, X3)
Likewise numerical I/O and string and boolean writes are converted into
procedures
ReadInt(F, x), ReadReal(F, x),
WriteInt(F, x:FW), WriteFloat(F, x:FW1), WriteFixed(F, x:FW1:FW2)
WriteBoolean(F, x:FW), WriteString(F, x:FW)
Example:
write(T, 'weeks.') becomes WriteString(T, 'weeks.')
which becomes:
write(T, 'w'); write(T, 'e'); ...; write(T, '.')
or
T := WRITE(T, 'w'); ...; T := WRITE(T, '.')
The eoln, readln and writeln's of text are converted into the following:
eoln(T) becomes T^ = &
readln(T) becomes while (T^ <> &) do T := GET(T);
T := GET(T)
writeln(T) becomes T := WRITE(T, &)
Through these means, everything all file operations can be reduced to the
functions WRITE, ADD, PUT, GET, RESET, REWRITE, ( )^ and eof.
--------------------------------------------------------------------------------
PUT: PUT(A#) : undefined buffer ADD: ADD(A#, x) = A# x
PUT(A# y) = Ay# ADD(A# y, x) = A# y
PUT(A$ B@) : wrong mode ADD(A$ B@, x) : wrong mode
WRITE: WRITE(F, x) = PUT( ADD(F, x) )
REWRITE = #
GET: GET(A#), GET(A# x) : wrong mode ( )^: (A#)^ : empty buffer
GET(A$ xB@) = Ax$ B@ (A# x)^ = x
GET(A$ @) : end of file read error (A$ xB@)^ = x
(A$ @)^ : end of file
RESET: RESET(A#) = $ A@ eof: eof(A#), eof(A# x) : wrong mode
RESET(A# x) = $ A@ eof(A$ xB@) = false
RESET(A$ B@) = $ AB@ eof(A$ @) = truebobdi@omepd (Bob Dietrich) (06/21/88)
Just glanced over your notes and have few comments: 1) What is the point you are trying to make? 2) Your notation bears a lot of similarity to the way files and operations on files are specified in the ANSI/ISO standards and in the Extended Pascal draft. There may be some similarity to the Axiomatic Definition, but I can't remember what was done there, and don't have a copy handy. 3) Files in the standards are specified as a triple consisting of a left sequence, a right sequence, and a mode. Mode is Inspection or Generation, corresponding to your READ and WRITE modes. Extended Pascal adds an Update mode. 4) Operations on files are stated in terms of pre and post-conditions on these triples. Usually these are axiomatic, with additional conditions (such as errors) stated in (standardese) English. 5) You might be careful in a couple of areas. One is that the ANSI and Extended Pascal interpretation is that for things like read, a "reference" is established to the file variable and then the operations performed. The intent is to have predictable behavior for things like read( f[i], i, j) where f is an array of files and i and j are variables. This is a possible problem with the expansions you suggest. The other potential problem area you may or may not have addressed is lazy I/O (actually, just I). The standards carefully leave this possibility open, which means that a processor may actually do external file operations (if that is what your file sequence is operating on) when eof or eoln is invoked. Again, this may not be a problem for your notation; I haven't looked very closely. 6) I don't believe you account for such things as the fact the file buffer is undefined after a put. Please don't construe these comments as negative. I am always pleased to see someone putting a little thought into a problem. I'm just trying to offer suggestions for improvements and point out similar work. Bob Dietrich Intel Corporation, Hillsboro, Oregon (503) 696-4400 or 2092(messages x4188,2111) usenet: tektronix!ogcvax!omepd!bobdi or tektronix!psu-cs!omepd!bobdi or ihnp4!verdix!omepd!bobdi