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 21:35:17 +0100
Organization: A noiseless patient Spider
Message-ID: <o31j3h$so5$1@dont-email.me>
References: <c06ee4e6-d616-4e01-ba2e-cb111a81f6f6@googlegroups.com>
 <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> <o30k7g$cif$1@dont-email.me>
 <alpine.DEB.2.20.1612161308590.29766@debian>
Reply-To: nonlegitur@notmyhomepage.de
Mime-Version: 1.0
Content-Type: text/plain; charset=iso-8859-15; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Fri, 16 Dec 2016 20:33:53 -0000 (UTC)
Injection-Info: mx02.eternal-september.org;
 posting-host="0c616e07f0384066ee27fa5f855b39fa";
	logging-data="29445"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX18duA3NTdeHuSBLNqgBOeab9FN0xFxc2jc="
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.12; rv:45.0)
 Gecko/20100101 Thunderbird/45.5.1
In-Reply-To: <alpine.DEB.2.20.1612161308590.29766@debian>
Cancel-Lock: sha1:t9RJ2d2ZXGl7FW7l9SiyTkVI41U=
Xref: news.eternal-september.org comp.lang.ada:32892
Date: 2016-12-16T21:35:17+01:00
List-Id: <comp.lang.ada>

On 16/12/2016 13:56, Stefan.Lucks@uni-weimar.de wrote:
> In contrast, the notation with "or else Exception" is technically not a precondition, any more. It tells the reader/client: "You don't need to bother with the order of First and Second. If you call Make with First > Second, I will raise a specific exception that you may handle, then.":
>
>    function Make (First, Second: POT) return Immutable_Ordered_Pair
>    with
>      Pre => First <= Second or else Raise_Constaint_Error,
>      Post => ...

Following the Eiffel lead, and also Randy Brukardt's reminder
to consider RM 6.4(10/2), I think it is correct to say that
no statement of the Ada block

   begin   -- of Make
     ....
   end Make;

will execute "raise Constraint_Error" announced in Pre. In fact,
RM 6.1.1(36/3) shows that Make cannot possibly raise the exception
from inside, because then, technically, it could handle it there,
contradicting the RM.

So if "Post" means "After", then a contract violation may come
first and an Assertion_Error is raised after that, but the
execution of statements of Make will not have begun. So, in
contract based design, Make does what it is supposed to do and
does *not* check its Pre, just like proofs do not check their
premises. (Eiffel just attaches names to "require"'s Boolean
expressions, for reference.)


That's a difference, I think, between contract based programming
and plain old defensive programming with exceptions, or "programming
by announced jumping", if I may call it that.