From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM
	autolearn=ham autolearn_force=no version=3.4.4
X-Google-Thread: a07f3367d7,fd504db0db66529c,start
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,UTF8
Path: 
 g2news2.google.com!news4.google.com!feeder.news-service.com!tudelft.nl!txtfeed1.tudelft.nl!zen.net.uk!dedekind.zen.co.uk!aioe.org!not-for-mail
From: =?utf-8?Q?Yannick_Duch=C3=AAne_=28Hibou57?=
 =?utf-8?Q?=29?=
 <yannick_duchene@yahoo.fr>
Newsgroups: comp.lang.ada
Subject: SPARK reserved and predefined words : alternative choices
Date: Thu, 20 May 2010 05:43:51 +0200
Organization: Ada At Home
Message-ID: <op.vczjbdgtule2fv@garhos>
NNTP-Posting-Host: Wj8XAjoNVRxqky9biWs8Mw.user.speranza.aioe.org
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed; delsp=yes
Content-Transfer-Encoding: Quoted-Printable
X-Complaints-To: abuse@aioe.org
X-Notice: Filtered by postfilter v. 0.8.2
User-Agent: Opera Mail/10.53 (Win32)
Xref: g2news2.google.com comp.lang.ada:11785
Date: 2010-05-20T05:43:51+02:00
List-Id: <comp.lang.ada>

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 secon=
d  =

list.

The ones from the first list are reserved in any cases and have a meanin=
g  =

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 b=
e  =

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 =E2=80=9Csome=E2=80=9D, =E2=80=9C=
derives=E2=80=9D, etc. Some else,  =

on the other hand, are quite common, and unlike Ada's keywords, more  =

resemble applications typical identifiers, like =E2=80=9Cfirst=E2=80=9D,=
 =E2=80=9Cstart=E2=80=9D, =E2=80=9Csave=E2=80=9D,  =

=E2=80=9Chold=E2=80=9D 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 idea=
s  =

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 expressiv=
e  =

as the ones they replace (the most difficult part).



Have a good day (at least as much as you can)