SPARK Technical References

Where indicated, PDF downloads of these publications are available for download here. Where PDF is not available, please contact us for how to obtain hardcopies.

Release notes

The SPARK Toolset v7.5 Release Note (PDF – 72k).

The SPARK Toolset v7.4 Release Note (PDF – 84k).

The SPARK Toolset v7.31 Release Note (PDF – 110k).

The SPARK Toolset v7.3 Release Note (PDF – 151k).

These contain detailed information on the new features of Releases 7.3 through 7.5, and a summary of all changes between Releases 2.0 and 7.4.

Language Definition and Reference

"SPARK95 — The SPADE Ada 95 Kernel (Including RavenSPARK)"
(PDF 299kb) Praxis, 2006.
This report defines SPARK 95, an annotated subset of the Ada 95 language. It describes the differences between SPARK 95 and Ada 95 and defines the SPARK 95 syntax.
Note
This report is written in the style of the Ada 95 Language Reference Manual, and assumes familiarity with the structure and terminology of that document. For a more friendly introduction to SPARK, try the SPARK Book.

"SPARK – The SPADE Ada Kernel"
Praxis, 2006.
This report defines SPARK, an annotated subset of the Ada 83 language. It describes the differences between SPARK and Ada and also defines the SPARK syntax. Please contact us if you'd like a hardcopy of this report.

"The Formal Semantics of SPARK83"
Ian O'Neill et. al., Program Validation Limited 1994.

These semantics reflect the SPARK83 language as-was in 1994. Since then, the language has developed in several significant areas. In particular, these semantics do not reflect SPARK95.

These documents are in PostScript format.

Volume 1 – Static Semantics. Please contact us if you'd like a hardcopy of this report.
Volume 2 – Dynamic Semantics. Please contact us if you'd like a hardcopy of this report.

The SPARK semantics were a product of QinetiQ's Systems Assurance Group's research programme funded by TG10 of MOD's CRP.

RavenSPARK

"The SPARK Ravenscar Profile" (PDF 265kb)
Praxis, 2006.
This report acts as a idiom guide and rationale for the RavenSPARK extensions to SPARK.

"RavenSPARK Design for the Minepump Case Study" (PDF 177kb)
Praxis, 2003.
This report contains a worked example of the design of a RavenSPARK program.

INFORMED Design

"The INFORMED Design Method for SPARK" Peter Amey, Praxis, 1999, 2001. This paper is available upon request. Please contact us for details.

Quick Reference Guides

These guides contain quick-reference information for the SPARK language and toolset release 6.1 and above. The first provides quick reference for the main tools and annotations. The second illustrates various SPARK design patterns.

Quick Reference Guide 1 – Toolset and Annotations (PDF – 95kbytes)
Quick Reference Guide 2 – Patterns (PDF – 87kbytes)
Quick Reference Guide 3 – RavenSPARK (PDF – 96kbytes)
Quick Reference Guide 4 – Proof (PDF – 76kbytes)