Talk:SPARK (programming language)

From Wikipedia, the free encyclopedia

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.

[edit] erroneous

Most Ada - and as such most SPARK - programmers will consider erroneous as "not defined in the Reference Manual (RM, ISO 8652)".

Examples (in C):

signed   int x = -1;
unsigned int y = x;   // depends on int beeing 16bit, 32bit or 64bit 

char a[] = malloc(100);

free (a);

if (a [1] == 'A')  // in a multi tasking environment memory might be reallocated
  {
  }

With the aid of Unchecked_Conversion and Unchecked_Deallocation both examples can be replicated in Ada and they would be just as buggy. They can not, however, be replicated in SPARK as SPARC does not allow Unchecked_Conversion and uses no heap memory.

Now it is quite possible to read the RM front to back and strike out all features with "undefined behavior" or similar. As a result you get a programming language without ambiguities. No need for "believed to".

Of course one can still make buggy programms SPARK. i.E.:

π : constant Float := 4.141_592_653_589_793_238;

Noticed the 4 at the beginning ;-).

I leave it to the native english speakers to fix the wording.

--Krischik ^T 07:33, 20 February 2006 (UTC)

Striking out the features with "undefined behavior" or similar is the easy part. What about the cases where the wording says "X is black" in one section and "X is white" in another? Cross checking the text for these kinds of inconsistencies is rather hard (undecidable?).

That's probably the reason why amost all ISO standards for programming languages are late :-( . --Krischik ^T 14:53, 20 February 2006 (UTC)

The discussion of the formal definition of the language is a smoke screen. There are at least three formal definitions of C (they use different formalisms). Having a formal definition is the easy part. You still need the tools to check the formal definitions for various properties.

Derek farn 12:38, 20 February 2006 (UTC)

Luckily Ada only got one formal definition (ISO 8652), a test suite (ISO 18009) to go with it and a list of problems (http://www.ada-auth.org/ais.html). Of corse the later proves you right. --Krischik ^T 14:53, 20 February 2006 (UTC)

ISO 8652 is not a formal definition, it is an informal definition written in English that attempts to be rigorous. There was a formal definition (ie, using a mathematical formalism) produced by some academics (Danish?). The SPARC people also claim it has a formal definition (I don't know the status of this work).

Derek farn 15:23, 20 February 2006 (UTC)

A formal (i.e. mathematical) definition of SPARK was constructed in 1996. These documents are available from us if anyone is interested. Unfortunately, we have not had the resources to keep this work up to date, so the formal def does not cover some of the more advanced features of SPARK95, RavenSPARK and so on. Rod Chapman 09:27, 21 February 2006 (UTC), SPARK Team, Praxis