File handling procedures

Except for the application of rewrite or reset to the program parameters denoted by input or output, the effects of applying each of the file handling procedures rewrite, put, reset, and get to a file-variable f shall be defined by pre-assertions and post-assertions about f, its components f.L, f.R, and f.M, and the associated buffer-variable f­. The use of the variable f0 within an assertion shall be considered to represent the state or value, as appropriate, of f prior to the operation, while f (within an assertion) shall denote the variable after the operation, and similarly for f0­ and f­.

It shall be an error if the stated pre-assertion does not hold immediately prior to any use of the defined operation. It shall be an error if any variable explicitly denoted in an assertion of equality is undefined. The post-assertion shall hold prior to the next subsequent access to the file, its components, or its associated buffer-variable. The post-assertions imply corresponding activities on the external entities, if any, to which the file-variables are bound. These activities, and the point at which they are actually performed, shall be implementation-defined.

NOTE --- In order to facilitate interactive terminal input and output, the procedure get (and other input procedures) should be performed at the latest opportunity, and the procedure put (and other output procedures) should be performed at the first opportunity. This technique has been called 'lazy I/O'.

rewrite(f)

pre-assertion: true.

post-assertion: (f.L = f.R = S( )) and (f.M = Generation) and (f­ is totally-undefined).

put(f)

pre-assertion: (f0.M = Generation) and (f0.L is not undefined) and (f0.R = S( )) and

(f0­ is not undefined).

post-assertion: (f.M = Generation) and (f.L = (f0.L ~S(f0­)) ) and (f.R = S( )) and

(f­ is totally-undefined).

reset(f)

pre-assertion: The components f0.L and f0.R are not undefined.

post-assertion: (f.L = S( )) and (f.R = (f0.L ~f0.R ~X)) and (f.M = Inspection) and

(if f.R = S( ) then (f­ is totally-undefined) else (f­ = f.R.first)),

where, if f possesses the type denoted by the required type-identifier text and if f0.L ~f0.R is not empty and if (f0.L ~f0.R).last is not an end-of-line, then X shall be a sequence having an end-of-line component as its only component; otherwise, X = S( ).

get(f)

pre-assertion: (f0.M = Inspection) and (neither f0.L nor f0.R is undefined) and (f0.R <> S( )).

post-assertion: (f.M = Inspection) and (f.L = (f0.L ~ S(f0.R.first))) and (f.R = f0.R.rest)

and (if f.R = S( ) then (f­ is totally-undefined) else (f­= f.R.first)).

When the file-variable f possesses a type other than that denoted by text, the required procedures read and write shall be defined as follows.

read

Let f denote a file-variable and v₁,...,v_n denote variable-accesses (n>=2); then the procedure-statement read(f,v₁ ,...,v_n) shall access the file-variable and establish a reference to that file-variable for the remaining execution of the statement. The execution of the statement shall be equivalent to

begin read(ff,v₁); read(ff,v₂,...,v_n) end

where ff denotes the referenced file-variable.

Let f be a file-variable and v be a variable-access; then the procedure-statement read(f,v) shall access the file-variable and establish a reference to that file-variable for the remaining execution of the statement. The execution of the statement shall be equivalent to

begin v := ff­; get(ff) end

where ff denotes the referenced file-variable.

NOTE --- The variable-access is not a variable parameter. Consequently, it may be a component of a packed structure, and the value of the buffer-variable need only be assignment-compatible with it.

write

Let f denote a file-variable and e₁ ,...,e_n denote expressions (n>=2); then the procedure-statement write(f,e₁ ,...,e_n) shall access the file-variable and establish a reference to that file-variable for the remaining execution of the statement. The execution of the statement shall be equivalent to

begin write(ff,e₁); write(ff,e₂ ,...,e_n) end

where ff denotes the referenced file-variable.

Let f be a file-variable and e be an expression; then the procedure-statement write(f,e) shall access the file-variable and establish a reference to that file-variable for the remaining execution of the statement. The execution of the write statement shall be equivalent to

begin ff­ := e; put(ff) end

where ff denotes the referenced file-variable.

NOTES

1 The required procedures read, write, readln, writeln, and page, as applied to textfiles, are described in 6.10.

2 Since the definitions of read and write include the use of get and put, the implementation-defined aspects of their post-assertions also apply.

3 A consequence of the definition of read and write is that the non-file parameters are evaluated in a left-to-right order.

Date: 2015-12-24; view: 1036