From: "Gerry Butler" To: Cc: Subject: RE: EiffelBase/2681 Date: Wed, 11 Oct 2000 09:34:51 +1000 This is a multi-part message in MIME format. ------=_NextPart_000_0000_01C03366.81324510 Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: 7bit Good morning I think I forgot to include the attachment with my original bug report. Here it is. Gerry ------=_NextPart_000_0000_01C03366.81324510 Content-Type: text/plain; name="read_x_precondition.txt" Content-Transfer-Encoding: quoted-printable Content-Disposition: attachment; filename="read_x_precondition.txt" There seems to be a problem with the preconditions of the = read_character,=20 read_integer, etc features in FILE. The problem occurs when you = inadvertently=20 attempt to read a file that has been opened only for writing. You would = expect=20 the precondition to detect the error, but it doesn't. Instead, it fails=20 later with an I/O error. Preconditions of 'read_x' features of FILE are ineffective =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D 'read_x' features inherit the precondition 'readable' from IO_MEDIUM. They add their own precondition 'file_readable'. 'file_readable' is introduced in FILE as: file_readable: BOOLEAN is do Result :=3D (mode >=3D Read_Write_file or mode =3D Read_file) and = readable end 'readable' is deferred in IO_MEDIUM and effected in FILE by the inheritance of 'readable' from SEQUENCE. The precondition of 'read_x' in FILE evaluates as: (precondition of IO_MEDIUM) or else (precondition of FILE) That is: (readable) or else ((mode >=3D Read_Write_file or mode =3D Read_file) = and readable) Therefore, '(mode >=3D Read_Write_file or mode =3D Read_file)' has no = effect. That is, 'read_x' features of FILE have preconditions that evaluate to: 'readable'=20 'read_x' features of FILE cannot fulfill the contracts they inherit from = IO_MEDIUM =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D Consider an open file containing at least 1 character, whose mode is = 'Write_file'. 'readable' is effected in SEQUENCE as: readable: BOOLEAN is do Result :=3D not off end 'off' is effected in FILE as: off: BOOLEAN is do Result :=3D (count =3D 0) or else is_closed or else end_of_file end Therefore 'readable' is True. ('file_readable' is False, but this is irrelevant.) Therefore, 'read_x' preconditions are fulfilled. But any attempt to read the file passes the precondition but fails in = 'read_x' with: Class: PLAIN_TEXT_FILE Feature: read_character (From FILE) Reason: Explicit exception pending Code: 27 (I/O error.) Tag: FILE: unable to read CHARACTER value. Note that FILE inherits an invariant from ACTIVE: writable implies readable. However, in FILE, the following does not hold: file_writable implies file_readable Suggested solution =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D The following may not be the only solution, or the best solution: In FILE, rename 'readable' from IO_MEDIUM as 'file_readable', then remove the 'require else' clauses from 'read_x' features. Questions =3D=3D=3D=3D=3D=3D=3D=3D=3D Is there a similar problem with the 'put_x' features of FILE? Does the suggested solution have any impact on TCP/IP streams and other descendents of IO_MEDIUM? ------=_NextPart_000_0000_01C03366.81324510--