Re: SPARK code samples

[Ada novice <ycalleecharan@gmx.com>]

On Aug 11, 7:45 pm, "(see below)" <yaldni...@blueyonder.co.uk> wrote:
> On 11/08/2010 18:39, in article
> bbc93c1c-9e12-4682-912d-9ff961c3a...@p7g2000yqa.googlegroups.com, "Ada
>
> novice" <ycalleecha...@gmx.com> wrote:
> > On Aug 11, 7:32 pm, Mark Lorenzen <mark.loren...@gmail.com> wrote:
>
> >> 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.
>
> > So you're saying not to think in terms of Ada when approaching SPARK?
> > I have yet to lay my hands on a copy of Barnes' SPARK book to learn
> > SPARK syntax and I can understand that SPARK is not just Ada with some
> > annotations.
>
> Yebbut. It is.
>
> --
> Bill Findlay
> <surname><forename> chez blueyonder.co.uk


In this article: "The Exterminators---A small British firm shows that
software bugs aren't inevitable" available at

http://spectrum.ieee.org/computing/software/the-exterminators/0

it is mentioned, I quote: "that the two-step translation--from English
to Z and from Z to Spark--lets engineers keep everything in mind"

I haven't yet personally written any programs in SPARK but does one
has necessarily to understand the Z language in order to use SPARK? I
recall reading somewhere that Barnes's book doesn't discuss the Z
language (I might be wrong though).


Thanks
YC