SPARK User’s Guide¶
Copyright (C) 2011-2021, AdaCore and Altran UK Ltd
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. Attribute
Old
- 5.5.4. Attribute
Result
- 5.5.5. Attribute
Loop_Entry
- 5.5.6. Delta Aggregates
- 5.5.7. Conditional Expressions
- 5.5.8. Quantified Expressions
- 5.5.9. Declare Expressions
- 5.5.10. Expression Functions
- 5.5.11. Ghost Code
- 5.5.12. Aspect
Relaxed_Initialization
and AttributeInitialized
- 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
- 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. Using CodePeer Static Analysis
- 7.1.6. Running GNATprove from GNAT Studio
- 7.1.7. Running GNATprove from GNATbench
- 7.1.8. GNATprove and Manual Proof
- 7.1.9. How to Speed Up a Run of GNATprove
- 7.1.10. 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. Writing Contracts for Program Integrity
- 7.4.3. Writing Contracts for Functional Correctness
- 7.4.4. Writing Contracts on Main Subprograms
- 7.4.5. Writing Contracts on Imported Subprograms
- 7.4.6. Contextual Analysis of Subprograms Without Contracts
- 7.4.7. 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.10. Examples in the Toolset Distribution
- 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. Aspects or Pragmas Specific to GNATprove
- Using Annotations to Justify Check Messages
- Using Annotations to Specify Possibly Nonreturning Procedures
- Using Annotations to Request Proof of Termination
- Using Annotations to Request Overflow Checking on Modular Types
- Customize Quantification over Types with the Iterable Aspect
- Inlining Functions for Proof
- Referring to a Value at the End of a Local Borrow
- F. GNATprove Limitations
- G. Portability Issues
- H. Semantics of Floating Point Operations
- I. SPARK Architecture, Quality Assurance and Maturity
- J. GNU Free Documentation License