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=-0.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD, FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: 103376,6941f5cd4f1d4739 X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news1.google.com!postnews.google.com!q12g2000yqj.googlegroups.com!not-for-mail From: Phil Thornley Newsgroups: comp.lang.ada Subject: Re: SPARK - an idea for high integrity data structures Date: Wed, 21 Jul 2010 05:40:17 -0700 (PDT) Organization: http://groups.google.com Message-ID: References: <9ac8feb3-5b79-41b1-a124-df211039c1bc@c10g2000yqi.googlegroups.com> <4c45f3e7$0$2388$4d3efbfe@news.sover.net> NNTP-Posting-Host: 80.177.171.182 Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 X-Trace: posting.google.com 1279716017 25302 127.0.0.1 (21 Jul 2010 12:40:17 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Wed, 21 Jul 2010 12:40:17 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: q12g2000yqj.googlegroups.com; posting-host=80.177.171.182; posting-account=Fz1-yAoAAACc1SDCr-Py2qBj8xQ-qC2q User-Agent: G2/1.0 X-HTTP-UserAgent: Mozilla/4.0 (compatible; MSIE 8.0; Windows NT 6.1; WOW64; Trident/4.0; SLCC2; .NET CLR 2.0.50727; .NET CLR 3.5.30729; .NET CLR 3.0.30729; Media Center PC 6.0; .NET4.0C),gzip(gfe) Xref: g2news1.google.com comp.lang.ada:12487 Date: 2010-07-21T05:40:17-07:00 List-Id: On 20 July, 20:18, Simon Wright wrote: > "Peter C. Chapin" writes: > > > I know Praxis is working on generics support in SPARK. Once that was > > ready it probably wouldn't be too hard for the original author of a > > high integrity collections library to generalize the code as > > appropriate. At least that would be my hope. > > An alternative might be to use an external macro processor to generate > appropriate code complete with annotations. I guess that would depend on > whether the proofs (a) didn't depend on the contained type, (b) didn't > need (much) human intervention. There are occasional hints about generics, and I guess that the pressure for these is increasing. OTOH I know that some work on this had already been done five years ago, so I'm not holding my breath. There are a couple of options for a usable version of these data structures before we get generics - it would be quite easy to add an arbitrary data component, so that the proofs never depended on the actual definition of that component and they would rerun with whatever any user required as the type for that data. Another option, which avoids changing anything in the data structure code, is to make the client code responsible for storing the actual data, and just to supply a key for storage/retrieval in the data structure. The operations then have output parameters that tell the client code the index for the data in the array that the client maintains. I have both of these possibilities in mind if these exercises are successfull - but am aware that they both place a constraint on the data structure code: that no element in the data structure is ever copied from one position to another. For the first option this could be grossly inefficient, if the data is large, and it would be invalid for the second option. (This means e.g. that I can't use the easy way of deleting an internal node of a binary tree, it has to be done by changing multiple tree links.) Cheers, Phil