From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-0.3 required=5.0 tests=BAYES_00,
	REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!mx02.eternal-september.org!.POSTED!not-for-mail
From: Georg Bauhaus <bauhaus@futureapps.invalid>
Newsgroups: comp.lang.ada
Subject: Re: SPARK: missing case value
Date: Fri, 9 Oct 2015 22:29:21 +0200
Organization: A noiseless patient Spider
Message-ID: <mv97v7$n8u$1@dont-email.me>
References: <ad7b2827-9111-4d9b-b065-1ebd26795365@googlegroups.com>
 <87twq09ke2.fsf@theworld.com> <owu3jtbtdvce.14rqd6apnvnwi.dlg@40tude.net>
 <mv8pck$ph0$1@dont-email.me> <ya5c42kcq5yh.a9z7g23yf2ac.dlg@40tude.net>
Reply-To: nonlegitur@futureapps.de
Mime-Version: 1.0
Content-Type: text/plain; charset=windows-1252; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Fri, 9 Oct 2015 20:27:20 +0000 (UTC)
Injection-Info: mx02.eternal-september.org;
 posting-host="10ca66458083610b89918ee8fea6489c";
	logging-data="23838"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX1/0FUQO4sYoXG9uJ4Q7hI4DkrTx0hg669k="
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9; rv:38.0)
 Gecko/20100101 Thunderbird/38.3.0
In-Reply-To: <ya5c42kcq5yh.a9z7g23yf2ac.dlg@40tude.net>
Cancel-Lock: sha1:YFc1D2t+kphh0/ABrvJbGaK/Y/A=
Xref: news.eternal-september.org comp.lang.ada:27955
Date: 2015-10-09T22:29:21+02:00
List-Id: <comp.lang.ada>

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.)