SPARK
SPARK Technical References
Where indicated, PDF downloads of these publications are available for download
here. Where PDFs are not available, please
contact us
for how to obtain hardcopies.
Release notes
SPARK Toolset v9.0 Release Note
/ 291k PDF
SPARK Toolset v7.6 Release Note
/ 196k PDF
SPARK Toolset v7.5 Release Note
/ 72k PDF
SPARK Toolset v7.4 Release Note
/ 84k PDF
SPARK Toolset v7.31 Release Note
/ 110k PDF
SPARK Toolset v7.3 Release Note
/ 151k PDF
These contain detailed information on the new features of Releases 7.3 through 9.0,
and a summary of all changes between Releases 2.0 and 9.0.
Language Definition and Reference
"SPARK95 - The SPADE Ada 95 Kernel (Including RavenSPARK)"
/ 299k PDF
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.
"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" / 341k PDF
This report acts as a idiom guide and rationale for the RavenSPARK
extensions to SPARK.
"RavenSPARK Design for the
Minepump Case Study" / 177k PDF
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 / 95k PDF
Quick Reference Guide 2 –
Patterns / 87k PDF
Quick Reference Guide 3 –
RavenSPARK / 96k PDF
Quick Reference Guide 4 –
Proof / 76k PDF
Please feel free to contact us if you find any ommissions
or errors.
Please email us : sparkinfo@altran-praxis.com.