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!news.eternal-september.org!.POSTED!not-for-mail
From: "G.B." <bauhaus@notmyhomepage.invalid>
Newsgroups: comp.lang.ada
Subject: Re: Ada 2012 Constraints (WRT an Ada IR)
Date: Tue, 13 Dec 2016 08:15:22 +0100
Organization: A noiseless patient Spider
Message-ID: <o2o73n$ci1$1@dont-email.me>
References: <c06ee4e6-d616-4e01-ba2e-cb111a81f6f6@googlegroups.com>
 <o1s71b$oi7$1@gioia.aioe.org> <o1sj6s$9vp$1@dont-email.me>
 <o1u6en$1igc$2@gioia.aioe.org> <o1uj70$qe2$1@dont-email.me>
 <o1uroj$jsj$1@gioia.aioe.org>
 <47366b42-c0a3-41bf-a44a-5241c109d60f@googlegroups.com>
 <alpine.DEB.2.20.1612050922450.22845@debian> <o23a8a$11e9$1@gioia.aioe.org>
 <o24om5$vfr$1@franka.jacob-sparre.dk> <o24phv$1ou6$1@gioia.aioe.org>
 <o27gpr$o8k$1@franka.jacob-sparre.dk> <o28non$1fn8$1@gioia.aioe.org>
 <o2a2ad$vnp$1@franka.jacob-sparre.dk> <o2b79r$1dit$1@gioia.aioe.org>
 <o2b9rg$ejl$1@dont-email.me> <o2bb4o$1jpb$1@gioia.aioe.org>
 <o2c93i$rpp$2@dont-email.me> <o2du2t$1ghu$1@gioia.aioe.org>
 <o2jcpd$75p$1@dont-email.me> <o2jgom$18jg$1@gioia.aioe.org>
 <o2jkdm$bt$1@dont-email.me> <o2js2d$1qh4$1@gioia.aioe.org>
 <o2ke6d$gcs$1@dont-email.me> <o2ln13$et0$1@gioia.aioe.org>
 <o2mfpc$ttp$1@dont-email.me> <o2mncc$gjn$1@gioia.aioe.org>
 <o2mroh$dsk$1@dont-email.me> <o2n2o1$1515$1@gioia.aioe.org>
Reply-To: nonlegitur@notmyhomepage.de
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Tue, 13 Dec 2016 07:13:59 -0000 (UTC)
Injection-Info: mx02.eternal-september.org;
 posting-host="eb28462d3cdfe36eb00d85b69972742c";
	logging-data="12865"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX18IMVcxsvFFWFSAyff4OVn6hH3y/SDay04="
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.12; rv:45.0)
 Gecko/20100101 Thunderbird/45.5.1
In-Reply-To: <o2n2o1$1515$1@gioia.aioe.org>
Cancel-Lock: sha1:vaeb80HRa9a9bc+88jBHq+4VbGk=
Xref: news.eternal-september.org comp.lang.ada:32773
Date: 2016-12-13T08:15:22+01:00
List-Id: <comp.lang.ada>

On 12/12/2016 21:53, Dmitry A. Kazakov wrote:
> On 2016-12-12 19:55, G.B. wrote:
>> On 12/12/2016 18:39, Dmitry A. Kazakov wrote:
>>> As I said before it must be moved to the post-condition,
>>> Storage_Error, or whatever raised upon stack overflow included.
>>
>> Could you please show a good Post aspect for
>>
>> function Plus_Too (A, B: Standard.Integer)
>>                   return Standard.Integer is
>> begin
>>    return A + B;
>> end Plus_Too;
>
> None. Don't use aspects they are not good. I have already listed post-conditions, see my post from 2016-12-09.

No Ada in there. I was thinking of this posting.

So, is there nothing we can say about the arguments
when we declare Plus_Too, such as how they need to be
related for Plus_Too at all having a chance of not raising?

> Implied contracts are outside the scope.

My point. Why should contracts not be explicit, in particular
when they had already been formal, albeit in a comment?

> There is an infinite number of implied contracts which can be violated,
>  e.g. the one that the Earth does not turn black hole...

That's curious. Can you show us the contract written and explicitly
stating that the Earth does not turn black hole, and then explain
how a programmer writing a call can violate this contract?

(Actually, there is no variable in the predicate other than those
implied in sub-expressions of Earth turning a black hole.
IIRC, the Large Hadron Collider was thought capable of violating
this contract according to explicit statements of some scientist.)