From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00
	autolearn=unavailable autolearn_force=no version=3.4.4
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!mx02.eternal-september.org!.POSTED!not-for-mail
From: Bob Duff <bobduff@theworld.com>
Newsgroups: comp.lang.ada
Subject: Re: function Is_Open (File : File_Type) return Boolean; :Text_io
Date: Tue, 27 Oct 2015 09:30:54 -0400
Organization: A noiseless patient Spider
Message-ID: <87pp0030c1.fsf@theworld.com>
References: <f30bbb5d-ebfd-427b-8c16-88aeb8a61318@googlegroups.com>
	<87twpd2qlo.fsf@theworld.com>
	<1pj15r7pul7f1.15qgdyrc8k133$.dlg@40tude.net>
Mime-Version: 1.0
Content-Type: text/plain
Injection-Info: mx02.eternal-september.org;
 posting-host="ff390eae7dae78eb85daece3eef8a589";
	logging-data="21954"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX18boCQcvkbTc/4LUrCxq/Gq"
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/24.3 (gnu/linux)
Cancel-Lock: sha1:pEranLzrxvDSWQFVjNsi3ooRMiI=
	sha1:kTJtfK3WNaOIGmutaKIy0RdPm0U=
Xref: news.eternal-september.org comp.lang.ada:28073
Date: 2015-10-27T09:30:54-04:00
List-Id: <comp.lang.ada>

"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.

> Looks entirely useless to me.

- Bob