From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-0.3 required=5.0 tests=BAYES_00,
	REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!mx02.eternal-september.org!.POSTED!not-for-mail
From: Georg Bauhaus <bauhaus@futureapps.invalid>
Newsgroups: comp.lang.ada
Subject: Re: function Is_Open (File : File_Type) return Boolean; :Text_io
Date: Sat, 31 Oct 2015 12:17:37 +0100
Organization: A noiseless patient Spider
Message-ID: <n127se$qnv$1@dont-email.me>
References: <f30bbb5d-ebfd-427b-8c16-88aeb8a61318@googlegroups.com>
 <87twpd2qlo.fsf@theworld.com> <1pj15r7pul7f1.15qgdyrc8k133$.dlg@40tude.net>
 <87pp0030c1.fsf@theworld.com> <135hiczk56x02.1xixcme8btbl4.dlg@40tude.net>
 <n0o9fb$3pq$2@dont-email.me> <1dzlgoh4u2j7t$.1un3dfy0oeigd$.dlg@40tude.net>
 <n0qa3q$th8$1@dont-email.me> <190shqocxd87d$.1d68ghgqgbvfs$.dlg@40tude.net>
 <n0t0t1$56e$1@dont-email.me> <19ihs115mzocg$.20s63jo0q2gf.dlg@40tude.net>
 <n0ufn3$e6$1@dont-email.me> <2qwfwnugm5q5.ajan0n5midql$.dlg@40tude.net>
 <n0vutc$hu6$1@dont-email.me> <18wdhboc0r4aj$.1rj6n8wv3scfd.dlg@40tude.net>
 <n10f12$96c$1@dont-email.me> <b0qn4s2ievhr.qfoi16ezp3o0.dlg@40tude.net>
Reply-To: nonlegitur@futureapps.de
Mime-Version: 1.0
Content-Type: text/plain; charset=windows-1252; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Sat, 31 Oct 2015 11:15:26 -0000 (UTC)
Injection-Info: mx02.eternal-september.org;
 posting-host="dee7f4689d1ae51229155cca7cef0a10";
	logging-data="27391"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX19JMdNzDFtmigylsGcyxdWq2PfEDK5B2yM="
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9; rv:38.0)
 Gecko/20100101 Thunderbird/38.3.0
In-Reply-To: <b0qn4s2ievhr.qfoi16ezp3o0.dlg@40tude.net>
Cancel-Lock: sha1:P3JC7iBL7kaniLF9VzTMix40DTw=
Xref: news.eternal-september.org comp.lang.ada:28147
Date: 2015-10-31T12:17:37+01:00
List-Id: <comp.lang.ada>

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.