[Spark2014-discuss] [M122-037] [Spark2014] aspect to identify code that is in/out of SPARK 2014
jon.burton at altran.com
Mon Jan 28 10:18:26 CET 2013
>>On 01/26/2013 03:44 PM, Cyrille Comar wrote:
>> Definitely needs more discussion since I don't see a viable alternative.
>> Could you point me to a trace of the discussion explaining what 'people'
>> found 'not appropriate'?
>We only discussed it live during the weekly SPARK language design
>meeting, and maybe I did not explain the proposal well enough to
>convince others. We've now had this discussion by email, and the main
>argument against the SPARK aspect seems to be that it is not flexible
>enough to allow hiding exception handlers. If we agree that this form of
>hiding is not desirable, is there any other reason not to adopt a SPARK
>aspect to denote which declarations are in SPARK?
There was no argument - at least from Bath - that we need a language feature to denote
what is intended to be in (or out of) SPARK 2014. The argument was that we shouldn't
pick the first version of that feature that we think of, and
we shouldn't just define a language feature without having defined first the needs
it is intended to meet. In particular, the nature of this language feature depends on
how exactly we intend to handle the mixing of SPARK and non-SPARK 2014 code and what
the use cases are in relation to that.
For example, it might make more sense to have a language feature that states code is
*not* SPARK 2014, rather than the other way round (this is what is currently done with
SPARK). After all, the obvious point to annotate is the boundary between the SPARK code and
the non-SPARK code that it calls, and if annotating at this point it makes sense to identify the
code that isn't in SPARK.
As an aside, the hiding of exception handlers is something that is currently used in
SPARK: iFACTS, for example, uses this a lot.
More information about the Spark2014-discuss