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!x21g2000yqa.googlegroups.com!not-for-mail From: Phil Thornley Newsgroups: comp.lang.ada Subject: Re: SPARK : third example for Roesetta - reviewers welcome Date: Fri, 20 Aug 2010 01:37:53 -0700 (PDT) Organization: http://groups.google.com Message-ID: <9a08d5d4-b0aa-4c99-b8e6-95ff22e768e0@x21g2000yqa.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> <1ddee5a6-fc25-4d23-bebd-3364923d0aa5@z10g2000yqb.googlegroups.com> <7cf71c68-4faf-4a7b-a350-405ff7f12ff9@z10g2000yqb.googlegroups.com> 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 1282293473 17593 127.0.0.1 (20 Aug 2010 08:37:53 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Fri, 20 Aug 2010 08:37:53 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: x21g2000yqa.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:13527 Date: 2010-08-20T01:37:53-07:00 List-Id: On 18 Aug, 11:44, Phil Thornley wrote: > On 17 Aug, 23:15, "Dmitry A. Kazakov" > wrote: > [...]> On Tue, 17 Aug 2010 12:53:18 -0700 (PDT), Phil Thornley wrote: > > > OK - I discovered that Rosetta Code has Encyclopedia pages, that can > > > be used for any topic that doesn't fit in anywhere else. =A0So I've > > > written a very short bit for the 'Category:SPARK' page which is what > > > is linked to by the language name. > > > Integrate it here, please: > > >http://rosettacode.org/wiki/SPARK > > Yes - will do. Now done. > > > This page will contain links to > > > the Altran-Praxis home page and to their page about SPARK. > > > Here is the standard place for this: > > >http://rosettacode.org/wiki/Category:SPARK_Implementations > > OK - I'll use this Now done. > > > 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. > > Maybe I don't need these - I've just discovered the Wiki page about > SPARK:http://en.wikipedia.org/wiki/SPARK_(programming_language) > > > Could you also write a short encyclopedia article about proofs and link= to > > SPARK specific pages from there? > > I've also just discovered the Wiki page about static analysis - which > should do for this purpose:http://en.wikipedia.org/wiki/Static_code_analy= sis I've ended up referencing the SPARK Wiki page to get a description of the language and tools, but added an encyclopedia page about the SPARK proof process. (I want this there so that the tasks can reference it when describing how they are proved.) I've updated the Binary Search example to show both versions of the package. I've also edited the other two examples to get syntax colouring working for them. Please have a look at all of these and make any further improvements you thing approriate. Cheers, Phil