Processing array subsections, a newbie question.
in [ADA]
|
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: -fdl=my 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 is type Var is range 0 .. 10_000; procedure Pred (First : in Var; Last : in out Var) --# derives Last from *, First; is Start : Var; Finish : Var; Succ : Var; begin 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; end loop; end if; Last := Succ; end Pred; end Sequence; Cheers, Phil
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. Peter
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! Peter
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> a écrit: >> 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! > > Peter 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. > loop 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.) -- Jeff Carter "Why don't you bore a hole in yourself and let the sap run out?" Horse Feathers 49 |