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.net-security.org/secworld.php?id=6619 (recent open source project) —Preceding unsigned comment added by Parallelized (talk • contribs) 21:19, 13 March 2009 (UTC)[reply]

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]

Copyvio

Looks like chunks have been copied from this website: [1]. "The "SPARK Examiner" (part of the "SPARK Toolset") performs two kinds of static analysis...." etc — Matt Crypto 12:03, 15 October 2009 (UTC)[reply]