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

["G.B." <bauhaus@futureapps.invalid>]

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.