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: Wed, 14 Dec 2016 17:55:30 +0100
Organization: Aioe.org NNTP Server
Message-ID: <o2rti5$qse$1@gioia.aioe.org>
References: <c06ee4e6-d616-4e01-ba2e-cb111a81f6f6@googlegroups.com>
 <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> <o2o73n$ci1$1@dont-email.me>
 <o2obed$qkk$1@gioia.aioe.org> <o2oj2u$i8h$1@dont-email.me>
 <o2olfi$1ca9$1@gioia.aioe.org> <o2p9bb$bcf$1@dont-email.me>
 <o2po6a$1hnq$1@gioia.aioe.org> <o2rdcq$pud$1@dont-email.me>
 <o2rfg7$f4$2@gioia.aioe.org> <o2rrf6$c1c$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:32823
Date: 2016-12-14T17:55:30+01:00
List-Id: <comp.lang.ada>

On 2016-12-14 17:21, G.B. wrote:
> On 14/12/2016 13:55, Dmitry A. Kazakov wrote:
>> On 14/12/2016 13:21, G.B. wrote:
>>> On 13/12/2016 22:11, Dmitry A. Kazakov wrote:
>>
>>> So, as far as contract based programming by programmers goes,
>>>
>>>    Pre => A > B
>>>
>>> is to mean that
>       ^^^^^^^
>>>
>>>   (forall A)(forall B)[A in T -> (B in T -> A > B)]
>>>
>>> SHALL be true so that the client gets what it deserves.
>>
>> Then it is
>>
>>    SHALL ((forall A)(forall B)[A in T -> (B in T -> A > B)] |= True)
>>
>> By no means this is an Ada expression.
>
> But reasonably close to a quantified expression that must
> be true, in case one is needed in place of just "A > B".
>
> If Pre => A > B means something to Ada programmers while
> following their contractual obligations, I don't think it is that
> all A>B entails True. Nor need the Post aspect be ignored
> as a source both for developing an implementation, and refining
> Pre.  If we do know what must be true for an implementation
> to produce a desired result, though, it will be negligent to not
> say so and instead start operations anyway.

You cannot say it in Ada, as the example shows. You must do that in 
English or in SPARK or in any other language where you can *spell* it. 
In Ada you cannot.

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