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=-1.9 required=5.0 tests=BAYES_00
	autolearn=unavailable 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!feeder.eternal-september.org!aioe.org!.POSTED!not-for-mail
From: "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>
Newsgroups: comp.lang.ada
Subject: Re: Ada 2012 Constraints (WRT an Ada IR)
Date: Mon, 12 Dec 2016 21:53:23 +0100
Organization: Aioe.org NNTP Server
Message-ID: <o2n2o1$1515$1@gioia.aioe.org>
References: <c06ee4e6-d616-4e01-ba2e-cb111a81f6f6@googlegroups.com>
 <o1q81b$9kc$1@franka.jacob-sparre.dk> <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>
NNTP-Posting-Host: s3c6wwRqkurrfTZpuYYZ+w.user.gioia.aioe.org
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 7bit
X-Complaints-To: abuse@aioe.org
User-Agent: Mozilla/5.0 (Windows NT 10.0; WOW64; rv:45.0) Gecko/20100101
 Thunderbird/45.5.1
X-Notice: Filtered by postfilter v. 0.8.2
Xref: news.eternal-september.org comp.lang.ada:32766
Date: 2016-12-12T21:53:23+01:00
List-Id: <comp.lang.ada>

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.

>>> My answer:
>>> The declaration should include that they must be related by A > B.
>>
>> They are not.
>
> Only when the client has violated the contract about
> which the programmer has never been told...

Implied contracts are outside the scope. They question was about the 
explicit ones. There is an infinite number of implied contracts which 
can be violated, e.g. the one that the Earth does not turn black hole...

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