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: Wed, 14 Dec 2016 12:04:46 +0100
Organization: A noiseless patient Spider
Message-ID: <o2r8tr$bc9$1@dont-email.me>
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>
 <999c67b0-4478-4d2b-8108-32ac48fe6316@googlegroups.com>
 <o2r0lo$175u$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: Wed, 14 Dec 2016 11:03:23 -0000 (UTC)
Injection-Info: mx02.eternal-september.org;
 posting-host="d7777aaea4e05f5460ede15b9236d665";
	logging-data="11657"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX1/GsG59SNaBkYJB8bwFDG1ldGszpm/JVQo="
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.12; rv:45.0)
 Gecko/20100101 Thunderbird/45.5.1
In-Reply-To: <o2r0lo$175u$1@gioia.aioe.org>
Cancel-Lock: sha1:IX64s0W9LjoMcQnohT56duvpvd4=
Xref: news.eternal-september.org comp.lang.ada:32810
Date: 2016-12-14T12:04:46+01:00
List-Id: <comp.lang.ada>

On 14/12/2016 09:42, Dmitry A. Kazakov wrote:
>
> The precondition here is *not* (Y in Positive), it is (Y in Integer). It is legal to call X on any Integer. Checking Y>=0 is semantically a part of the X's body, even if the compiler could inline this part at the caller's side or optimize it or the rest of the body away.

And this is where Design by Contract, by intent, would differ
from current choice of Ada's defensive style:

   The programmer is NOT allowed to just call an operation
   when there is a Pre aspect that says: Don't!

So, by intent, if you declare

   procedure X (Y : Positive)
      with
         Pre => Y > 0;

then a client programmer is required, by contract, to not
call X with a non-positive Integer.  If he or she does,
then the programmer is violating the contract, and held
responsible for any damage caused by the body of X.

This is what contract based programming is all about.