SPARK reserved and predefined words : alternative choices

SPARK reserved and predefined words : alternative choices

[Yannick Duchêne (Hibou57)]

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)

Re: SPARK reserved and predefined words : alternative choices

[Rod Chapman]

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

Re: SPARK reserved and predefined words : alternative choices

[Yannick Duchêne (Hibou57)]

Le Thu, 20 May 2010 11:01:30 +0200, Rod Chapman  
<roderick.chapman@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.