SPARK Reference Manual
Copyright (C) 2013-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. Introduction
- 1.1. Structure of Introduction
- 1.2. How to Read and Interpret this Manual
- 1.3. Method of Description
- 1.4. Formal Analysis
- 1.5. Executable Contracts and Mathematical Numbers
- 1.6. Dynamic Semantics of SPARK Programs
- 1.7. Main Program
- 1.8. SPARK Strategic Requirements
- 1.9. Explaining the Strategic Requirements
- 2. Lexical Elements
- 3. Declarations and Types
- 4. Names and Expressions
- 5. Statements
- 6. Subprograms
- 6.1. Subprogram Declarations
- 6.1.1. Preconditions and Postconditions
- 6.1.2. Subprogram Contracts
- 6.1.3. Contract Cases
- 6.1.4. Global Aspects
- 6.1.5. Depends Aspects
- 6.1.6. Global and Depends Aspects of Dispatching Subprograms
- 6.1.7. Extensions_Visible Aspects
- 6.1.8. Subprogram_Variant Aspects
- 6.1.9. Exceptional Cases
- 6.1.10. Always_Terminates Aspects
- 6.1.11. Functions With Side Effects
- 6.2. Formal Parameter Modes
- 6.3. Subprogram Bodies
- 6.4. Subprogram Calls
- 6.5. Return Statements
- 6.6. Overloading of Operators
- 6.7. Null Procedures
- 6.8. Expression Functions
- 6.9. Ghost Entities
- 6.10. Relaxed Initialization
- 6.1. Subprogram Declarations
- 7. Packages
- 8. Visibility Rules
- 9. Tasks and Synchronization
- 10. Program Structure and Compilation Issues
- 11. Exceptions
- 12. Generic Units
- 13. Representation Issues
- 13.1. Operational and Representation Aspects
- 13.2. Packed Types
- 13.3. Operational and Representation Attributes
- 13.4. Enumeration Representation Clauses
- 13.5. Record Layout
- 13.6. Change of Representation
- 13.7. The Package System
- 13.8. Machine Code Insertions
- 13.9. Unchecked Type Conversions
- 13.10. Unchecked Access Value Creation
- 13.11. Storage Management
- 13.12. Pragma Restrictions and Pragma Profile
- 13.13. Streams
- 13.14. Freezing Rules
- 14. Predefined Language Environment (Annex A)
- 14.1. The Package Standard (A.1)
- 14.2. The Package Ada (A.2)
- 14.3. Character Handling (A.3)
- 14.3.1. The Packages Characters, Wide_Characters, and Wide_Wide_Characters (A.3.1)
- 14.3.2. The Package Characters.Handling (A.3.2)
- 14.3.3. The Package Characters.Latin_1 (A.3.3)
- 14.3.4. The Package Characters.Conversions (A.3.4)
- 14.3.5. The Package Wide_Characters.Handling (A.3.5)
- 14.3.6. The Package Wide_Wide_Characters.Handling (A.3.6)
- 14.4. String Handling (A.4)
- 14.4.1. The Package Strings (A.4.1)
- 14.4.2. The Package Strings.Maps (A.4.2)
- 14.4.3. Fixed-Length String Handling (A.4.3)
- 14.4.4. Bounded-Length String Handling (A.4.4)
- 14.4.5. Unbounded-Length String Handling (A.4.5)
- 14.4.6. String-Handling Sets and Mappings (A.4.6)
- 14.4.7. Wide_String Handling (A.4.7)
- 14.4.8. Wide_Wide_String Handling (A.4.8)
- 14.4.9. String Hashing (A.4.9)
- 14.4.10. String Comparison (A.4.10)
- 14.4.11. String Encoding (A.4.11)
- 14.5. The Numerics Packages (A.5)
- 14.6. Input-Output (A.6)
- 14.7. External Files and File Objects (A.7)
- 14.8. Sequential and Direct Files (A.8)
- 14.9. The Generic Package Storage_IO (A.9)
- 14.10. Text Input-Output (A.10)
- 14.10.1. The Package Text_IO (A.10.1)
- 14.10.2. Text File Management (A.10.2)
- 14.10.3. Default Input, Output and Error Files (A.10.3)
- 14.10.4. Specification of Line and Page Lengths (A.10.4)
- 14.10.5. Operations on Columns, Lines and Pages (A.10.5)
- 14.10.6. Get and Put Procedures (A.10.6)
- 14.10.7. Input-Output of Characters and Strings (A.10.7)
- 14.10.8. Input-Output for Integer Types (A.10.8)
- 14.10.9. Input-Output for Real Types (A.10.9)
- 14.10.10. Input-Output for Enumeration Types (A.10.10)
- 14.10.11. Input-Output for Bounded Strings (A.10.11)
- 14.10.12. Input-Output of Unbounded Strings (A.10.12)
- 14.11. Wide Text Input-Output and Wide Wide Text Input-Output (A.11)
- 14.12. Stream Input-Output (A.12)
- 14.13. Exceptions in Input-Output (A.13)
- 14.14. File Sharing (A.14)
- 14.15. The Package Command_Line (A.15)
- 14.16. The Package Directories (A.16)
- 14.17. The Package Environment_Variables (A.17)
- 14.18. Containers (A.18)
- 14.19. The Package Locales (A.19)
- 14.20. Interface to Other Languages (Annex B)
- 14.21. Systems Programming (Annex C)
- 14.22. Real-Time Systems (Annex D)
- 14.23. Distributed Systems (Annex E)
- 14.24. Information Systems (Annex F)
- 14.25. Numerics (Annex G)
- 14.26. High Integrity Systems (Annex H)
- 15. Language-Defined Aspects and Attributes (Annex K)
- 16. Language-Defined Pragmas (Annex L)
- 17. Glossary