From: Georg Bauhaus <bauhaus@futureapps.invalid>
Subject: Re: SPARK: missing case value
Date: Fri, 9 Oct 2015 22:29:21 +0200
Date: 2015-10-09T22:29:21+02:00 [thread overview]
Message-ID: <mv97v7$n8u$1@dont-email.me> (raw)
In-Reply-To: <ya5c42kcq5yh.a9z7g23yf2ac.dlg@40tude.net>
On 09.10.15 18:35, Dmitry A. Kazakov wrote:
> On Fri, 9 Oct 2015 18:20:32 +0200, G.B. wrote:
>
>> On 09.10.15 17:10, Dmitry A. Kazakov wrote:
>>> Because the above is a proper contract, while precondition is a land mine.
>>
>> A land mine has a very proper contract.
>
> Certainly so. But there is a huge semantic and language difference between
> IS and HAS.
Right, a land mine cannot be stated as a precondition.
A precondition states conditionality of proper execution.
(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.)
next prev parent reply other threads:[~2015-10-09 20:29 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 [this message]
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