comp.lang.ada
 help / color / mirror / Atom feed
From: "Randy Brukardt" <randy@rrsoftware.com>
Subject: Re: Tests in a software release
Date: Thu, 16 Nov 2017 18:15:52 -0600
Date: 2017-11-16T18:15:52-06:00	[thread overview]
Message-ID: <oul9no$o8o$1@franka.jacob-sparre.dk> (raw)
In-Reply-To: oul0ra$jee$1@dont-email.me

"G.B." <bauhaus@notmyhomepage.invalid> wrote in message 
news:oul0ra$jee$1@dont-email.me...
> 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?

Because the real world is a nasty place where unexpected things go wrong. 
The fewer assumptions a human has to make, the the better. A computer 
program can handle making assumptions much better, because it can juggle 
many of them and will not get confused.




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

My blog was exclusively talking about language-defined constructs and 
checks. None of the rules described in the blog have any effect on 
user-defined operators (that is, ordinary function calls) because the 
compiler cannot know what the body does. Indeed, my entire discussion here 
has been about pragma Suppress and does not necessarily apply to 
user-defined contracts (that is, pragma Assertion_Policy as applies to 
things like Pre and Post).

There is absolutely no connection between pragma Suppress and pragma 
Assertion_Policy in Ada -- they work entirely differently 
(Assertion_Policy(Ignore) cannot by itself cause erroneous execution, while 
pragma Suppress almost always can).

A lot can be done with user-defined contracts, but that depends on contract 
aspects not defined in Ada 2012 (like Global, which hopefully will be in Ada 
2020). As you note correctly, timing issues might still require using 
Ignore, since it is easy to write very expensive predicates that cannot be 
left in a production system.

I believe that latter problem is a flaw in the contract system as written; 
most predicates are *not* expensive (think Is_Open in Text_IO) and thus have 
no need to be Ignored; it would be best if the occassional expensive 
predicate could be flagged and only those ignored. But again, none of that 
has anything to do with what I was discussing.

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

Never for language-defined checks; there is no point as any barely competent 
compiler will drop them automatically for free. If it can't drop them, it's 
highly likely that your code has a bug. User-defined contracts are a 
different deal; I'd prefer to never eliminate them, either, but I recognize 
that a few are going to be too expensive, and it's not as clear that the 
compiler will be able to optimize them (although in many cases, it will be 
able to do so to get sufficient performance).

...
>    if X /= X or else X /= X then
>
>       --  what, at compile time,
>       --  for which which kind of X?

This is dubious for *ANY* kind of X. This is just a warning because X might 
be something with a side-effect and thus this might actually mean something 
other than the nothing that it appears to mean -- but even in such a case, 
the code is clearly tricky and it would be better written some other way 
that is less tricky to a reader that doesn't necessarily know the details of 
X.

This is all explained in detail in the blog and I'm not sure why you are 
asking about it here.

                                              Randy.





  reply	other threads:[~2017-11-17  0:15 UTC|newest]

Thread overview: 39+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2017-10-25 19:30 Tests in a software release Victor Porton
2017-10-26  7:20 ` Dmitry A. Kazakov
2017-10-27 18:06   ` G. B.
2017-10-27 18:54     ` Dmitry A. Kazakov
2017-10-28  6:53       ` G.B.
2017-10-28  7:35         ` Dmitry A. Kazakov
2017-10-30 20:44           ` G. B.
2017-10-30 20:56             ` Dmitry A. Kazakov
2017-10-31  7:17               ` G.B.
2017-10-31  8:32                 ` Dmitry A. Kazakov
2017-11-03  7:24                   ` G.B.
2017-11-03  8:16                     ` Dmitry A. Kazakov
2017-11-03 12:49                     ` Shark8
2017-11-04 10:15                       ` G.B.
2017-11-15  0:11                     ` Randy Brukardt
2017-11-15 17:57                       ` G. B.
2017-11-15 20:46                         ` Dmitry A. Kazakov
2017-11-17 15:36                           ` Shark8
2017-11-15 22:17                         ` Randy Brukardt
2017-11-16 21:44                           ` G.B.
2017-11-17  0:15                             ` Randy Brukardt [this message]
2017-11-17 15:45                             ` Shark8
2017-11-18  1:07                               ` Randy Brukardt
2017-11-15  0:06                   ` Randy Brukardt
2017-11-15  8:47                     ` Dmitry A. Kazakov
2017-11-15 21:53                       ` Randy Brukardt
2017-11-15 16:47                     ` Jeffrey R. Carter
2017-11-15 16:59                       ` J-P. Rosen
2017-11-15 20:45                         ` Dmitry A. Kazakov
2017-11-15 21:58                         ` Randy Brukardt
2017-11-16  5:50                           ` J-P. Rosen
2017-11-16 23:53                             ` Randy Brukardt
2017-11-15  0:01                 ` Randy Brukardt
2017-11-16 17:02           ` Robert Eachus
2017-11-17  0:20             ` Randy Brukardt
2017-11-22 20:40               ` Robert Eachus
2017-11-14 23:55       ` Randy Brukardt
2017-10-26  8:09 ` Stefan.Lucks
2017-10-26 17:30 ` Simon Clubley
replies disabled

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox