Re: SPARK code samples

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

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. Although SPARK
constantly evolves it will never evolve into a language with the same
feature-set as Ada - no matter how well tested all Ada festures one
day will be.