SPARK User’s Guide
Copyright (C) 2011-2022, AdaCore and Capgemini Engineering
Permission is granted to copy, distribute and/or modify this document under the terms of the GNU Free Documentation License, Version 1.1 or any later version published by the Free Software Foundation; with no Invariant Sections, with no Front-Cover Texts, and with no Back-Cover Texts. A copy of the license is included in the section entitled ‘GNU Free Documentation License’.
- 1. Getting Started with SPARK
- 2. Introduction
- 3. Installation of GNATprove
- 4. Identifying SPARK Code
- 5. Overview of SPARK Language
- 5.1. Language Restrictions
- 5.2. Subprogram Contracts
- 5.3. Package Contracts
- 5.4. Type Contracts
- 5.5. Specification Features
- 5.5.1. Aspect
Constant_After_Elaboration
- 5.5.2. Aspect
No_Caching
- 5.5.3. Aspect
Relaxed_Initialization
and Ghost AttributeInitialized
- 5.5.4. Aspect
Side_Effects
- 5.5.5. Attribute
Loop_Entry
- 5.5.6. Attribute
Old
- 5.5.7. Attribute
Result
- 5.5.8. Aggregates
- 5.5.9. Conditional Expressions
- 5.5.10. Declare Expressions
- 5.5.11. Expression Functions
- 5.5.12. Ghost Code
- 5.5.13. Quantified Expressions
- 5.5.1. Aspect
- 5.6. Assertion Pragmas
- 5.7. Overflow Modes
- 5.8. Object Oriented Programming and Liskov Substitution Principle
- 5.9. Pointer Support and Dynamic Memory Management
- 5.10. Concurrency and Ravenscar Profile
- 5.11. SPARK Libraries
- 5.11.1. SPARK Library
- 5.11.2. Big Numbers Library
- 5.11.3. Functional Containers Library
- 5.11.4. Formal Containers Library
- 5.11.5. Containers and Executablity
- 5.11.6. SPARK Lemma Library
- 5.11.7. Higher Order Function Library
- 5.11.8. Input-Output Libraries
- 5.11.9. Strings Libraries
- 5.11.10. C Strings Interface
- 5.11.11. Addresses to Access Conversions
- 5.11.12. Cut Operations
- 6. SPARK Tutorial
- 7. Formal Verification with GNATprove
- 7.1. How to Run GNATprove
- 7.1.1. Setting Up a Project File
- 7.1.2. Running GNATprove from the Command Line
- 7.1.3. Using the GNAT Target Runtime Directory
- 7.1.4. Specifying the Target Architecture and Implementation-Defined Behavior
- 7.1.5. Running GNATprove from GNAT Studio
- 7.1.6. Running GNATprove from Visual Studio Code
- 7.1.7. Running GNATprove from GNATbench
- 7.1.8. Running GNATprove Without a Project File
- 7.1.9. GNATprove and Manual Proof
- 7.1.10. How to Speed Up a Run of GNATprove
- 7.1.11. GNATprove and Network File Systems or Shared Folders
- 7.2. How to View GNATprove Output
- 7.3. How to Use GNATprove in a Team
- 7.4. How to Write Subprogram Contracts
- 7.4.1. Generation of Dependency Contracts
- 7.4.2. Infeasible Subprogram Contracts
- 7.4.3. Writing Contracts for Program Integrity
- 7.4.4. Writing Contracts for Functional Correctness
- 7.4.5. Writing Contracts on Main Subprograms
- 7.4.6. Writing Contracts on Imported Subprograms
- 7.4.7. Contextual Analysis of Subprograms Without Contracts
- 7.4.8. Subprogram Termination
- 7.5. How to Write Object Oriented Contracts
- 7.6. How to Write Package Contracts
- 7.7. How to Write Loop Invariants
- 7.7.1. Automatic Unrolling of Simple For-Loops
- 7.7.2. Automatically Generated Loop Invariants
- 7.7.3. The Four Properties of a Good Loop Invariant
- 7.7.4. Proving a Loop Invariant in the First Iteration
- 7.7.5. Completing a Loop Invariant to Prove Checks Inside the Loop
- 7.7.6. Completing a Loop Invariant to Prove Checks After the Loop
- 7.7.7. Proving a Loop Invariant After the First Iteration
- 7.8. How to Investigate Unproved Checks
- 7.9. GNATprove by Example
- 7.1. How to Run GNATprove
- 8. Applying SPARK in Practice
- 8.1. Levels of Software Assurance
- 8.2. Objectives of Using SPARK
- 8.2.1. Safe Coding Standard for Critical Software
- 8.2.2. Prove Absence of Run-Time Errors (AoRTE)
- 8.2.3. Prove Correct Integration Between Components
- 8.2.4. Prove Functional Correctness
- 8.2.5. Ensure Correct Behavior of Parameterized Software
- 8.2.6. Safe Optimization of Run-Time Checks
- 8.2.7. Address Data and Control Coupling
- 8.2.8. Ensure Portability of Programs
- 8.3. Project Scenarios
- A. Command Line Invocation
- B. Alternative Provers
- C. Project Attributes
- D. Implementation Defined Pragmas
- E. Additional Annotate Pragmas
- Annotation for Justifying Check Messages
- Annotation for Skipping Parts of the Analysis for an Entity
- Annotation for Handling Modular Types as Integers in All Provers
- Annotation for Overflow Checking on Modular Types
- Annotation for Simplifying Iteration for Proof
- Annotation for Inlining Functions for Proof
- Annotation for Referring to a Value at the End of a Local Borrow
- Annotation for Accessing the Logical Equality for a Type
- Annotation for the Predefined Equality of Private Types
- Annotation for Enforcing Ownership Checking on a Private Type
- Annotation for Instantiating Lemma Procedures Automatically
- Annotation for Managing the Proof Context
- Annotation for Handling Specially Higher Order Functions
- Annotation for Handlers
- Annotation for Container Aggregates
- Annotation for Mutable IN Parameters
- F. Environment Variable
- G. GNATprove Limitations
- H. Portability Issues
- I. Semantics of Floating Point Operations
- J. SPARK Architecture, Quality Assurance and Maturity
- K. GNU Free Documentation License