Talk:SPARK (programming language)

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)[reply]

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)[reply]

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)[reply]

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)[reply]

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)[reply]

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)[reply]