The Eight Reasons For Using SPARK

Based on our many years of experience with our customers using SPARK in their projects, we have come up with a list of eight objectives that are most commonly targeted when using SPARK. Most projects only target a few of them, but in theory one could try to achieve all of them with SPARK on a project. This list may be useful for those who want to assess if the SPARK technology can be of benefit in their context, and to existing SPARK users to compare their existing practice with what others do. Each objective is described with some details in a separate section of the SPARK User's Guide.

Objectives 1 to 4 are applicable to most projects:

• Objective 1 (the simplest): Safe Coding Standard for Critical Software
• Objective 2 (the most common): Prove Absence of Run-Time Errors (AoRTE)
• Objective 3 (a touch of functional): Prove Correct Integration Between Components
• Objective 4 (the richest): Prove Functional Correctness

Objectives 5 to 8 address specific issues:

• Objective 5 Ensure Correct Behavior of Parameterized Software
• Objective 6 Safe Optimization of Run-Time Checks
• Objective 7 Address Data and Control Coupling
• Objective 8 Ensure Portability of Programs

If you feel that your own objectives for using SPARK are not represented in the list above, please let us know. Our aim is to enrich this list in the future to represent most (if not all) SPARK projects.