Talk:SPARK (programming language)/Archive 1

Archive 1

Comment

To quote: "A SPARK program "... "can never be erroneous."

This article should be revised by someone with Spark expertise. I doubt a SPARK program can "never be erroneous". I am not an expert in SPARK though and am just making a comment --L505

I am not an expert either, but I think this was simply a poor choice of language on the original author. I have changed "erroneous" to "ambiguous" which seems more correct - while an full Ada program can be ambiguous and result in different behaviour from different compilers SPARK uses a subset of Ada that makes this impossible. Leland McInnes 02:56, 10 January 2006 (UTC)

It is my experience that SPARK users promote it with almost religious fervor, so descriptions of it do tend to cast it as being shining white free of any dark corners. Perhaps the wording "... while eliminating all its potential ambiguities and insecurities." should really be "... and it believed to eliminate all its potential ambiguities and insecurities." Also the question of ambiguities and insecurities caused by differences in behavior between the "formal comments" and the actual code ought to be mentioned. Derek farn 16:17, 18 February 2006 (UTC)

---

Erroneous execution is a term defined by the Ada reference manual. It is somewhat similar to the concept of undefined execution in C. Anyway, we are confident that a SPARK program, having passed all the static analysis and verification required by the language, can never exhibit such a behaviour. The original wording could be improved, but the term "erroneous" is used quite deliberately with its LRM meaning here, so we would prefer it to remain. Rod Chapman 09:27, 21 February 2006 (UTC), SPARK Team, Praxis.