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
next prev parent 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