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 18:39:22 +0100
Organization: Aioe.org NNTP Server
Message-ID: <o2mncc$gjn$1@gioia.aioe.org>
References: <c06ee4e6-d616-4e01-ba2e-cb111a81f6f6@googlegroups.com>
 <o1oohd$13nu$1@gioia.aioe.org> <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>
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:32759
Date: 2016-12-12T18:39:22+01:00
List-Id: <comp.lang.ada>

On 2016-12-12 16:31, G.B. wrote:
> On 12/12/2016 09:27, Dmitry A. Kazakov wrote:
>
>>> I.e., the programmer writing Y (X (A, B)) has ensured that
>>> the assumption expressed as X'Pre is actually true before
>>> calling X.
>>
>> So what? Programmers program programs, and how is that related to
>> contracts etc?
>
> Informing is contracts' primary purpose,

Nope. The contract's purpose is to constrain contracted parties. 
Informing is the purpose of E-mail, newspaper etc...

>> Right, ">" is a relation, Remainder is not. And the point was?
>
> The point was:
> How much should the declaration of function Remainder tell a programmer
> about the relation between parameters A and B?

It should not unless statically enforceable. And there are lots of other 
mathematical facts about remainders and relations defined on the 
argument and the result you are conveniently ignoring. Including 
relations between stack pointer and stack size. Reason?

Now, from the software design POW, preconditions (the true ones, not the 
things you call so) must be as weak as possible. Thus even if A>B would 
be statically provable it is against good design practice to impose it 
because it burdens clients and means distributed overhead.

As I said before it must be moved to the post-condition, Storage_Error, 
or whatever raised upon stack overflow included.

> My answer:
> The declaration should include that they must be related by A > B.

They are not. Remainder is defined for A <= B as Constraint_Error, 
unless you get Storage_Error before that...

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