SPARK at Wikipedia

SPARK at Wikipedia

[Martin Krischik]

Hello,

There is some discussion on SPARK going on on Wikipedia and it's far to
theoretical for me:

http://en.wikipedia.org/wiki/Talk:SPARK_programming_language

Can anybody here answer the questions at hand?

Martin
-- 
mailto://krischik@users.sourceforge.net
Ada programming at: http://ada.krischik.com

Re: SPARK at Wikipedia

[Jeffrey R. Carter]

Martin Krischik wrote:
> 
> There is some discussion on SPARK going on on Wikipedia and it's far to
> theoretical for me:
> 
> http://en.wikipedia.org/wiki/Talk:SPARK_programming_language
> 
> Can anybody here answer the questions at hand?

I might be able to, but I know Rod Chapman and Peter Amey read c.l.a, so it's 
probably best to let them deal with this.

However, "erroneous execution" is defined in ARM 1.1.5:

     "Erroneous execution.

       "In addition to bounded errors, the language rules define certain kinds 
of errors as leading to erroneous execution. Like bounded errors, the 
implementation need not detect such errors either prior to or during run time. 
Unlike bounded errors, there is no language-specified bound on the possible 
effect of erroneous execution; the effect is in general not predictable."

An "erroneous program" is not defined, but is generally understood to mean a 
program that leads to erroneous execution.

-- 
Jeff Carter
"Alms for an ex-leper!"
Monty Python's Life of Brian
75

Re: SPARK at Wikipedia

[Rod Chapman]

Thanks for spotting this!  I have added a couple of notes to this
discussion.
 - Rod, SPARK Team

Re: SPARK at Wikipedia

[Martin Krischik]

Rod Chapman wrote:

> Thanks for spotting this!  I have added a couple of notes to this
> discussion.

Of corse you can allways change the actual test as well:

http://en.wikipedia.org/wiki/SPARK_programming_language

Martin
-- 
mailto://krischik@users.sourceforge.net
Ada programming at: http://ada.krischik.com