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
  • 3.1. System Requirements
  • 3.2. Installation under Windows
  • 3.3. Installation under Linux/Mac
• 4. Identifying SPARK Code
  • 4.1. Mixing SPARK Code and Ada Code
  • 4.2. Project File Setup
    • 4.2.1. Setting the Default SPARK_Mode
    • 4.2.2. Specifying Files To Analyze
    • 4.2.3. Excluding Files From Analysis
    • 4.2.4. Using Multiple Projects
  • 4.3. Using SPARK_Mode in Code
    • 4.3.1. Basic Usage
    • 4.3.2. Consistency Rules
    • 4.3.3. Examples of Use
• 5. Overview of SPARK Language
  • 5.1. Language Restrictions
    • 5.1.1. Excluded Ada Features
    • 5.1.2. Sizes of Objects
    • 5.1.3. Data Validity
    • 5.1.4. Data Initialization Policy
    • 5.1.5. Memory Ownership Policy
    • 5.1.6. Absence of Interferences
    • 5.1.7. Raising Exceptions and Other Error Signaling Mechanisms
    • 5.1.8. Nonreturning Procedures
    • 5.1.9. Analysis of Generics
  • 5.2. Subprogram Contracts
    • 5.2.1. Preconditions
    • 5.2.2. Postconditions
    • 5.2.3. Contract Cases
    • 5.2.4. Data Dependencies
    • 5.2.5. Flow Dependencies
    • 5.2.6. State Abstraction and Contracts
    • 5.2.7. Subprogram Variant
  • 5.3. Package Contracts
    • 5.3.1. State Abstraction
    • 5.3.2. Package Initialization
    • 5.3.3. Package Initial Condition
    • 5.3.4. Interfaces to the Physical World
  • 5.4. Type Contracts
    • 5.4.1. Scalar Ranges
    • 5.4.2. Record Discriminants
    • 5.4.3. Predicates
    • 5.4.4. Type Invariants
    • 5.4.5. Default Initial Condition
  • 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 Attribute Initialized
  • 5.6. Assertion Pragmas
    • 5.6.1. Pragma Assert
    • 5.6.2. Pragma Assertion_Policy
    • 5.6.3. Loop Invariants
    • 5.6.4. Loop Variants
    • 5.6.5. Pragma Assume
    • 5.6.6. Pragma Assert_And_Cut
  • 5.7. Overflow Modes
  • 5.8. Object Oriented Programming and Liskov Substitution Principle
    • 5.8.1. Class-Wide Subprogram Contracts
    • 5.8.2. Mixing Class-Wide and Specific Subprogram Contracts
    • 5.8.3. Dispatching Calls and Controlling Operands
    • 5.8.4. Dynamic Types and Invisible Components
  • 5.9. Pointer Support and Dynamic Memory Management
    • 5.9.1. Access to Objects and Ownership
    • 5.9.2. Deallocation
    • 5.9.3. Observing
    • 5.9.4. Borrowing
    • 5.9.5. Traversal Functions
    • 5.9.6. Subprogram Pointers
    • 5.9.7. Contracts for Subprogram Pointers
  • 5.10. Concurrency and Ravenscar Profile
    • 5.10.1. Tasks and Data Races
    • 5.10.2. Task Contracts
    • 5.10.3. Protected Objects and Deadlocks
    • 5.10.4. Suspension Objects
    • 5.10.5. State Abstraction and Concurrency
    • 5.10.6. Project-wide Tasking Analysis
    • 5.10.7. Interrupt Handlers
  • 5.11. SPARK Libraries
    • 5.11.1. Big Numbers Library
    • 5.11.2. Functional Containers Library
    • 5.11.3. Formal Containers Library
    • 5.11.4. SPARK Lemma Library
    • 5.11.5. Higher Order Function Library
    • 5.11.6. SPARK Heap Library
    • 5.11.7. Input-Output Libraries
    • 5.11.8. Strings Libraries
• 6. SPARK Tutorial
  • 6.1. Writing SPARK Programs
    • 6.1.1. Checking SPARK Legality Rules
    • 6.1.2. Checking SPARK Initialization Policy
    • 6.1.3. Writing Functional Contracts
  • 6.2. Testing SPARK Programs
  • 6.3. Proving SPARK Programs
• 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.2.1. The Analysis Report Panel
    • 7.2.2. The Analysis Results Summary File
    • 7.2.3. Categories of Messages
    • 7.2.4. Effect of Mode on Output
    • 7.2.5. Description of Messages
    • 7.2.6. Understanding Counterexamples
  • 7.3. How to Use GNATprove in a Team
    • 7.3.1. Possible Workflows
    • 7.3.2. Suppressing Warnings
    • 7.3.3. Suppressing Information Messages
    • 7.3.4. Justifying Check Messages
    • 7.3.5. Sharing Proof Results with Others
    • 7.3.6. Sharing Proof Results Via a Memcached Server
    • 7.3.7. Managing Assumptions
  • 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.5.1. Object Oriented Code Without Dispatching
    • 7.5.2. Writing Contracts on Dispatching Subprograms
    • 7.5.3. Writing Contracts on Subprograms with Class-wide Parameters
  • 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.8.1. Investigating Incorrect Code or Assertion
    • 7.8.2. Investigating Unprovable Properties
    • 7.8.3. Investigating Prover Shortcomings
    • 7.8.4. Looking at Machine-Parsable GNATprove Output
    • 7.8.5. Understanding Proof Strategies
  • 7.9. GNATprove by Example
    • 7.9.1. Basic Examples
    • 7.9.2. Loop Examples
    • 7.9.3. Manual Proof Examples
  • 7.10. Examples in the Toolset Distribution
    • 7.10.1. Individual Subprograms
    • 7.10.2. Single Units
    • 7.10.3. Multi-Units Demos
• 8. Applying SPARK in Practice
  • 8.1. Levels of Software Assurance
    • 8.1.1. Levels of SPARK Use
    • 8.1.2. Stone Level - Valid SPARK
    • 8.1.3. Bronze Level - Initialization and Correct Data Flow
    • 8.1.4. Silver Level - Absence of Run-time Errors (AoRTE)
    • 8.1.5. Gold Level - Proof of Key Integrity Properties
    • 8.1.6. Platinum Level - Full Functional Correctness
  • 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
    • 8.3.1. Maintenance and Evolution of Existing Ada Software
    • 8.3.2. New Developments in SPARK
    • 8.3.3. Conversion of Existing SPARK Software to SPARK 2014
    • 8.3.4. Analysis of Frozen Ada Software

• A. Command Line Invocation
• B. Alternative Provers
  • Installed with SPARK Pro
  • Installed with SPARK Discovery
  • Installed with SPARK Community
  • Other Automatic or Manual Provers
    • Updating the Why3 Configuration File
    • Sharing Libraries of Theorems
  • Coq
• C. Project Attributes
• D. Implementation Defined Pragmas
  • Pragma SPARK_Mode
• 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
  • Tool Limitations
  • Legality Rules
  • Flow Analysis Limitations
  • Proof Limitations
• G. Portability Issues
  • Compiling with a non-SPARK Aware Compiler
  • Implementation-specific Decisions
    • Parenthesized Arithmetic Operations
    • Base Type of User-Defined Integer Types
    • Size of ‘Image and ‘Img attributes
• H. Semantics of Floating Point Operations
• I. SPARK Architecture, Quality Assurance and Maturity
  • Development Process and Quality Assurance
  • Structure of the SPARK Software
    • GNAT front-end
    • GNAT2Why
    • Why3
    • Alt-Ergo
    • Z3
    • CVC4
    • COLIBRI
• J. GNU Free Documentation License
  • PREAMBLE
  • APPLICABILITY AND DEFINITIONS
  • VERBATIM COPYING
  • COPYING IN QUANTITY
  • MODIFICATIONS
  • COMBINING DOCUMENTS
  • COLLECTIONS OF DOCUMENTS
  • AGGREGATION WITH INDEPENDENT WORKS
  • TRANSLATION
  • TERMINATION
  • FUTURE REVISIONS OF THIS LICENSE
  • ADDENDUM: How to use this License for your documents