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

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

On Fri, 30 Oct 2015 02:06:43 +0100, Georg Bauhaus wrote:

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

Because contracts describe programs.

> I saw picking a universe that suffers from failure
> to respond usefully to some runs of programs failing, even in some
> expected way.

Yes, and the salary is far too low, did I even mention weather? Horrible!

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

Only because you call contracts things which are not. Naming is no problem,
which is that any usefulness of contracts is based on clear distinction to
the program itself. Once you confuse them you have no contracts, just
poorly designed implementations. Poorly because considering them
non-behavior, you don't pay attention to what they cause (and they surely
do) at run-time. It is just a lazy self-indulgent way of design, not much
different from C's approach.

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

Universe is an extremely boring place, if you look at it.

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

It does not because documentation is informal. Things you can describe
formal, you do. The rest goes into documentation.

> Also how, if not using either the contract or the program.

As an old saying say: if nothing else helps read the documentation.

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

The concern is safe design. If B has bugs it cannot be relied on to
determine if it has them.

> Anyway, if a Rational R-1000 did perform checks on a coprocessor,

Checks are not necessarily correctness checks. There is nothing incorrect
in subscript error or zero divide without further assumptions about the
problem space array or number is used to model.

> perhaps we just need another word? So that we could say
> "formal description of program(s)"

"formal description of program" is the program itself. A programming
language is a formal one. A sentence in this language is a description of a
program (meaning: set of actions) to execute.

> when we mean it and use "contract"
> instead for what seems to be its "other" meaning?

"contract" is a formal description of a *set* of programs or their parts.
It specifies desired properties of shared by all these programs, the
properties other programs can rely on. E.g. Dynamic Is_Open predicate is
not a contract, because you cannot rely on it. It is just a part of the
program itself, misplaced in the declarative region.

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