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,6d79efdb8dde2c5a X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII Path: g2news1.google.com!postnews.google.com!z10g2000yqb.googlegroups.com!not-for-mail From: Phil Thornley Newsgroups: comp.lang.ada Subject: Re: SPARK : third example for Roesetta - reviewers welcome Date: Tue, 17 Aug 2010 12:53:18 -0700 (PDT) Organization: http://groups.google.com Message-ID: <1ddee5a6-fc25-4d23-bebd-3364923d0aa5@z10g2000yqb.googlegroups.com> References: <589eea9a-0b14-4ae5-bf62-9abf4b33e7fb@i31g2000yqm.googlegroups.com> <82mxsnuhbq.fsf@stephe-leake.org> <4c69a251$0$2371$4d3efbfe@news.sover.net> <4c69cd5f$0$2375$4d3efbfe@news.sover.net> NNTP-Posting-Host: 80.177.171.182 Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Trace: posting.google.com 1282074798 17922 127.0.0.1 (17 Aug 2010 19:53:18 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Tue, 17 Aug 2010 19:53:18 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: z10g2000yqb.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:13467 Date: 2010-08-17T12:53:18-07:00 List-Id: On 17 Aug, 10:15, Phil Thornley wrote: > I'm going to try and come up with an explanation of SPARK for Rosetta > Code that covers all the ground, but is as succinct as possible (so no- > one should be holding their breath for that). =A0I'll link out to > detailed descriptions where possible. OK - I discovered that Rosetta Code has Encyclopedia pages, that can be used for any topic that doesn't fit in anywhere else. So I've written a very short bit for the 'Category:SPARK' page which is what is linked to by the language name. This page will contain links to the Altran-Praxis home page and to their page about SPARK. Then I've written a longer 'SPARK tools' page to go in the Encyclopedia, to be linked from the category text, that describes the Examiner and the Simplifier. Then a 'SPARK Proof' page, also for the Encyclopedia and to be linked from the SPARK tools page, that describes how verification conditions are processed and discharged. (So readers won't see all the horrible confusing options about proof until they've followed three separate links and so are likely to be a bit more interested than the casual browser). The proof page briefly lists the different ways that an unproven but provable VC can be dealt with (which is where all the problems have cropped up), so if the code examples reference back to this when they need to it should help to reduce the confusion in the reader faced by multiple different types of artefact. My first draft is in http://www.sparksure.com/resources/Rosetta_Text.txt. Cheers, Phil