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: Fri, 16 Dec 2016 12:48:20 +0100
Organization: A noiseless patient Spider
Message-ID: <o30k7g$cif$1@dont-email.me>
References: <c06ee4e6-d616-4e01-ba2e-cb111a81f6f6@googlegroups.com>
 <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>
 <999c67b0-4478-4d2b-8108-32ac48fe6316@googlegroups.com>
 <o2r0lo$175u$1@gioia.aioe.org>
 <a960c6dd-80aa-4c9f-bf3b-47da529e0e01@googlegroups.com>
 <o2s8l1$1fef$1@gioia.aioe.org>
 <f1cebe17-25b1-4f75-9c1d-ff89d869aa87@googlegroups.com>
 <o2tl0b$1af0$1@gioia.aioe.org> <o2trb6$aso$1@dont-email.me>
 <o2u54i$73i$1@gioia.aioe.org> <o2us43$gik$1@dont-email.me>
 <o30e6s$1oqo$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: Fri, 16 Dec 2016 11:46:56 -0000 (UTC)
Injection-Info: mx02.eternal-september.org;
 posting-host="0c616e07f0384066ee27fa5f855b39fa";
	logging-data="12879"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX18n2+s+ptFoly52zBf22xmxyAN1/xr/Ayc="
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.12; rv:45.0)
 Gecko/20100101 Thunderbird/45.5.1
In-Reply-To: <o30e6s$1oqo$1@gioia.aioe.org>
Cancel-Lock: sha1:QCgnUzeZn77vzzTEE3rkCuBuVD4=
Xref: news.eternal-september.org comp.lang.ada:32877
Date: 2016-12-16T12:48:20+01:00
List-Id: <comp.lang.ada>

On 16/12/2016 11:04, Dmitry A. Kazakov wrote:

>>    function Make (First, Second: POT) return Immutable_Ordered_Pair
>>    with
>>      --Pre => First <= Second,   -- (*)
>>      Post => Make'Result in Immutable_Ordered_Pair; -- or raise
>
> Right, no precondition

As you have chosen to not address, except for here saying
"no precondition" while stating a Pre later, the lack of Pre
will cause major differences. They comprise both Make
and the whole design and efficiency, all as outlined.
How could anyone always ignore these differences?

>> Now give the programmer Pre as it follows from {Post, Type_Invariant},
>> and you are designing by contract:
>
> No. Pre does not follow from Post. The one that does is different:
>
>    First >= Second or else Constraint_Error is propagating

I assume you meant

     First <= Second or else Constraint_Error is propagating?

Which is basically the observable behavior of current Ada,
except that

- with Pre,
     a call may have been started, but is stopped from entering
     the Ada-body,

- without Pre,
     the Ada-body has started checking and runs into all sorts
     of decisions, and possibly into the Type_Invariant not
     being True for the parameters it has already "accepted".

> The key difference is

... a design choice: establishing the precondition is work
to be done be the programmer who writes the call. There may be
Make'Pre as a guide. If there isn't, the implementers of
Make and writers of Make'Post have not done their homework.

But this is puzzling:
Suppose the compiler can't prove that calling Make is safe in the
Pre/Post sense. Then, how did the programmer of Make determine
which parameters will lead to safe return? And be silent about it?

Again, I think that an important purpose of the Pre aspect is to
inform the programmer about when *not* to call.