From: Phil Thornley on 15 Jun 2010 05:45
On 15 June, 00:54, "Peter C. Chapin" <pcc482...(a)gmail.com> wrote:
> 'First' and 'Last' are reserved by SPARK as FDL identifiers. Similarly 'Start'
> and 'Finish' are reserved by SPARK.
There is a well-hidden feature of the Examiner to get over this
problem - use the qualifier -fdl=your_string.
(Where your_string is not either "accept" or "reject" or any
abbreviation of these.)
It's described in Section 3.1.5 of the Examiner User Manual (the
section on command qualifiers) but is not mentioned in the section on
reserved words (5.3, where you would really expect to find it).
I only discovered this a couple of weeks ago, but the line:
is now a permanent addition to my switch files.
Here is a program that examines and proves OK with that qualifier:
(For the non-SPARK readers, every identifier in this code is one of
the reserved words that would otherwise cause an error.)
(For the pedants: use of any identifier in this code is not a
recommendation to use that identifier in any other code.)
package body Sequence
type Var is range 0 .. 10_000;
procedure Pred (First : in Var;
Last : in out Var)
--# derives Last from *, First;
Start : Var;
Finish : Var;
Succ : Var;
Succ := Var'First;
Start := First;
Finish := Last;
if Start < Last then
for Element in Var range Start + 1 .. Finish loop
Succ := Succ + 1;
--# assert Succ <= Element - Start
--# and Start >= 0;
Last := Succ;
From: Peter C. Chapin on 15 Jun 2010 07:24
Simon Wright wrote:
> Oops, I didn't know that.
> A shame that to make code provable you have to make it unreadable.
The naming issue isn't that big a problem in practice. I've only hit it this
once so far. With a little effort I could probably come up with something
better that doesn't clash.
From: Peter C. Chapin on 15 Jun 2010 07:27
Phil Thornley wrote:
> There is a well-hidden feature of the Examiner to get over this
> problem - use the qualifier -fdl=your_string.
> (Where your_string is not either "accept" or "reject" or any
> abbreviation of these.)
> It's described in Section 3.1.5 of the Examiner User Manual (the
> section on command qualifiers) but is not mentioned in the section on
> reserved words (5.3, where you would really expect to find it).
That's cool. Good to know!
From: Yannick Duchêne (Hibou57) on 15 Jun 2010 08:11
Le Tue, 15 Jun 2010 13:27:06 +0200, Peter C. Chapin <pcc482719(a)gmail.com>
>> It's described in Section 3.1.5 of the Examiner User Manual (the
>> section on command qualifiers) but is not mentioned in the section on
>> reserved words (5.3, where you would really expect to find it).
> That's cool. Good to know!
If you use it, just be careful that names in VC and simplified VC files
will be changed (just wanted to noticed so you will not feel lost).
There is even better than a pragma Assert: a SPARK --# check.
--# check C and WhoKnowWhat and YouKnowWho;
--# assert Ada;
-- i.e. forget about previous premises which leads to conclusion
-- and start with new conclusion as premise.
From: Jeffrey R. Carter on 13 Jun 2010 02:54
Niklas Holsti wrote:
> if Index_Fst <= Buffer'Last then
> -- Buffer is not empty, something to be done.
OK, we get here with Index_Fst < Buffer'Last.
> Do_Something(Buffer, Index_Fst, Index_Lst, Ok);
And Do_Something set Ok to True.
> exit when not Ok;
Do_Something doesn't change Index_Fst, so we get past
> exit when Index_Fst >= Buffer'Last;
to here. Now the OP's concern, IIUC, is that Index_Lst, which Do_Something sets,
might be = Buffer'Last = Natural'Last (seems unlikely, but I suspect this is
simplified from an example in which the index range is more constrained and
Index_Lst is more likely to be = Index_Subtype'Last). In that case
> Index_Fst := Index_Lst + 1;
will raise an exception.
So it looks to me as if the correct test is
exit when Index_Lst [>]= Buffer'Last;
(Maybe Brenta meant this, and mistyped it; the variable names are very similar.
Using _First and _Last might make such an error more obvious.)
"Why don't you bore a hole in yourself and let the sap run out?"