Archives

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]

History lacks creation date

Having just learnt of SPARK I was interested in when it was created and a timeline of its adoption over Ada, but bizarrely the only year mentioned is for Spark 2014 "April 30, 2014". Ironically it is the only one with its actual creation year as part of the name, I have no idea for SPARK83, SPARK95 and SPARK2005.

I would update the page myself but I am aware that this language along with Ada is heavily used within the military industrial complex. Media articles written with state approval are unlikely to present an accurate picture. BeardedChimp (talk) 22:48, 8 October 2024 (UTC)[reply]