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 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.[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 SPARK 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 almost 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 course the later proves you right. --Krischik ^T 14:53, 20 February 2006 (UTC)[reply]

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

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

Resources

TODO: clean up, group into sections and provide title for links listed

http://www.techworld.com/opsys/news/index.cfm?newsid=2275 —Preceding unsigned comment added by Parallelized (talk • contribs) 22:59, 4 May 2008 (UTC)[reply]

http://www.ddj.com/embedded/199905389 —Preceding unsigned comment added by 82.83.112.152 (talk) 20:46, 30 December 2007 (UTC)[reply]
SPARK 95 - The SPADE Ada 95 Kernel (excluding RavenSPARK) —Preceding unsigned comment added by 82.83.112.152 (talk) 22:48, 30 December 2007 (UTC)[reply]
http://www.esafetycase.com/pdfs/spark_common_criteria.pdf —Preceding unsigned comment added by 82.83.76.5 (talk) 09:30, 26 January 2008 (UTC)[reply]

http://www.era.co.uk/assc/docs/C++_Strategy_Paper.pdf

More Background Info

Quoting some contents from the manufacturer's webpage here to encourage inclusion of some of the details in the actual wikipedia entry, if this should turn out to be unacceptable, please feel free to remove the contents but leave the link, thanks!

Taken from http://www.praxis-his.com/sparkada/language.asp:

"SPARK is a subset of the Ada language. It includes Ada constructs regarded as essential for the construction of complex software, such as packages, private types, typed constants, functions with structured values, and the library system. It excludes tasks, exceptions, generic units, access types, use clauses, type aliasing, anonymous types, default values in record declarations, default subprogram parameters, goto statements, and declare statements."

Might make sense to incorporate some of this info by summarizing and rewording the essentials of it.

Also:

"Mandatory Annotations The requirements for analysis and verification imply a need for (non-Ada) formal comments which supply extra information to the SPARK tools. These annotations include: • global definitions in procedures (which declare 'imported' or 'exported' global variables) or functions (which import such variables); • dependency relations in procedures (which specify the imported variables which are required to derive the value of each exported variable); • the inherit clause in a SPARK package declaration (which restricts penetration of the package to items specifically imported from other packages); • the own variable clause in a SPARK package specification (which makes actions on the package state visible to analysis tools); • the initialisation annotation in a SPARK package specification (which indicates the initialisation by the package of its own state).

And:

"Proof Contexts These are special non-mandatory annotations which support the formal proof of SPARK programs. They are written in an expression language which is an extension of Ada's. Each proof context is associated with a particular location in the code: • the precondition of a procedure or function is associated with the begin of its body: it specifies conditions under which the procedure or function should be called; • the postcondition of a procedure (or the return annotation of a function) is associated with the end of the subprogram body: it defines the expected final state; • each assert statement (eg a loop invariant) or check statement (ie a well-formation statement) is located between two executable statements: it specifies the state expected of the program at that point. " —Preceding unsigned comment added by Parallelized (talk • contribs) 11:44, 28 January 2008 (UTC) [reply]