From: "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>
Subject: Re: SPARK: missing case value
Date: Fri, 9 Oct 2015 17:34:34 +0200
Date: 2015-10-09T17:34:34+02:00 [thread overview]
Message-ID: <o0waam7igg9i$.1snrocvgm593q$.dlg@40tude.net> (raw)
In-Reply-To: 87lhbc9idb.fsf@theworld.com
On Fri, 09 Oct 2015 11:22:40 -0400, Bob Duff wrote:
> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
>
>> Because the above is a proper contract, while precondition is a land
>> mine.
>
> Why do you think preconditions are dangerous?
Even when statically checked they may cause issues as presented. And it
trivially follows from the basic SW design principle of weakening
preconditions. The weakest possible precondition is True, i.e. none.
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
next prev parent reply other threads:[~2015-10-09 15:34 UTC|newest]
Thread overview: 17+ messages / expand[flat|nested] mbox.gz Atom feed top
2015-10-09 11:38 SPARK: missing case value Maciej Sobczak
2015-10-09 12:28 ` Stefan.Lucks
2015-10-09 12:35 ` Mark Lorenzen
2015-10-09 14:53 ` Bob Duff
2015-10-09 14:39 ` Bob Duff
2015-10-09 15:10 ` Dmitry A. Kazakov
2015-10-09 15:22 ` Bob Duff
2015-10-09 15:34 ` Dmitry A. Kazakov [this message]
2015-10-09 16:20 ` G.B.
2015-10-09 16:35 ` Dmitry A. Kazakov
2015-10-09 20:29 ` Georg Bauhaus
2015-10-09 21:01 ` Dmitry A. Kazakov
2015-10-10 6:44 ` Randy Brukardt
2015-10-10 9:10 ` Georg Bauhaus
2015-10-10 10:00 ` Dmitry A. Kazakov
2015-10-10 14:19 ` Georg Bauhaus
2015-10-11 9:49 ` Dmitry A. Kazakov
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox