comp.lang.ada
 help / color / mirror / Atom feed
From: "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>
Subject: Re: Generic-Package Elaboration Question / Possible GNAT Bug.
Date: Tue, 22 Nov 2011 17:23:30 +0100
Date: 2011-11-22T17:23:30+01:00	[thread overview]
Message-ID: <vagow98uvk3n$.198v2ms719j4e$.dlg@40tude.net> (raw)
In-Reply-To: 4ecbb96e$0$6581$9b4e6d93@newsspool3.arcor-online.net

On Tue, 22 Nov 2011 16:02:06 +0100, Georg Bauhaus wrote:

> On 22.11.11 15:32, Dmitry A. Kazakov wrote:
>> On Tue, 22 Nov 2011 11:25:59 +0100, Georg Bauhaus wrote:
>> 
>>> On 22.11.11 09:29, Dmitry A. Kazakov wrote:
>>>>  I think that a solution is not in adding new sources of
>>>> exceptions, but by making exceptions contracted (using conditional
>>>> contracts, e.g. "I don't raise, if you don't", "I don't raise if there is N
>>>> units of memory free" etc).
>>>
>>> I think that, with the exception of compiler-determines-all-of-this,
>>> the above is a well known characterization of DbC.
>> 
>> Not really. DbC is about upfront formalized requirements.
> 
> Not sure, are you speaking about DbC (TM)?

I don't care about trade marks and definitions given by reference
manuals...

>> For contracted exceptions more important is how contracts influence the
>> implementation. The idea is that in order to be legal the program must be
>> written so that the contract would be provable. If not provable, either the
>> program or the contract has to be changed. That is opposite to dynamic
>> checks, you don't need to check for non-contracted exceptions.
> 
> DbC (TM) is meant to be
> 
> (a) A model of design: client-ensures-proconditions and then
>     supplier-ensures-postconditions, so as to keep certain properties
>     of the object invariant.

This is not a model of design, this a description of some contract.

The model of design is, for example, that components can be designed
independently when contracts are stated upfront.

> (b) A debugging ("design", "specification", bla-bla) aid leading
>     towards formally proven components where such proofs are possible.

I cannot decipher this, sorry.

> "An exception is the element's inability to fulfil its contract, for any
> reason: a hardware failure has occurred, a called routine has failed, a
> software bug makes it impossible to satisfy the contract."

An exception is a program state. It is not an inability. The behavior in an
exceptional state is contracted, at least in Ada it is.

> Without those dynamic checks, we wouldn't ever notice a failure?

How would you notice a failure to notice? No need to repeat it again and
again: dynamic checks of correctness are inconsistent, see the liar paradox
et al. Dynamic check is a part of program, which determines the program's
behavior. No more, no less.

> Assuming, in this case, that there is still some amount of software
> whose behavior is not known until it executes.

The software which behavior is unknown shall never be executed.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de



  reply	other threads:[~2011-11-22 16:23 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 [this message]
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
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