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

[Shark8 <onewingedshark@gmail.com>]

On Monday, July 15, 2013 6:16:56 PM UTC-6, Randy Brukardt wrote:
> "Georg Bauhaus" <rm-host.bauhaus@maps.arcor.de> wrote in message 
> news:984821833395507830.672948rm-host.bauhaus-maps.arcor.de@news.arcor.de...
> > "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote:
> >
> >> I don't see how adding optional exception contracts should disrupt
> >> anything.
> >
> > Aren't exceptions already part of contracts? Implied, though.
> 
> Yes, but only for inbound contracts (preconditions and predicates). We need 
> them for outbound contracts as well, without having to guess. And I agree 
> with Dmitry that those need to be compile-time checked in the subprogram 
> bodies. (Exactly how that's done has to be worked out, of course).
> 
> procedure Op (x : in out T)
>   with Post => Foo(x),
>          Exception => Constraint_Error when not Foo(x);
> or something like that.
> 
>                             Randy.

I think you and I talked about that idea (basically sets of exceptions) and I like the idea a lot (though not the particular syntax you were using, which is ok) -- I really like the idea you have for renaming the violation exception, in retrospect that would have been very desirable for constraint-aspect violations (pre-/post-conditions, particularly).

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));

which would reuse the keyword(s) AT [and NOT] in addition to preventing the unnecessary duplication. {The use of parenthesis could also be mandated that way the clauses [which are different constitutions] could be made/forced-distinct when they are to raise differing exceptions on violation.}