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: Mon, 12 Dec 2016 16:31:12 +0100
Organization: A noiseless patient Spider
Message-ID: <o2mfpc$ttp$1@dont-email.me>
References: <c06ee4e6-d616-4e01-ba2e-cb111a81f6f6@googlegroups.com>
 <3ef819e8-55f7-4ef7-9f37-77e6abc33f98@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>
Reply-To: nonlegitur@notmyhomepage.de
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Mon, 12 Dec 2016 15:29:48 -0000 (UTC)
Injection-Info: mx02.eternal-september.org;
 posting-host="2bd15e9ad73c93509b7db25068f7dfe4";
	logging-data="30649"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX1972YJl00B6T3tYk+mFMQYdjh5j84gn8gI="
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.12; rv:45.0)
 Gecko/20100101 Thunderbird/45.5.1
In-Reply-To: <o2ln13$et0$1@gioia.aioe.org>
Cancel-Lock: sha1:MWq01LPJng2enFxP0xYT9mvldos=
Xref: news.eternal-september.org comp.lang.ada:32751
Date: 2016-12-12T16:31:12+01:00
List-Id: <comp.lang.ada>

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, informing about contractual
obligations in particular. For X, True means void IMHO. As in
"Warranty void if called with unsuitable parameters".

>>>> How much should a function declaration tell a programmer about
>>>> the relation between parameters A and B in the following?
>>>
>>> Remainder is not a relation. Relation is a Boolean-valued function.
>>
>> Given parameters A, B : T and
>>
>>    Pre => A > B
>>
>> the ">" is the relation, ((A, B) ∈ ">")  ≣  (A > B).
>
> 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?
My answer:
The declaration should include that they must be related by A > B.