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!news.eternal-september.org!feeder.eternal-september.org!gegeweb.org!aioe.org!.POSTED!not-for-mail
From: "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>
Newsgroups: comp.lang.ada
Subject: Re: The future of Spark . Spark 2014 : a wreckage
Date: Thu, 18 Jul 2013 09:19:52 +0200
Organization: cbb software GmbH
Message-ID: <15q73x8g743d.solfjve1fywf$.dlg@40tude.net>
References: <1d4tuwlfdnz2j$.18l68s96x3vjj.dlg@40tude.net>
 <984821833395507830.672948rm-host.bauhaus-maps.arcor.de@news.arcor.de>
 <ks23dp$npd$1@loke.gir.dk>
 <e7de5753-5819-41a4-a40f-3d80c101bf03@googlegroups.com>
 <ks7851$3mm$1@loke.gir.dk>
Reply-To: mailbox@dmitry-kazakov.de
NNTP-Posting-Host: IenaDxMXK2hi7fvYcb+MlQ.user.speranza.aioe.org
Mime-Version: 1.0
Content-Type: text/plain; charset="us-ascii"
Content-Transfer-Encoding: 7bit
X-Complaints-To: abuse@aioe.org
User-Agent: 40tude_Dialog/2.0.15.1
X-Notice: Filtered by postfilter v. 0.8.2
Xref: news.eternal-september.org comp.lang.ada:16411
Date: 2013-07-18T09:19:52+02:00
List-Id: <comp.lang.ada>

On Wed, 17 Jul 2013 18:08:17 -0500, Randy Brukardt wrote:

> "Shark8" <onewingedshark@gmail.com> wrote in message 
> news:e7de5753-5819-41a4-a40f-3d80c101bf03@googlegroups.com...
> ...
>>The one drawback from your proposal is that it makes you reiterate the 
>>condition, but with a negation, this could be a source of bugs. Even though it's a 
>>little less straightforward the following would circumvent that problem:
> 
>> procedure Op (x : in out T)
>>   with Post => (Constraint_Error at [not?] Foo(x));
> 
> I didn't mean this to be a real example. An example like the one given 
> probably would have been better written as a precondition (depending on 
> exactly what Foo does):
> 
>   procedure Op (x : in out T)
>      with Pre => Foo(x) or else raise Constraint_Error,
>             Post => Foo(x);
> 
> which is just normal Ada 2012 code (using the raise expression, which we 
> added 'after the fact' to support this usage).

Yep, and also highlights the inconvenient truth, that the "precondition" is
not a precondition but rather a chunk of executable code pushed in front of
the body.

Why not to honestly call it Prologue?

> I don't think most exception contracts would have an associated 
> postcondition (that is, cause); what would the postcondition be for 
> Use_Error, for instance?

If proper post-condition meant then:

   ensure Foo (X) or Raised (Constraint_Error); -- Weak contract

The issue you mentioned is strong exception contract telling when the
exception has to propagate and when not. That would be:

   ensure Foo (X) xor Raised (Constraint_Error); -- Explicit contract

If not Foo (X) then exception.

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