Re: function Is_Open (File : File_Type) return Boolean; :Text_io

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Tue, 27 Oct 2015 09:30:54 -0400, Bob Duff wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
> 
>> On Mon, 26 Oct 2015 18:48:51 -0400, Bob Duff wrote:
>>
>>> comicfanzine@gmail.com writes:
>>> 
>>>> Can someone please show my a code in which this function is used , i'm
>>>> lost , thanks .
>>> 
>>> Most code is written so that it is statically known whether a file is
>>> open, so Is_Open is close to useless.  Not entirely useless -- you might
>>> use it in an assertion, such as:
>>> 
>>>     subtype Open_File is File with Predicate => Is_Open(Open_File);
>>
>> In order to have the Constraint_Error exception instead of Status_Error?
> 
> No, in order to document the fact that a certain formal parameter must
> be open, and in order to prove things statically.  If a procedure takes
> "F: Open_File", then we can easily prove that writes to F within that
> procedure do not raise Status_Error.

That does not make sense either. There is nothing in the procedure itself 
that would prevent raising Status_Error. Everything is on the caller's 
side. How do you know if some callers would not appreciate Status_Error as 
a possible outcome? Looks like poor design to me.

Anyway proving either of the conditions A) not raising Constraint_Error, B) 
not raising Status_Error look equally hard.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de