Re: The future of Spark . Spark 2014 : a wreckage

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

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