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:
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.