 |
Introduction to SPARK
What is SPARK?
SPARK is a high level programming language and toolset designed
for writing software for high integrity applications.
Why should I use SPARK?
SPARK gives confidence in the correctness of code –
it is verifiable. Early detection and prevention of defects
reduces the cost of verification and validation. SPARK is
a very portable language and has minimal runtime system requirements.
What language is SPARK based on?
SPARK should be thought of as a language in its own right,
however it is based on a subset of the Ada language, and designed
in such a way that all SPARK programs are legal Ada programs.
What is the SPARK toolset?
The SPARK toolset consists of the Examiner, the Simplifier
and the Checker. The Examiner performs:
- checking of SPARK language syntactic and static
semantic rules
- data and information
flow analysis
- generation of verification
conditions for:
- absence of run time errors
- partial correctness
- safety and security properties
The Simplifier and Checker automate the discharging of proof
obligations.
Who uses SPARK?
SPARK is used on safety-critical systems, primarily in the
Aerospace, Defence, Rail and Security industry. It is suitable
for use wherever there is a desire to produce high-quality
software which behaves in a predictable manner.
How long has SPARK been around?
SPARK was developed in the late 1970s and 1980s. It has been
in use on major projects since 1990.
How difficult is it to learn?
SPARK will be familiar to programmers with knowledge of imperative
languages such as C, Java and Ada. There is some effort involved
with learning how to use the annotations correctly. As you become
more fluent, the apparent "extra cost" of producing
SPARK falls to effectively zero, for a significant quality improvement.
We offer training courses for both basic and advanced SPARK.
How do I get hold of it?
Please contact us. If you are interested in evaluating SPARK
please contact us for advice and support.
What support do I get?
Full support will usually be included in the cost of the toolset.
This includes access to our experienced SPARK team at Praxis
High Integrity Systems and any upgrades.
How much does it cost?
The cost of the SPARK Toolset depends on:
- How many "seats" you need - we licence the tools
using a "floating" network scheme. Additional
seats are less expensive.
- The criticality
of your project - this would largely determine if you need
the Proof Checker tool, which is priced as a separate option.
- Do you need support
for the RavenSPARK (i.e. tasking) language, or just standard
SPARK? Again, RavenSPARK is priced as a separate option.
For a quote, please contact us.
Do you support academics?
We are happy to supply a free of charge, fully supported SPARK
Toolset to academics for teaching and/or research. The toolset
can be distributed to your students to install on their machines
and/or your departmental machines as you see fit. Please contact us.
Where can I find out more?
The rest of this website contains a lot more detailed information
about SPARK – its philosophy and its use. For an excellent
guide to the language, look at John Barnes’ SPARK book.
If you have any further questions please contact us. |
|
