Re: SPARK : third example for Roesetta - reviewers welcome

[Phil Thornley <phil.jpthornley@gmail.com>]

On 18 Aug, 11:44, Phil Thornley <phil.jpthorn...@gmail.com> wrote:
> On 17 Aug, 23:15, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
> 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.  So 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_analysis
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