From: Yannick Duchêne (Hibou57) on
Hello,

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
list.

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)]:

assert
check
derives
from
global
hide
hold
inherit
initializes
invariant
main_program
own
post
pre
some

More others are given in annexe [SPARK 95 (M.2)]:

are_interchangeable
as
assume
const
finish
first
for_all
for_some
goal
may_be_deduced
may_be_deduced_from
may_be_replaced_by
nonfirst
nonlast
not_in
odd
requires
save
sequence
set
sqr
start
strict_subset_of
subset_of
succ


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
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.
- Rod

From: Yannick Duchêne (Hibou57) on
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".

-fd=string:

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.