SPARK reserved and predefined words : alternative choices
in [ADA]
|
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 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 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. - Rod
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". -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. |