SPARK

["Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>]

Hello,

Short title, “SPARK”, as short as a subset (joking)

I wanted to start some SPARK related questions, ... “GNAT packages in  
Linux” kept apart.


Well, sorry for that, my first question gonna be about license. The GPL  
applies to SPARK-GPL (oh? really?). How does it apply ? I'm dubious about  
it in this context, because using SPARK to check an implementation does  
not implies any kind of linking to any binary or library, and I did not  
see anywhere something stating there was license restrictions on the usage  
of SPARK annotations in Ada sources.

What are the concrete restrictions so ?



Hope this first question will get a short answer, so let us jump to the  
second question, which is intended to start with one major deal of SPARK  
for people who know/use Ada : Ada subset and restrictions (not to disclaim  
or disagree with, mostly to talk and understand more).

The Praxis reference for SPARK-95 says :

[Praxis SPARK95 3]
> SPADE-Pascal was developed essentially by excising from
> ISO-Pascal those features which were considered particularly
> “dangerous”, or which could give rise to intractable validation
> problems - such as variant records,
That said, variant record can be emulated by user or program too, as  
that's just what were doing many people when there was no language support  
for that. What is different when the Pascal or Ada variant record compared  
to a user or program doing explicitly the same ? May be the answer is just  
in one of the last three words : “explicitly” ?

Does this quotation from the Praxis's reference about SPARK suggests SPARK  
has some troubles with the implicit or the underlying ?

If SPARK could know about a formalization of what's going on with variant  
records, as explicit as would be the same made by the user or program,  
would that solve the trick ?

What would possibly make this difficult or non-trustable ?