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

["Randy Brukardt" <randy@rrsoftware.com>]

"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).

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? It's just an optional help in a few circumstances.

                                                Randy.