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

[Georg Bauhaus <bauhaus@futureapps.invalid>]

On 31.10.15 10:31, Dmitry A. Kazakov wrote:

>>>>  Which kind of program is relied upon to determine
                                ^^^^^^
>>>> if it has bugs or not?
>>>
>>> A program that contains run-time checks for bugs.
>>
>> I don't think anybody says that, nor does "contract based design",

Let me put the essential piece back in, the one that you didn't quote:

   “not the part with "relying"!”

> Thus:
>
> "Detecting a false positive needs to be assessed empirically."
>
> reads as
>
> "Somebody needs empirically assess misinterpretation of desired outcomes as
> undesired outcomes..."

Somebody *will* say "This effect was not intended!", after the fact.

(If you could leave the bits in that make clear how a single correct
interpretation before the fact might not exist (when static properties
of programs (to be) are insufficient as a basis for drafting contracts)
...)

> May I suggest, for a start, do not misinterpret anything, then you won't
> need to assess that later... (:-))

So, how do we make sure that we do not misinterpret anything?

By not saying anything, I guess, if Boolean expressions should
not be asserted unless our favorite PL's compiler can handle them
at compile time. Is that right?

(Again, program A is a template.)

> Any non-contradictory definition [of correct program] is workable.

Why?

(Again, program A is a template, no consistency issues.)

>> Except per the narrow situation-excluding circularity of
>> "work" = "operation":
>
> Workable here = logically consistent.

How did the program in Ariane IV logically rest on inconsistency
within it, then? How did its "contract" fail at compile time?

Static properties of programs do not exhaust the material which is
typically put in contracts. Work is done using unknowns, every day.

Conquering the word "contract" to mean nothing but formal semantics
of programs conveniently removes its usual meaning.

It also removes programming techniques that have been seen
to be useful and efficient.