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:23:45 +0100
Organization: A noiseless patient Spider
Message-ID: <o2mfbd$s5r$1@dont-email.me>
References: <c06ee4e6-d616-4e01-ba2e-cb111a81f6f6@googlegroups.com>
 <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> <87eg1e2f2c.fsf@nightsong.com>
 <o2lndc$fmo$1@gioia.aioe.org>
Reply-To: nonlegitur@notmyhomepage.de
Mime-Version: 1.0
Content-Type: text/plain; charset=windows-1252; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Mon, 12 Dec 2016 15:22:21 -0000 (UTC)
Injection-Info: mx02.eternal-september.org;
 posting-host="2bd15e9ad73c93509b7db25068f7dfe4";
	logging-data="28859"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX184X9XOZHCqiKkox+cL9mtShIq5Cn0CK6E="
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.12; rv:45.0)
 Gecko/20100101 Thunderbird/45.5.1
In-Reply-To: <o2lndc$fmo$1@gioia.aioe.org>
Cancel-Lock: sha1:ohQf8f1BPrIgPDM9m7QXSluzQcI=
Xref: news.eternal-september.org comp.lang.ada:32749
Date: 2016-12-12T16:23:45+01:00
List-Id: <comp.lang.ada>

On 12/12/2016 09:33, Dmitry A. Kazakov wrote:
> On 12/12/2016 00:58, Paul Rubin wrote:

>> Ada certainly allows Pre=> to be checked at runtime.
>
> Because they are not preconditions,

Right, the aspect is called Pre, not Precondition. Good Thing.
The language makers aren't usually shy about using full
names, so... The Rationale outlines their intent.

> part of the subprogram body.

Does the LRM state that Pre checks must be part
of the subprogram body? I don't think so.

> Surely you could not turn it off, but you could optimize it away.

How so, if the programmer has configured Checks?