From: "Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>
Subject: SPARK reserved and predefined words : alternative choices
Date: Thu, 20 May 2010 05:43:51 +0200
Date: 2010-05-20T05:43:51+02:00 [thread overview]
Message-ID: <op.vczjbdgtule2fv@garhos> (raw)
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)
next reply other threads:[~2010-05-20 3:43 UTC|newest]
Thread overview: 3+ messages / expand[flat|nested] mbox.gz Atom feed top
2010-05-20 3:43 Yannick Duchêne (Hibou57) [this message]
2010-05-20 9:01 ` SPARK reserved and predefined words : alternative choices Rod Chapman
2010-05-20 16:37 ` Yannick Duchêne (Hibou57)
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox