Prev: Q: SPARK visibility rules and inherit annotations.
Next: Symbolic tracebacks on Debian (Was: About static libraries and Debian policy)
From: Yannick Duchêne (Hibou57) on 19 May 2010 23:43
The topic I am coming with may looks a bit stupid at first sight, I hope
not too much, as this may be worth to discuss.
SPARK defines some reserved words as a kind of keywords -- in the first
list -- and reserved words as FDL predefined identifiers -- in the second
The ones from the first list are reserved in any cases and have a meaning
in SPARK annotations, its extension to the core Ada kernel. The ones in
the second list, are not strictly reserved, while they will inevitably
conflict with FDL predefined identifiers, as soon as verification
conditions (VCs) are expected to be generated (which is very likely to be
as you guess).
The first identifiers set is listed in [SPARK 95 (2.9)]:
More others are given in annexe [SPARK 95 (M.2)]:
Some are probably uncommon as-is, like âsomeâ, âderivesâ, etc. Some else,
on the other hand, are quite common, and unlike Ada's keywords, more
resemble applications typical identifiers, like âfirstâ, âstartâ, âsaveâ,
âholdâ etc, and it's not that easy to find replacements for these.
I suggest to help each others in this area, discussing this matter and
attempting to create a kind of standard replacement list :p (if possible)
Sorry for not opening my self the suggestions list, as I don't have ideas
at the time (as an example, I was to replace a parameter named First by
Start... unfortunately, Start is also predefined FDL identifier).
If possible, these replacements should be as much readable and expressive
as the ones they replace (the most difficult part).
Have a good day (at least as much as you can)
From: Rod Chapman on 20 May 2010 05:01
You can, of course, use the -fdl=XXXX switch
to de-conflict the name-space if you like. In that case,
the predefined FDL identifiers are usable. See the Examiner
User Manual for details.
From: Yannick Duchêne (Hibou57) on 20 May 2010 12:37
Le Thu, 20 May 2010 11:01:30 +0200, Rod Chapman
<roderick.chapman(a)googlemail.com> a Ã©crit:
> You can, of course, use the -fdl=XXXX switch
> to de-conflict the name-space if you like. In that case,
> the predefined FDL identifiers are usable. See the Examiner
> User Manual for details.
There is something funny with this option. The documentation says it is
"-fd" and also refer to it as "-fdl".
This switch controls the Examinerâs treatment
of FDL reserved words (see section 5.3). The
option -fd=reject, or any abbreviation of
ârejectâ, rejects all FDL reserved words as being
syntactically unacceptable. This is the default.
The option -fd=accept, or any abbreviation
of âacceptâ, suppresses the rejection of FDL
reserved words, but also prevents the
generation of any proof files. Any string other
than ârejectâ or âacceptâ (or their abbreviations)
causes recognised FDL reserved words to be
mangled on output by placing the string before
the identifier, separated by a double underbar.
As an example, -fdl=praxis would cause
the identifier start to be output as
praxis__start. Previously this was a binary
option (-fdl_identifiers and -
nofdl_identifiers) and this form is still
supported, but deprecated.
Mangling is what is needed, indeed. If this work, I will use it as a
default option everywhere. Something like â-fdl=argâ or â-fdl=appâ should
be enough. Sources relying on this should add a note about in a README or
some of the like.
There was an option which deals with only one specific keywords, and I
though this was the only one.
Thanks Rod, that's the tip of the day.
There is even better than a pragma Assert: a SPARK --# check.