comp.lang.ada
 help / color / mirror / Atom feed
From: Georg Bauhaus <rm.dash-bauhaus@futureapps.de>
Subject: Re: Generic-Package Elaboration Question / Possible GNAT Bug.
Date: Wed, 23 Nov 2011 00:52:23 +0100
Date: 2011-11-23T00:52:24+01:00	[thread overview]
Message-ID: <4ecc35b8$0$7628$9b4e6d93@newsspool1.arcor-online.net> (raw)
In-Reply-To: <12hfiflyf7pr5$.l3pkpgoid8xt$.dlg@40tude.net>

On 22.11.11 20:15, Dmitry A. Kazakov wrote:

>> Meyer: "Programming is a human activity".
>> Programmers are led towards a solution during the process of programming.
>> Depending on the characteristics of the process, then,
>> programmers will produce different results.
>
> I see no word "debugging" there.

A debugging aid is a means of finding mistakes when developing programs.
Trying to write assertions pre/post/inv for types and their primitive operations
is a means of finding mistakes (bugs) at a number of stages during program
development. At one stage, I will state the intended effect of operations
on visible object state. At another stage, I might want to know why a
subprogram has failed to establish its postcondition and raised.
Answering the questions revolves around the very same subject.
(It will be cool to make "permissible input" to a subprogram a consequence
of 'Valid; is it practical?)

Then, evaluation of the conditionals may or may not happen (depending on
settings like Assertion_Policy). The intent is to prod programmers into trying
harder with one specific goal: to render the conditionals a *consequence*
of the program (without assertions), a redundancy, rather than a part
of it.  A non-trivial consequence that reflects the intent. A non-trivial
consequence of a suitable corrected program.
When this is achieved, assertions not only will not negatively affect any
execution of the program, they also document programmers' intent which
is otherwise lost in mere implications, obscure comments, unspoken.

>
>> DbC (TM), as a characteristic of a process, leads to products
>> that lend themselves to proving them correct more than others,
>> provided this is possible.
>
> I suppose drinking coffee does that as well.

No, coffee is not known to yield better manifestations of intended
subprogram behavior in source text, certainly not better than specifying
conditions (program states) framing possible executions.  Coffee can have
rather obfuscating long term effects, in particular when spilt.


> I my experience at least 40% of my debugging
> efforts in Ada 95 was spent on catching accessibility checks faults. Ada
> 2005 improved that greatly. To me this is a vivid example why dynamic
> checks are evil.

One may prefer static checks and still want dynamic checks for
cases where static checks are not within reach of any tool
known to man.


> You have to specify the failures you are going to notice.

DbC (TM) suggests that you specify the set of states
that a program can reach if both the program

(a) is started from some state in a set of given states and

(b) if all goes well.

You do not specify what happens if not both (a) and (b).

(Hence,  trying alternatives, organized panic, or hoping for
false alarm if not both (a) and (b). Rescue clauses are a
there to assist the brave only.)

> Once
> you do qualify them, you would easily be able to avoid them.

Yes.

> Note that all
> the buzz is about noticing something unanticipated.

If a description of possible program states in not exhaustive,
then, nevertheless, this description establishes a non-empty set
of states, and another non-empty set, its complement.
When a state is found to be in the complement,
then I'd like to know this, even when this knowledge just teaches me
that my original attempt at specifying conditions was wrong.
I'm told by way of an exception raised.

>>> The software which behavior is unknown shall never be executed.
>>
>> But this is impossible, in general!
>
> I see the point, since it is impossible do right, you are going to do it
> wrong. I am not arguing for or against your or Meyer's motivations. I only
> state that it is wrong.

You do use compilers, and since it is impossible to know their behavior in
general, are you doing wrong?

There is no right or wrong in most programs. There is only I/O
that satisfies users. I can try to do it right, locally.
I'll try to make programs as good as possible.
As part of this effort, I can state my expectations of how the
subprograms should behave. This may be universally wrong,
improved types might be better, but should I do nothing because
something is wrong in principle?  At least I'm not allowed to
follow that path because of deadlines. :-)





  parent reply	other threads:[~2011-11-22 23:52 UTC|newest]

Thread overview: 86+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2011-11-19 21:14 Generic-Package Elaboration Question / Possible GNAT Bug Shark8
2011-11-19 22:12 ` Robert A Duff
2011-11-19 23:36   ` Shark8
2011-11-20  9:55     ` Dmitry A. Kazakov
2011-11-21  7:25       ` AdaMagica
2011-11-21  8:43         ` Dmitry A. Kazakov
2011-11-21 10:25           ` AdaMagica
2011-11-21 13:08           ` Robert A Duff
2011-11-21 13:50             ` Dmitry A. Kazakov
2011-11-21 19:41               ` Robert A Duff
2011-11-22  8:21                 ` Dmitry A. Kazakov
2011-11-21 20:40               ` J-P. Rosen
2011-11-22  8:29                 ` Dmitry A. Kazakov
2011-11-22 10:25                   ` Georg Bauhaus
2011-11-22 14:32                     ` Dmitry A. Kazakov
2011-11-22 15:02                       ` Georg Bauhaus
2011-11-22 16:23                         ` Dmitry A. Kazakov
2011-11-22 17:46                           ` Georg Bauhaus
2011-11-22 19:15                             ` Dmitry A. Kazakov
2011-11-22 21:03                               ` Randy Brukardt
2011-11-22 21:26                                 ` Dmitry A. Kazakov
2011-11-23  0:07                                   ` Georg Bauhaus
2011-11-23  8:44                                     ` Dmitry A. Kazakov
2011-11-23  9:32                                       ` Simon Wright
2011-11-23  9:56                                         ` Dmitry A. Kazakov
2011-11-23 11:03                                           ` Georg Bauhaus
2011-11-23 11:13                                             ` Dmitry A. Kazakov
2011-11-23 11:25                                               ` Georg Bauhaus
2011-11-23 13:14                                                 ` Dmitry A. Kazakov
2011-11-23 13:59                                                   ` Georg Bauhaus
2011-11-23 14:43                                                     ` Dmitry A. Kazakov
2011-11-23 16:10                                                       ` Georg Bauhaus
2011-11-23 19:51                                                         ` Dmitry A. Kazakov
2011-11-24  0:59                                                           ` Georg Bauhaus
2011-11-24  9:14                                                             ` Dmitry A. Kazakov
2011-11-23 15:12                                           ` Simon Wright
2011-11-23 19:53                                             ` Dmitry A. Kazakov
2011-11-24  8:07                                               ` Simon Wright
2011-11-24  9:27                                                 ` Dmitry A. Kazakov
2011-11-24 10:49                                                   ` Georg Bauhaus
2011-11-24 13:14                                                     ` Dmitry A. Kazakov
2011-11-24 14:31                                                       ` Georg Bauhaus
2011-11-24 16:32                                                         ` Dmitry A. Kazakov
2011-11-24 11:15                                                 ` Brian Drummond
2011-11-24 18:12                                                   ` Simon Wright
2011-11-24 23:52                                                     ` Brian Drummond
2011-11-23 10:35                                         ` Brian Drummond
2011-11-23  9:54                                       ` Georg Bauhaus
2011-11-23 10:30                                         ` Dmitry A. Kazakov
2011-11-23  4:08                                 ` Yannick Duchêne (Hibou57)
2011-11-23  4:11                                 ` Yannick Duchêne (Hibou57)
2011-11-22 23:52                               ` Georg Bauhaus [this message]
2011-11-23  9:04                                 ` Dmitry A. Kazakov
2011-11-23 11:15                                   ` Georg Bauhaus
2011-11-23 13:30                                     ` Dmitry A. Kazakov
2011-11-23 14:42                                       ` Georg Bauhaus
2011-11-23 19:48                                         ` Dmitry A. Kazakov
2011-11-24  1:36                                           ` Georg Bauhaus
2011-11-24 10:52                                             ` Dmitry A. Kazakov
2011-11-24 11:30                                               ` Georg Bauhaus
2011-11-24 12:52                                                 ` Dmitry A. Kazakov
2011-11-24 14:45                                                   ` Georg Bauhaus
2011-11-25  9:54                                                     ` Dmitry A. Kazakov
2011-11-24  7:46                                           ` stefan-lucks
2011-11-24  3:07                           ` Shark8
2011-11-24  6:07                             ` Yannick Duchêne (Hibou57)
2011-11-24 10:10                             ` Dmitry A. Kazakov
2011-11-24 11:15                               ` Georg Bauhaus
2011-11-24 22:48                               ` Shark8
2011-11-25  9:25                                 ` Yannick Duchêne (Hibou57)
2011-11-26 21:59                                   ` Shark8
2011-11-25  9:47                                 ` Dmitry A. Kazakov
2011-11-25 10:15                                   ` Georg Bauhaus
2011-11-25 10:51                                     ` Yannick Duchêne (Hibou57)
2011-11-25 15:45                                   ` Georg Bauhaus
2011-11-25 16:05                                     ` Yannick Duchêne (Hibou57)
2011-11-25 16:19                                     ` Yannick Duchêne (Hibou57)
2011-11-23  3:49                         ` Yannick Duchêne (Hibou57)
2011-11-23  8:50                           ` Georg Bauhaus
2011-11-23  9:45                             ` Yannick Duchêne (Hibou57)
2011-11-23 10:55                               ` Georg Bauhaus
2011-11-23  3:20             ` Yannick Duchêne (Hibou57)
2011-11-23 15:05               ` Robert A Duff
2011-11-21 17:00 ` Adam Beneschan
2011-11-23  3:13 ` Yannick Duchêne (Hibou57)
2011-11-24  3:47   ` Shark8
replies disabled

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