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

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

On Thu, 29 Oct 2015 12:47:48 +0100, G.B. wrote:

> 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 mean that something unknown is, well, unknown.

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

Yes. Contracts may have no effect on program execution. Consider this:

program describes execution
contract describes program(s)
documentation describes anything

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

We discussed that earlier. You can have program A asserting program B. You
never can do this in a single program. That is inconsistent.

Any execution effects of A are not of B. Thus, as before, assertion has no
run-time effect on B. Nothing changed.

When you put A into B, that is automatically broken.

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

Either the program raises exception or it does not.

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