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

[Georg Bauhaus <bauhaus@futureapps.invalid>]

On 29.10.15 15:00, Dmitry A. Kazakov wrote:

> Contracts may have no effect on program execution.

(Must have no effect?)

Did I miss why? I saw picking a universe that suffers from failure
to respond usefully to some runs of programs failing, even in some
expected way. There was also the assumption of the existence of a
single allowed run-time effect for each pair <source program, input>.

Naturally, contracts will have no effect at run-time when tools and
brains are capable of demonstrating that all assertions will always
be true. For me, this is just a dream.

>  Consider this:
>
> program describes execution
> contract describes program(s)
> documentation describes anything

Yes, the definitions look like the rattling machinery of clean room
program analysis and fully informed decision making.

HOMER: (stands up) "Boring!"

I think the third line (documentation describing *anything*) is troublesome,
in part because the generality might lead to a paradox, and because it
remains unclear to me if documentation describes program(s) or execution.
Also how, if not using either the contract or the program.

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

There is no program A, as A is a template. Instances (for runs) are
created when choosing an Assertion_Policy, or levels of optimization,
say. If levels of optimization may change formal semantics (11.6 IIUC),
then why is optimization o.K., but controlling assertion checking is not?
Just because of some thin, formal, logical concern that contracts pushing
us into the morass of recursion is as problematical as most programming?

Anyway, if a Rational R-1000 did perform checks on a coprocessor,
perhaps we just need another word? So that we could say
"formal description of program(s)" when we mean it and use "contract"
instead for what seems to be its "other" meaning?