From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: 103376,641efb0456c6f090 X-Google-Attributes: gid103376,public X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news1.google.com!news3.google.com!newshub.sdsu.edu!elnk-nf2-pas!newsfeed.earthlink.net!stamper.news.pas.earthlink.net!newsread3.news.pas.earthlink.net.POSTED!a6202946!not-for-mail From: "Jeffrey R. Carter" Organization: jrcarter at acm dot org User-Agent: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-US; rv:1.7.12) Gecko/20050915 X-Accept-Language: en-us, en MIME-Version: 1.0 Newsgroups: comp.lang.ada Subject: Re: SPARK at Wikipedia References: <1485989.F37Gpsk2YC@linux1.krischik.com> In-Reply-To: <1485989.F37Gpsk2YC@linux1.krischik.com> Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit Message-ID: Date: Tue, 21 Feb 2006 05:03:36 GMT NNTP-Posting-Host: 67.150.73.203 X-Complaints-To: abuse@earthlink.net X-Trace: newsread3.news.pas.earthlink.net 1140498216 67.150.73.203 (Mon, 20 Feb 2006 21:03:36 PST) NNTP-Posting-Date: Mon, 20 Feb 2006 21:03:36 PST Xref: g2news1.google.com comp.lang.ada:3029 Date: 2006-02-21T05:03:36+00:00 List-Id: 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