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

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

On 28.10.15 19:20, Dmitry A. Kazakov wrote:
>> >If the assumptions are correct, but the compiler cannot determine
>> >their truth, should we hide the assumptions?
> As hide from the compiler? Certainly so! If as you said the compiler has no
> idea what your assumption is supposed to mean, how can it generate a useful
> code?

You mean, contract code needs to add value to *executables*
other than run-time tests?

I think the biggest misunderstanding here is in asking for
contracts to be considered just expressions, and then analyzing
them like they were *meant* to be ordinary expressions.

Even so, I think that an implementation of Ada could "outsource"
assertion checking to some read-only copy of the program that
is running on a twin processor, suitably connected, so as to
reduce run-time effects of assertion checking.

> If you force it, it generates garbage, which the semantics of dynamic
> predicates is, a garbage.

No, the compiler will be effecting the computation of a result
that does not need to be computed because we know it is true.
However, we wish to say that we know what the compiler does not
know, because a conjecture is being used as an assumption
when designing our subprogram, say.  If this assertion might
be checked at run-time due to some Assertion_Policy, then we
have to add a contraption,

     Some_Assertion =>
         Conjecture_X_To_Be_Assumed or else Conjecture_X (...);

So, if an algorithm is based on a conjecture, and we wish
to communicate what it is, precisely, a Boolean expression
allows us to do so. It documents our assumptions precisely.