Re: SPARK : third example for Roesetta - reviewers welcome

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

On 17 Aug, 10:15, Phil Thornley <phil.jpthorn...@gmail.com> 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).  I'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