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!feeder.eternal-september.org!.POSTED!not-for-mail
From: "G.B." <bauhaus@notmyhomepage.invalid>
Newsgroups: comp.lang.ada
Subject: Re: Tests in a software release
Date: Thu, 16 Nov 2017 22:44:21 +0100
Organization: A noiseless patient Spider
Message-ID: <oul0ra$jee$1@dont-email.me>
References: <osqoph$1ves$1@gioia.aioe.org> <oss2c3$1p2m$1@gioia.aioe.org>
 <osvsjs$t4b$1@dont-email.me> <osvvds$s97$1@gioia.aioe.org>
 <ot19fo$7mi$2@dont-email.me> <ot1bvm$ub7$1@gioia.aioe.org>
 <ot82v3$h2c$1@dont-email.me> <ot83l0$1rb1$1@gioia.aioe.org>
 <ot981s$7m5$1@dont-email.me> <ot9cfr$1k6s$1@gioia.aioe.org>
 <oth5k4$eih$1@dont-email.me> <oug0n1$h7m$1@franka.jacob-sparre.dk>
 <ouhv6m$cig$1@dont-email.me> <ouiedt$gd1$1@franka.jacob-sparre.dk>
Reply-To: nonlegitur@notmyhomepage.de
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Thu, 16 Nov 2017 21:44:10 -0000 (UTC)
Injection-Info: reader02.eternal-september.org;
 posting-host="277ae01b66849e6deb695aefb25f18fb";
	logging-data="19918"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX184VKfNmfQ19j5hIOBtEJGxn0P13x8Ah6M="
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.12; rv:52.0)
 Gecko/20100101 Thunderbird/52.4.0
In-Reply-To: <ouiedt$gd1$1@franka.jacob-sparre.dk>
Content-Language: en-US
Cancel-Lock: sha1:qZin47VNYL2pmPqjNj/a2/WwWIk=
Xref: feeder.eternal-september.org comp.lang.ada:48939
Date: 2017-11-16T22:44:21+01:00
List-Id: <comp.lang.ada>

On 15.11.17 23:17, Randy Brukardt wrote:

> ...
>> The most important thing is, designing by contract
>> is *not* programming defensively. By definition.
> 
> One *always* programs defensively.

Why would that be?

FTR, and for what the definitions are,
  http://se.ethz.ch/~meyer/publications/computer/contract.pdf

Referring to some notes from your blog, you cannot always

   - compute things at compile time, hoping to optimize;
   - perform run-time checks in a timely fashion, without
     checks causing timeouts:

     function Binary_Search (X : List_of_Things) return Thing;
     --  ... provided that elements of X are ordered by "<=".
  

     procedure Foo (X : Graph; P : Node_Process);
     --  ... provided that X is a DAG.


Is_Sorted can be expressed in Ada, but the compiler cannot
prove this at run-time, foreseeing data that are becoming
available only then. It has no say, at that point.

Similarly, Is_Dag cannot be computed at compile time.
Checking Is_Dag at run-time will be prohibitively
expensive at Foo's end. Still checking is Bad Design, as
Dmitry might possibly put it, I guess, because a DAG is
a DAG by construction. At run-time.

So, what needs to be done and what is usually done
is that clients will be sure to call subprograms
passing sorted lists and passing DAGs, resp. No checks,
no defenses, just doing what the contract says we should.

So, while no compiler can eliminate the computations for
the reasons stated ("optimize"), we can if our code abides,
by *not* having Binary_Search *check* proper ordering.

Thus, your future compiler could not "demonstrate likely
bugs" for these contracts, but if the optimizer fails at
predicting all run-time values in X and therefore adds checks,
it likely prevents efficient real-time computation for the
contracts outlined above.

> In any case, this is the exact opposite of the sort of approach that you are
> championing.

On the contrary: you write the contract's clauses of
all parties to your compiler and then, once you
know your code meets the requirements of the contracts,
you drop checking code accordingly ("optimize") and in
good conscience.

    if X /= X or else X /= X then

       --  what, at compile time,
       --  for which which kind of X?