Re: SPARK code samples

[Mark Lorenzen <mark.lorenzen@gmail.com>]

On 11 Aug., 18:33, "(see below)" <yaldni...@blueyonder.co.uk> wrote:
> On 11/08/2010 17:07, in article
> fa1507ef-77a8-4a28-b271-2293c5115...@j8g2000yqd.googlegroups.com, "Mark
>
> Lorenzen" <mark.loren...@gmail.com> wrote:
> > On 11 Aug., 13:38, Ada novice <ycalleecha...@gmx.com> wrote:
>
> >> Thanks for this information. I'm interested to learn SPARK. If I
> >> understand correctly, SPARK aligns itself well with Ada 95 and not yet
> >> with Ada 05. Is this because of the strictness of SPARK to provide
> >> highly reliable codes and hence it contains only well-tested features
> >> (subset of Ada features)? It would be interesting to see some SPARK
> >> codes on the wiki page building over time.
>
> > Not quite. SPARK is a proper subset of Ada and is amenable to static
> > analysis. This has (in principle) nothing to do with if an Ada feature
> > is well-tested or not. You should think of SPARK as a language in its
> > own right and not as a subset of some other language.
>
> Why?
>
> --
> Bill Findlay
> <surname><forename> chez blueyonder.co.uk

I take it you refer to my last sentence.

First of all because SPARK is not only a set of restrictions imposed
on the Ada language, SPARK also mandates the use of annotations (and
even more so if you want to prove program correctnes). As SPARK
annotations are written as Ada comments, it is true that every SPARK
program is also an Ada program and that may be why people often think
of SPARK as "just" a subset of Ada [1].

I also think there is a risk of getting stuck with SPARK if you try to
design a SPARK program with Ada in mind. You constantly bump into a
useful feature of Ada that is not in SPARK (discriminated types, array
slicing etc.) and you think "why the h... isn't that a part of SPARK
when it's so easy to do in Ada?". So it's probably a way of tuning
your mindset from "Ada with restrictions" into SPARK.

[1] Purists may argue that even with the presence formal annotations,
every SPARK program will be a member of the set of all Ada programs
that include every permutation of every legal comment in every legal
place. Or what?

- Mark L