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=-0.3 required=5.0 tests=BAYES_00,
	REPLYTO_WITHOUT_TO_CC autolearn=no 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: "G.B." <bauhaus@futureapps.invalid>
Newsgroups: comp.lang.ada
Subject: Re: function Is_Open (File : File_Type) return Boolean; :Text_io
Date: Tue, 27 Oct 2015 15:00:07 +0100
Organization: A noiseless patient Spider
Message-ID: <n0nvsr$ss6$1@dont-email.me>
References: <f30bbb5d-ebfd-427b-8c16-88aeb8a61318@googlegroups.com>
 <87twpd2qlo.fsf@theworld.com> <1pj15r7pul7f1.15qgdyrc8k133$.dlg@40tude.net>
 <87pp0030c1.fsf@theworld.com>
Reply-To: nonlegitur@futureapps.de
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Tue, 27 Oct 2015 13:57:47 +0000 (UTC)
Injection-Info: mx02.eternal-september.org;
 posting-host="b96887e80893c84a90c3007226ca0d1c";
	logging-data="29574"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX192azKdABzvwyfEDsndj76LATQI2UMiPfE="
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.10; rv:38.0)
 Gecko/20100101 Thunderbird/38.3.0
In-Reply-To: <87pp0030c1.fsf@theworld.com>
Cancel-Lock: sha1:2k6XmElrdTP+7BpBR9hzmZiSJbw=
Xref: news.eternal-september.org comp.lang.ada:28074
Date: 2015-10-27T15:00:07+01:00
List-Id: <comp.lang.ada>

On 27.10.15 14:30, Bob Duff wrote:
> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:

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

A big Thank You for providing a example of the usefulness of predicates!

The part that refers to formally "documenting" what is expected,
be it expressible in the static type system or not, deserves more
attention IMHO. (Not every project has the time and money
for fully analyzing and transforming programs until the compiler
is capable of tackling everything before run-time. Does anyone
expect all possible and reasonable Boolean expressions to be
statically computable in the near future? Are they therefore
useless?)

Meyer has recently communicated that understanding classes means
to know the classes' contracts. This reminded me of a similar
effect ascribed to unit tests.