comp.lang.ada
 help / color / mirror / Atom feed
From: "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>
Subject: Re: SPARK: missing case value
Date: Fri, 9 Oct 2015 23:01:33 +0200
Date: 2015-10-09T23:01:33+02:00	[thread overview]
Message-ID: <8ea6wfytssdg.1ake0jrn1irc8.dlg@40tude.net> (raw)
In-Reply-To: mv97v7$n8u$1@dont-email.me

On Fri, 9 Oct 2015 22:29:21 +0200, Georg Bauhaus wrote:

> A precondition states conditionality of proper execution.

You said that. Proper execution should be unconditional to the program
state. Otherwise it is called 'bug'. Ergo, precondition, especially a
dynamic one, is a method of introducing bugs. I called it a mine because
these bugs are well hidden, disguised as something appearing useful and
improving program design...

> (To me, it seems improper to narrow contract based design to what
> seem to be expressions of disbelief in anything mathematical truth
> before the fact. Static_Predicate says less than Predicate, and
> less is less practical, as of now, I think.)

No idea what this was supposed to mean.

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


  reply	other threads:[~2015-10-09 21:01 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
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 [this message]
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