Logo
  • About

Ada Courses

  • Introduction to Ada
    • Introduction
      • History
      • Ada today
      • Philosophy
      • SPARK
    • Imperative Language
      • Hello world
      • Imperative language - If/Then/Else
      • Imperative language - Loops
        • For loops
        • Bare loops
        • While loops
      • Imperative language - Case statement
      • Imperative language - Declarative regions
      • Imperative language - conditional expressions
        • If expressions
        • Case expressions
    • Subprograms
      • Subprograms
        • Subprogram calls
        • Nested subprograms
        • Function calls
      • Parameter modes
      • Subprogram calls
        • In parameters
        • In out parameters
        • Out parameters
        • Forward declaration of subprograms
      • Renaming
    • Modular Programming
      • Packages
      • Using a package
      • Package body
      • Child packages
        • Child of a child package
        • Multiple children
        • Visibility
      • Renaming
    • Strongly Typed Language
      • What is a type?
      • Integers
        • Operational semantics
      • Unsigned types
      • Enumerations
      • Floating-point types
        • Basic properties
        • Precision of floating-point types
        • Range of floating-point types
      • Strong typing
      • Derived types
      • Subtypes
        • Subtypes as type aliases
    • Records
      • Record type declaration
      • Aggregates
      • Component selection
      • Renaming
    • Arrays
      • Array type declaration
      • Indexing
      • Simpler array declarations
      • Range attribute
      • Unconstrained arrays
      • Predefined array type: String
      • Restrictions
      • Returning unconstrained arrays
      • Declaring arrays (2)
      • Array slices
      • Renaming
    • More About Types
      • Aggregates: A primer
      • Overloading and qualified expressions
      • Character types
    • Access Types
      • Overview
      • Allocation (by type)
      • Dereferencing
      • Other features
      • Mutually recursive types
    • More About Records
      • Dynamically sized record types
      • Records with discriminant
      • Variant records
    • Fixed-Point Types
      • Decimal fixed-point types
        • Decimal delta
        • Decimal digits
        • Decimal delta and digits
        • Requirements for the delta
      • Ordinary fixed-point types
      • Fixed-point vs. floating-point types
    • Privacy
      • Basic encapsulation
      • Abstract data types
      • Limited types
      • Child packages & privacy
    • Generics
      • Introduction
      • Formal type declaration
      • Formal object declaration
      • Generic body definition
      • Generic instantiation
      • Generic packages
      • Formal subprograms
      • Example: I/O instances
      • Example: ADTs
      • Example: Swap
      • Example: Reversing
      • Example: Test application
    • Exceptions
      • Exception declaration
      • Raising an exception
      • Handling an exception
      • Predefined exceptions
    • Tasking
      • Tasks
        • Simple task
        • Simple synchronization
        • Delay
        • Synchronization: rendezvous
        • Select loop
        • Cycling tasks
      • Protected objects
        • Simple object
        • Entries
      • Task and protected types
        • Task types
        • Protected types
    • Design by contracts
      • Pre- and postconditions
      • Predicates
      • Type invariants
    • Interfacing With C
      • Multi-language project
      • Type convention
      • Foreign subprograms
        • Calling C subprograms in Ada
        • Calling Ada subprograms in C
      • Foreign variables
        • Using C global variables in Ada
        • Using Ada variables in C
      • Generating bindings
        • Adapting bindings
    • Object Oriented Programming
      • Derived types
      • Tagged types
      • Classwide types
      • Dispatching operations
      • Dot notation
      • Private & Limited
      • Classwide access types
    • Standard Library: Containers
      • Vectors
        • Instantiation
        • Initialization
        • Appending and prepending elements
        • Accessing first and last elements
        • Iterating
        • Finding and changing elements
        • Inserting elements
        • Removing elements
        • Other Operations
      • Sets
        • Initialization and iteration
        • Operations on elements
        • Other Operations
      • Indefinite maps
        • Hashed maps
        • Ordered maps
        • Complexity
    • Standard Library: Dates & Times
      • Date and time handling
        • Delaying using date
      • Real-time
        • Benchmarking
    • Standard Library: Strings
      • String operations
      • Limitation of fixed-length strings
      • Bounded strings
      • Unbounded strings
    • Standard Library: Files & Streams
      • Text I/O
      • Sequential I/O
      • Direct I/O
      • Stream I/O
    • Standard Library: Numerics
      • Elementary Functions
      • Random Number Generation
      • Complex Types
      • Vector and Matrix Manipulation
    • Appendices
      • Appendix A: Generic Formal Types
        • Indefinite version
      • Appendix B: Containers
  • Advanced Journey With Ada
    • Data types
      • Types
        • Names
        • Objects
        • Scalar Types
        • Enumerations
        • Universal and Root Types
        • Definite and Indefinite Subtypes
        • Incomplete types
        • Type view
        • Type conversion
        • Qualified Expressions
        • Default initial values
        • Deferred Constants
        • User-defined literals
      • Types and Representation
        • Enumeration Representation Clauses
        • Data Representation
        • Sizes
        • Alignment
        • Overlapping Storage
        • Packed Representation
        • Record Representation and storage clauses
        • Changing Data Representation
        • Valid Attribute
        • Unchecked Union
        • Addresses
        • Discarding names
      • Shared variable control
        • Volatile
        • Independent
        • Atomic
        • Full-access only
        • Atomic operations
      • Records
        • Default Initialization
        • Mutually dependent types
        • Null records
        • Record discriminants
        • Discriminant constraints and operations
        • Unknown discriminants
        • Unconstrained subtypes
        • Variant parts
        • Per-Object Expressions
      • Aggregates
        • Container Aggregates
        • Record aggregates
        • Full coverage rules for Aggregates
        • Array aggregates
        • Extension Aggregates
        • Delta Aggregates
      • Arrays
        • Array constraints
        • Multidimensional Arrays
        • Derived array types and array subtypes
      • Strings
        • Character and String Literals
        • Wide and Wide-Wide Strings
        • String Encoding
        • UTF-8 applications
        • Image attribute
        • Put_Image aspect
        • Universal text buffer
      • Numerics
        • Numeric Literals
        • Universal Numeric Types
        • Base types
        • Discrete and Real Numeric Types
        • Integer types
        • Modular Types
        • Floating-point types
        • Big Numbers
      • Numeric Attributes
        • Attributes of Modular Types
        • Attributes of Floating-Point Types
        • Attributes of Fixed-Point types
    • Control Flow
      • Expressions
        • Expressions: Definition
        • Conditional Expressions
        • Quantified Expressions
        • Declare Expressions
        • Reduction Expressions
      • Statements
        • Simple and Compound Statements
        • Labels
        • Exit loop statement
        • If, case and loop statements
        • Block Statements
        • Extended return statement
      • Subprograms
        • Parameter Modes and Associations
        • Operators
        • Expression functions
        • Overloading
        • Operator Overloading
        • Operator Overriding
        • Nonreturning procedures
        • Inline subprograms
        • Null Procedures
      • Exceptions
        • Classification of Errors
        • Asserts
        • Assertion policies
        • Checks and exceptions
        • Ada.Exceptions package
        • Exception renaming
        • Out and Uninitialized
        • Suppressing checks
    • Modular programming
      • Packages
        • Package renaming
        • Private packages
        • Private with clauses
        • Limited Visibility
        • Visibility
        • Use type clause
        • Use clauses and naming conflicts
      • Subprograms and Modularity
        • Private subprograms
    • Resource Management
      • Access Types
        • Access types: Terminology
        • Access types: Allocation
        • Discriminants as Access Values
        • Parameters as Access Values
        • Self-reference
        • Mutually dependent types using access types
        • Dereferencing
        • Ragged arrays
        • Aliasing
        • Accessibility Levels and Rules: An Introduction
        • Unchecked Access
        • Unchecked Deallocation
        • Null & Not Null Access
        • Design strategies for access types
        • Access to subprograms
        • Accessibility Rules and Access-To-Subprograms
        • Access and Address
      • Anonymous Access Types
        • Named and Anonymous Access Types
        • Anonymous Access-To-Object Types
        • Access discriminants
        • Self-reference
        • Mutually dependent types using anonymous access types
        • Access parameters
        • User-Defined References
        • Anonymous Access Types and Accessibility Rules
        • Anonymous Access-To-Subprograms
        • Accessibility Rules and Anonymous Access-To-Subprograms
      • Limited Types
        • Assignment and equality
        • Limited private types
        • Explicitly limited types
        • Subtypes of Limited Types
        • Deriving from limited types
        • Immutably Limited Types
        • Limited Types with Discriminants
        • Record components of limited type
        • Limited types and aggregates
        • Constructor functions for limited types
        • Return objects
        • Building objects from constructors
        • Limited types as parameter
      • Controlled Types
        • Overview
        • Initialization
        • Assignment
        • Finalization
        • Controlled Types and Exception Handling
        • Applications of Controlled Types
  • Ada In Practice
    • Introduction
      • Assumptions
      • Definitions
        • Suppliers and Clients
        • Compile-time Visibility
        • Views
        • Partial and Full Views
    • Essential Design Idioms for Packages
      • Motivation
      • Implementation(s)
        • Named Collection of Declarations
        • Groups of Related Program Units
      • Notes
    • Abstract Data Types
      • Motivation
      • Implementation(s)
      • Pros
      • Cons
      • Relationship With Other Idioms
      • Notes
    • Abstract Data Machines
      • Motivation
      • Implementation(s)
      • Pros
      • Cons
    • Programming by Extension
      • Motivation
      • Implementation(s)
      • Pros
      • Cons
      • Relationship With Other Idioms
      • Notes
    • Constructor Functions For Abstract Data Types
      • Motivation
      • Implementation(s)
      • Pros
      • Cons
      • Relationship With Other Idioms
      • Notes
    • Controlling Object Initialization and Creation
      • Motivation
      • Implementation(s)
        • Compile-Time Legality
        • Run-Time Checks
        • Preventing Object Creation by Clients
      • Pros
      • Cons
      • Relationship With Other Idioms
      • Notes
    • Type Punning
      • Motivation
      • Implementation(s)
        • Overlays
        • Unchecked Conversions on Address Values
      • Pros
      • Cons
      • Relationship With Other Idioms
      • Notes
    • Expressing Inheritance Idioms
      • Motivation
        • Building Blocks
      • Implementation(s)
        • Subtype Inheritance
        • Implementation Inheritance
      • Pros
      • Cons
      • Relationship With Other Idioms
    • Providing Component Access to Enclosing Record Objects
      • Motivation
      • Implementation(s)
      • Real-World Example
      • Pros
      • Cons
      • Relationship With Other Idioms
      • Notes
      • Full Source Code for Selected Units
    • Interrupt Handling
      • Motivation
      • Implementation(s)
        • First Level Handler Alone
        • Task Notification Introduction
        • Task Notification With Communication
        • Task Notification Without Communication
      • Pros
      • Cons
      • Relationship With Other Idioms
      • What About Priorities?
      • Notes
    • Reducing Object Code from Generic Package Instantiations
      • Motivation
      • Implementation(s)
      • Pros
      • Cons
      • Relationship With Other Idioms
      • Notes
    • Resource Acquisition Is Initialization (RAII)
      • Motivation
      • Implementation
      • Pros
      • Cons
      • Relationship With Other Idioms
      • Notes
    • Using Streams for API Flexibility
      • Motivation
      • Implementation
      • Pros
      • Cons
      • Relationship With Other Idioms
      • Notes
    • Dealing with Silent Task Termination
      • Motivation
      • Solution
      • Pros
      • Cons
      • Relationship With Other Idioms
      • Notes
  • Ada for the C++ or Java Developer
    • Preface
    • Basics
    • Compilation Unit Structure
    • Statements, Declarations, and Control Structures
      • Statements and Declarations
      • Conditions
      • Loops
    • Type System
      • Strong Typing
      • Language-Defined Types
      • Application-Defined Types
      • Type Ranges
      • Generalized Type Contracts: Subtype Predicates
      • Attributes
      • Arrays and Strings
      • Heterogeneous Data Structures
      • Pointers
    • Functions and Procedures
      • General Form
      • Overloading
      • Subprogram Contracts
    • Packages
      • Declaration Protection
      • Hierarchical Packages
      • Using Entities from Packages
    • Classes and Object Oriented Programming
      • Primitive Subprograms
      • Derivation and Dynamic Dispatch
      • Constructors and Destructors
      • Encapsulation
      • Abstract Types and Interfaces
      • Invariants
    • Generics
      • Generic Subprograms
      • Generic Packages
      • Generic Parameters
    • Exceptions
      • Standard Exceptions
      • Custom Exceptions
    • Concurrency
      • Tasks
      • Rendezvous
      • Selective Rendezvous
      • Protected Objects
    • Low Level Programming
      • Representation Clauses
      • Embedded Assembly Code
      • Interfacing with C
    • Conclusion
    • References

SPARK Courses

  • Introduction to SPARK
    • Overview
      • What is it?
      • What do the tools do?
      • Key Tools
      • A trivial example
      • The Programming Language
      • Limitations
        • No side-effects in expressions
        • No aliasing of names
      • Designating SPARK Code
      • Code Examples / Pitfalls
        • Example #1
        • Example #2
        • Example #3
        • Example #4
        • Example #5
        • Example #6
        • Example #7
        • Example #8
        • Example #9
        • Example #10
    • Flow Analysis
      • What does flow analysis do?
      • Errors Detected
        • Uninitialized Variables
        • Ineffective Statements
        • Incorrect Parameter Mode
      • Additional Verifications
        • Global Contracts
        • Depends Contracts
      • Shortcomings
        • Modularity
        • Composite Types
        • Value Dependency
        • Contract Computation
      • Code Examples / Pitfalls
        • Example #1
        • Example #2
        • Example #3
        • Example #4
        • Example #5
        • Example #6
        • Example #7
        • Example #8
        • Example #9
        • Example #10
    • Proof of Program Integrity
      • Runtime Errors
      • Modularity
        • Exceptions
      • Contracts
        • Executable Semantics
        • Additional Assertions and Contracts
      • Debugging Failed Proof Attempts
        • Debugging Errors in Code or Specification
        • Debugging Cases where more Information is Required
        • Debugging Prover Limitations
      • Code Examples / Pitfalls
        • Example #1
        • Example #2
        • Example #3
        • Example #4
        • Example #5
        • Example #6
        • Example #7
        • Example #8
        • Example #9
        • Example #10
    • State Abstraction
      • What's an Abstraction?
      • Why is Abstraction Useful?
      • Abstraction of a Package's State
      • Declaring a State Abstraction
      • Refining an Abstract State
      • Representing Private Variables
      • Additional State
        • Nested Packages
        • Constants that Depend on Variables
      • Subprogram Contracts
        • Global and Depends
        • Preconditions and Postconditions
      • Initialization of Local Variables
      • Code Examples / Pitfalls
        • Example #1
        • Example #2
        • Example #3
        • Example #4
        • Example #5
        • Example #6
        • Example #7
        • Example #8
        • Example #9
        • Example #10
    • Proof of Functional Correctness
      • Beyond Program Integrity
      • Advanced Contracts
        • Ghost Code
        • Ghost Functions
        • Global Ghost Variables
      • Guide Proof
        • Local Ghost Variables
        • Ghost Procedures
        • Handling of Loops
        • Loop Invariants
      • Code Examples / Pitfalls
        • Example #1
        • Example #2
        • Example #3
        • Example #4
        • Example #5
        • Example #6
        • Example #7
        • Example #8
        • Example #9
        • Example #10
  • SPARK Ada for the MISRA C Developer
    • Preface
    • Enforcing Basic Program Consistency
      • Taming Text-Based Inclusion
      • Hardening Link-Time Checking
      • Going Towards Encapsulation
    • Enforcing Basic Syntactic Guarantees
      • Distinguishing Code and Comments
      • Specially Handling Function Parameters and Result
        • Handling the Result of Function Calls
        • Handling Function Parameters
      • Ensuring Control Structures Are Not Abused
        • Preventing the Semicolon Mistake
        • Avoiding Complex Switch Statements
        • Avoiding Complex Loops
        • Avoiding the Dangling Else Issue
    • Enforcing Strong Typing
      • Enforcing Strong Typing for Pointers
        • Pointers Are Not Addresses
        • Pointers Are Not References
        • Pointers Are Not Arrays
        • Pointers Should Be Typed
      • Enforcing Strong Typing for Scalars
        • Restricting Operations on Types
        • Restricting Explicit Conversions
        • Restricting Implicit Conversions
    • Initializing Data Before Use
      • Detecting Reads of Uninitialized Data
      • Detecting Partial or Redundant Initialization of Arrays and Structures
    • Controlling Side Effects
      • Preventing Undefined Behavior
      • Reducing Programmer Confusion
      • Side Effects and SPARK
    • Detecting Undefined Behavior
      • Preventing Undefined Behavior in SPARK
      • Proof of Absence of Run-Time Errors in SPARK
    • Detecting Unreachable Code and Dead Code
    • Conclusion
    • References
      • About MISRA C
      • About SPARK
      • About MISRA C and SPARK

Ada for Embedded Courses

  • Introduction to Embedded Systems Programming
    • Introduction
      • So, what will we actually cover?
      • Definitions
      • Down To The Bare Metal
      • The Ada Drivers Library
    • Low Level Programming
      • Separation Principle
      • Guaranteed Level of Support
      • Querying Implementation Limits and Characteristics
      • Querying Representation Choices
      • Specifying Representation
      • Unchecked Programming
      • Data Validity
    • Multi-Language Development
      • General Interfacing
        • Aspect/Pragma Convention
        • Aspect/Pragma Import and Export
        • Aspect/Pragma External_Name and Link_Name
        • Package Interfaces
      • Language-Specific Interfacing
        • Package Interfaces.C
        • Package Interfaces.C.Strings
        • Package Interfaces.C.Pointers
        • Package Interfaces.Fortran
        • Machine Code Insertions (MCI)
      • When Ada Is Not the Main Language
    • Interacting with Devices
      • Non-Memory-Mapped Devices
      • Memory-Mapped Devices
      • Dynamic Address Conversion
      • Address Arithmetic
    • General-Purpose Code Generators
      • Aspect Independent
      • Aspect Volatile
      • Aspect Atomic
      • Aspect Full_Access_Only
    • Handling Interrupts
      • Background
      • Language-Defined Interrupt Model
      • Interrupt Handlers
      • Interrupt Management
      • Associating Handlers With Interrupts
      • Interrupt Priorities
      • Common Design Idioms
        • Parameterizing Handlers
        • Multi-Level Handlers
      • Final Points
    • Conclusion
  • Ada for the Embedded C Developer
    • Introduction
      • So, what is this Ada thing anyway?
      • Ada — The Technical Details
    • The C Developer's Perspective
      • What we mean by Embedded Software
      • The GNAT Toolchain
      • The GNAT Toolchain for Embedded Targets
      • Hello World in Ada
      • The Ada Syntax
      • Compilation Unit Structure
      • Packages
        • Declaration Protection
        • Hierarchical Packages
        • Using Entities from Packages
      • Statements and Declarations
      • Conditions
      • Loops
      • Type System
        • Strong Typing
        • Language-Defined Types
        • Application-Defined Types
        • Type Ranges
        • Unsigned And Modular Types
        • Attributes
        • Arrays and Strings
        • Heterogeneous Data Structures
        • Pointers
      • Functions and Procedures
        • General Form
        • Overloading
        • Aspects
    • Concurrency and Real-Time
      • Understanding the various options
      • Tasks
      • Rendezvous
      • Selective Rendezvous
      • Protected Objects
      • Ravenscar
    • Writing Ada on Embedded Systems
      • Understanding the Ada Run-Time
      • Low Level Programming
        • Representation Clauses
        • Embedded Assembly Code
      • Interrupt Handling
      • Dealing with Absence of FPU with Fixed Point
      • Volatile and Atomic data
        • Volatile
        • Atomic
      • Interfacing with Devices
        • Size aspect and attribute
        • Register overlays
        • Data streams
      • ARM and svd2ada
    • Enhancing Verification with SPARK and Ada
      • Understanding Exceptions and Dynamic Checks
      • Understanding Dynamic Checks versus Formal Proof
      • Initialization and Correct Data Flow
      • Contract-Based Programming
      • Replacing Defensive Code
      • Proving Absence of Run-Time Errors
      • Proving Abstract Properties
      • Final Comments
    • C to Ada Translation Patterns
      • Naming conventions and casing considerations
      • Manually interfacing C and Ada
      • Building and Debugging mixed language code
      • Automatic interfacing
      • Using Arrays in C interfaces
      • By-value vs. by-reference types
      • Naming and prefixes
      • Pointers
      • Bitwise Operations
      • Mapping Structures to Bit-Fields
        • Overlays vs. Unchecked Conversions
    • Handling Variability and Re-usability
      • Understanding static and dynamic variability
      • Handling variability & reusability statically
        • Genericity
        • Simple derivation
        • Configuration pragma files
        • Configuration packages
      • Handling variability & reusability dynamically
        • Records with discriminants
        • Variant records
        • Object orientation
        • Pointer to subprograms
      • Design by components using dynamic libraries
    • Performance Considerations
      • Overall expectations
      • Switches and optimizations
        • Optimizations levels
        • Inlining
      • Checks and assertions
        • Checks
        • Assertions
      • Dynamic vs. static structures
      • Pointers vs. data copies
        • Function returns
    • Argumentation and Business Perspectives
      • What's the expected ROI of a C to Ada transition?
      • Who is using Ada today?
      • What is the future of the Ada technology?
      • Is the Ada toolset complete?
      • Where can I find Ada or SPARK developers?
      • How to introduce Ada and SPARK in an existing code base?
    • Conclusion
    • Hands-On: Object-Oriented Programming
      • System Overview
      • Non Object-Oriented Approach
        • Starting point in C
        • Initial translation to Ada
        • Improved Ada implementation
      • First Object-Oriented Approach
        • Interfaces
        • Base type
        • Derived types
        • Subprograms from parent
        • Type AB
        • Updated source-code
      • Further Improvements
        • Dispatching calls
        • Dynamic allocation
        • Limited controlled types
        • Updated source-code

Ada/SPARK: General Material

  • Guidelines for Safe and Secure Ada/SPARK
    • Introduction
      • Scope
      • Structure
      • Enforcement
      • About the Rules
        • Mapping to Other Standards
    • Definitions
      • Level
      • Remediation
    • Dynamic Storage Management
      • Common High Integrity Restrictions (DYN01)
        • Reference
        • Description
        • Applicable Vulnerability within ISO TR 24772-2
        • Applicable Common Weakness Enumeration
        • Noncompliant Code Example
        • Compliant Code Example
        • Notes
      • Traditional Static Allocation Policy (DYN02)
        • Reference
        • Description
        • Applicable Vulnerability within ISO TR 24772-2
        • Applicable Common Weakness Enumeration
        • Noncompliant Code Example
        • Compliant Code Example
        • Notes
      • Access Types Without Allocators Policy (DYN03)
        • Reference
        • Description
        • Applicable Vulnerability within ISO TR 24772-2
        • Applicable Common Weakness Enumeration
        • Noncompliant Code Example
        • Compliant Code Example
        • Notes
      • Minimal Dynamic Allocation Policy (DYN04)
        • Reference
        • Description
        • Applicable Vulnerability within ISO TR 24772-2
        • Applicable Common Weakness Enumeration
        • Noncompliant Code Example
        • Compliant Code Example
        • Notes
      • User-Defined Storage Pools Policy (DYN05)
        • Reference
        • Description
        • Applicable Vulnerability within ISO TR 24772-2
        • Applicable Common Weakness Enumeration
        • Noncompliant Code Example
        • Compliant Code Example
        • Notes
      • Statically Determine Maximum Stack Requirements (DYN06)
        • Reference
        • Description
        • Applicable Vulnerability within ISO TR 24772-2
        • Applicable Common Weakness Enumeration
        • Noncompliant Code Example
        • Compliant Code Example
        • Notes
    • Safe Reclamation
      • No Multiple Reclamations (RCL01)
        • Reference
        • Description
        • Applicable Vulnerability within ISO TR 24772-2
        • Applicable Common Weakness Enumeration
        • Noncompliant Code Example
        • Compliant Code Example
        • Notes
      • Only Reclaim Allocated Storage (RCL02)
        • Reference
        • Description
        • Applicable Vulnerability within ISO TR 24772-2
        • Applicable Common Weakness Enumeration
        • Noncompliant Code Example
        • Compliant Code Example
        • Notes
      • Only Reclaim To The Same Pool (RCL03)
        • Reference
        • Description
        • Applicable Vulnerability within ISO TR 24772-2
        • Applicable Common Weakness Enumeration
        • Noncompliant Code Example
        • Compliant Code Example
        • Notes
    • Concurrency
      • Use the Ravenscar Profile (CON01)
        • Reference
        • Description
        • Applicable Vulnerability within ISO TR 24772-2
        • Applicable Common Weakness Enumeration
        • Noncompliant Code Example
        • Compliant Code Example
        • Notes
      • Use the Jorvik Profile (CON02)
        • Reference
        • Description
        • Applicable Vulnerability within ISO TR 24772-2
        • Applicable Common Weakness Enumeration
        • Noncompliant Code Example
        • Compliant Code Example
        • Notes
      • Avoid Shared Variables for Inter-task Communication (CON03)
        • Reference
        • Description
        • Applicable Vulnerability within ISO TR 24772-2
        • Applicable Common Weakness Enumeration
        • Noncompliant Code Example
        • Compliant Code Example
        • Notes
    • Robust Programming Practice
      • No Use of "others" in Case Constructs (RPP01)
        • Reference
        • Description
        • Applicable Vulnerability within ISO TR 24772-2
        • Applicable Common Weakness Enumeration
        • Noncompliant Code Example
        • Compliant Code Example
        • Notes
      • No Enumeration Ranges in Case Constructs (RPP02)
        • Reference
        • Description
        • Applicable Vulnerability within ISO TR 24772-2
        • Applicable Common Weakness Enumeration
        • Noncompliant Code Example
        • Compliant Code Example
        • Notes
      • Limited Use of "others" In Aggregates (RPP03)
        • Reference
        • Description
        • Applicable Vulnerability within ISO TR 24772-2
        • Applicable Common Weakness Enumeration
        • Noncompliant Code Example
        • Compliant Code Example
        • Notes
      • No Unassigned Mode-Out Procedure Parameters (RPP04)
        • Reference
        • Description
        • Applicable Vulnerability within ISO TR 24772-2
        • Applicable Common Weakness Enumeration
        • Noncompliant Code Example
        • Compliant Code Example
        • Notes
      • No Use of "others" in Exception Handlers (RPP05)
        • Reference
        • Description
        • Applicable Vulnerability within ISO TR 24772-2
        • Applicable Common Weakness Enumeration
        • Noncompliant Code Example
        • Compliant Code Example
        • Notes
      • Avoid Function Side-Effects (RPP06)
        • Reference
        • Description
        • Applicable Vulnerability within ISO TR 24772-2
        • Applicable Common Weakness Enumeration
        • Noncompliant Code Example
        • Compliant Code Example
        • Notes
      • Functions Only Have Mode "in" (RPP07)
        • Reference
        • Description
        • Applicable Vulnerability within ISO TR 24772-2
        • Applicable Common Weakness Enumeration
        • Noncompliant Code Example
        • Compliant Code Example
        • Notes
      • Limit Parameter Aliasing (RPP08)
        • Reference
        • Description
        • Applicable Vulnerability within ISO TR 24772-2
        • Applicable Common Weakness Enumeration
        • Noncompliant Code Example
        • Compliant Code Example
        • Notes
      • Use Precondition and Postcondition Contracts (RPP09)
        • Reference
        • Description
        • Applicable Vulnerability within ISO TR 24772-2
        • Applicable Common Weakness Enumeration
        • Noncompliant Code Example
        • Compliant Code Example
        • Notes
      • Do Not Re-Verify Preconditions In Subprogram Bodies (RPP10)
        • Reference
        • Description
        • Applicable Vulnerability within ISO TR 24772-2
        • Applicable Common Weakness Enumeration
        • Noncompliant Code Example
        • Compliant Code Example
        • Notes
      • Always Use the Result of Function Calls (RPP11)
        • Reference
        • Description
        • Applicable Vulnerability within ISO TR 24772-2
        • Applicable Common Weakness Enumeration
        • Noncompliant Code Example
        • Compliant Code Example
        • Notes
      • No Recursion (RPP12)
        • Reference
        • Description
        • Applicable Vulnerability within ISO TR 24772-2
        • Applicable Common Weakness Enumeration
        • Noncompliant Code Example
        • Compliant Code Example
        • Notes
      • No Reuse of Standard Typemarks (RPP13)
        • Reference
        • Description
        • Applicable Vulnerability within ISO TR 24772-2
        • Applicable Common Weakness Enumeration
        • Noncompliant Code Example
        • Compliant Code Example
        • Notes
      • Use Symbolic Constants For Literal Values (RPP14)
        • Reference
        • Description
        • Applicable Vulnerability within ISO TR 24772-2
        • Applicable Common Weakness Enumeration
        • Noncompliant Code Example
        • Compliant Code Example
        • Notes
    • Exception Usage
      • Do Not Raise Language-Defined Exceptions (EXU01)
        • Reference
        • Description
        • Applicable Vulnerability within ISO TR 24772-2
        • Applicable Common Weakness Enumeration
        • Noncompliant Code Example
        • Compliant Code Example
        • Notes
      • No Unhandled Application-Defined Exceptions (EXU02)
        • Reference
        • Description
        • Applicable Vulnerability within ISO TR 24772-2
        • Applicable Common Weakness Enumeration
        • Noncompliant Code Example
        • Compliant Code Example
        • Notes
      • No Exception Propagation Beyond Name Visibility (EXU03)
        • Reference
        • Description
        • Applicable Vulnerability within ISO TR 24772-2
        • Applicable Common Weakness Enumeration
        • Noncompliant Code Example
        • Compliant Code Example
        • Notes
      • Prove Absence of Run-time Exceptions (EXU04)
        • Reference
        • Description
        • Applicable Vulnerability within ISO TR 24772-2
        • Applicable Common Weakness Enumeration
        • Noncompliant Code Example
        • Compliant Code Example
        • Notes
    • Object-Oriented Programming
      • No Class-wide Constructs Policy (OOP01)
        • Reference
        • Description
        • Applicable Vulnerability within ISO TR 24772-2
        • Applicable Common Weakness Enumeration
        • Noncompliant Code Example
        • Compliant Code Example
        • Notes
      • Static Dispatching Only Policy (OOP02)
        • Reference
        • Description
        • Applicable Vulnerability within ISO TR 24772-2
        • Applicable Common Weakness Enumeration
        • Noncompliant Code Example
        • Compliant Code Example
        • Notes
      • Limit Inheritance Hierarchy Depth (OOP03)
        • Reference
        • Description
        • Applicable Vulnerability within ISO TR 24772-2
        • Applicable Common Weakness Enumeration
        • Noncompliant Code Example
        • Compliant Code Example
        • Notes
      • Limit Statically-Dispatched Calls To Primitive Operations (OOP04)
        • Reference
        • Description
        • Applicable Vulnerability within ISO TR 24772-2
        • Applicable Common Weakness Enumeration
        • Noncompliant Code Example
        • Compliant Code Example
        • Notes
      • Use Explicit Overriding Annotations (OOP05)
        • Reference
        • Description
        • Applicable Vulnerability within ISO TR 24772-2
        • Applicable Common Weakness Enumeration
        • Noncompliant Code Example
        • Compliant Code Example
        • Notes
      • Use Class-wide Pre/Post Contracts (OOP06)
        • Reference
        • Description
        • Applicable Vulnerability within ISO TR 24772-2
        • Applicable Common Weakness Enumeration
        • Noncompliant Code Example
        • Compliant Code Example
        • Notes
      • Ensure Local Type Consistency (OOP07)
        • Reference
        • Description
        • Applicable Vulnerability within ISO TR 24772-2
        • Applicable Common Weakness Enumeration
        • Noncompliant Code Example
        • Compliant Code Example
        • Notes
    • Software Engineering
      • Use SPARK Extensively (SWE01)
        • Reference
        • Description
        • Applicable Vulnerability within ISO TR 24772-2
        • Applicable Common Weakness Enumeration
        • Noncompliant Code Example
        • Compliant Code Example
        • Notes
      • Enable Optional Warnings and Treat As Errors (SWE02)
        • Reference
        • Description
        • Applicable Vulnerability within ISO TR 24772-2
        • Applicable Common Weakness Enumeration
        • Noncompliant Code Example
        • Compliant Code Example
        • Notes
      • Use A Static Analysis Tool Extensively (SWE03)
        • Reference
        • Description
        • Applicable Vulnerability within ISO TR 24772-2
        • Applicable Common Weakness Enumeration
        • Noncompliant Code Example
        • Compliant Code Example
        • Notes
      • Hide Implementation Artifacts (SWE04)
        • Reference
        • Description
        • Applicable Vulnerability within ISO TR 24772-2
        • Applicable Common Weakness Enumeration
        • Noncompliant Code Example
        • Compliant Code Example
        • Notes
    • References
  • What's New in Ada 2022
    • Introduction
      • References
    • 'Image attribute for any type
      • 'Image attribute for a value
      • 'Image attribute for any type
      • References
    • Redefining the 'Image attribute
      • What's the Root_Buffer_Type?
      • Outdated draft implementation
      • References
    • User-Defined Literals
      • Turn Ada into JavaScript
      • References
    • Advanced Array Aggregates
      • Square brackets
      • Iterated Component Association
      • References
    • Container Aggregates
      • References
    • Delta Aggregates
      • Delta aggregate for records
      • Delta aggregate for arrays
      • References
    • Target Name Symbol (@)
      • Alternatives
      • References
    • Enumeration representation
      • Literal positions
      • Representation values
      • Before Ada 2022
      • References
    • Big Numbers
      • Big Integers
      • Tiny RSA implementation
      • Big Reals
      • References
    • Interfacing C variadic functions
      • References
  • Introduction to the GNAT Toolchain
    • GNAT Toolchain Basics
      • Basic commands
      • Compiler warnings
        • -gnatwa switch and warning suppression
        • Style checking
    • GPRbuild
      • Basic commands
      • Project files
        • Basic structure
        • Customization
      • Project dependencies
        • Simple dependency
        • Dependencies to dynamic libraries
      • Configuration pragma files
      • Configuration packages
    • GNAT Studio
      • Start-up
        • Windows
        • Linux
      • Creating projects
      • Building
      • Debugging
        • Debug information
        • Improving main application
        • Debugging the application
      • Formal verification
    • GNAT Tools
      • gnatchop
      • gnatprep
      • gnatmem
      • gnatdoc
      • gnatpp
      • gnatstub

Upcoming Courses

  • Advanced Journey With Ada (UNPUBLISHED)
    • Resource Management
      • Memory Management
        • Maximum allocation size and alignment
        • Storage elements
        • Memory pools
        • Memory subpools
        • Secondary stack
      • Containers
        • Aggregate aspect
        • User-Defined Iterator Types
      • Standard Containers
        • Linked lists
        • Trees
        • Queue containers
        • Indefinite containers
        • Holder container
      • Restrictions and Profiles
        • Pragmas
        • Language-Defined Restrictions and Profiles
    • Abstraction-oriented programming
      • Strong typing
        • Type-based security
        • Example: Table access
        • Example: Multiple indices
        • Discriminants
      • Object-Oriented Programming
        • Primitives
        • Overriding indicators
        • Abstract types and subprograms
        • Interfaces
        • Example: Extending Interfaces
        • Calling inherited subprograms
        • Dynamic Polymorphism
        • Controlled types
        • Ada.Tags package
        • User-defined indexing
      • Generics
        • Mapping of Definite and Indefinite Subtypes
        • Formal incomplete types
        • Formal packages
        • Formal objects
        • Formal definite and indefinite types
        • Formal incomplete type
        • Default subtype mark
        • Formal private and derived types
        • Formal interfaces
        • Formal numeric types
        • Generic Renaming
    • Design by contract
      • Contracts
        • Class-wide contracts
        • Default initial conditions
        • Entry index attribute
        • Global Aspect Definition
        • Predicate failure
        • Stable Properties of a Type
    • Initialization
      • Freezing
        • Freezing rules
      • Package Elaboration
        • Preelaboration
        • Elaboration control
        • Pure program and library units
      • Elaboration Of Generics
        • Elaboration check
    • Multithreading
      • Tasking
        • Statements
        • Task IDs and attributes
        • Task termination
        • Tasking and exceptions
        • Task and synchronized interfaces
        • Protected Subprograms and Protected Actions
    • Interfacing with the external world
      • File I/O
        • Efficient Stream I/O for Array Types
        • Container streaming
      • Interfacing with C and C++
        • Interfacing with C
        • Interfacing with C++
    • Appendices
      • Legacy features
        • Nested packages
        • separate compilation
  • Advanced SPARK
    • Subprogram Contracts
      • Subprogram Contracts in Ada 2012 and SPARK 2014
      • Dynamic Execution of Subprogram Contracts
      • Dynamic Behavior when Subprogram Contracts Fail
      • Precondition
      • Postcondition
      • Contract Cases
      • Attribute 'Old
      • Implication and Equivalence
      • Reasoning by Cases
      • Universal and Existential Quantification
      • Expression Functions
      • Code Examples / Pitfalls
        • Example #1
        • Example #2
        • Example #3
        • Example #4
        • Example #5
        • Example #6
        • Example #7
        • Example #8
        • Example #9
        • Example #10
    • Type Contracts
      • Type Contracts in Ada 2012 and SPARK 2014
      • Static and Dynamic Predicates
        • Static Predicate
        • Dynamic Predicate
        • Restrictions on Types With Dynamic Predicate
        • Dynamic Checking of Predicates
        • Temporary Violations of the Dynamic Predicate
      • Type Invariant
        • Dynamic Checking of Type Invariants
      • Inheritance of Predicates and Type Invariants
      • Other Useful Gotchas on Predicates and Type Invariants
      • Default Initial Condition
      • Code Examples / Pitfalls
        • Example #1
        • Example #2
        • Example #3
        • Example #4
        • Example #5
        • Example #6
        • Example #7
        • Example #8
        • Example #9
        • Example #10
    • Systems Programming
      • Type Contracts in Ada 2012 and SPARK 2014
      • Systems Programming – What is it?
      • Systems Programming – How can SPARK help?
      • Systems Programming – A trivial example
      • Volatile Variables and Volatile Types
      • Flavors of Volatile Variables
        • Using Async_Readers / Async_Writers
        • Using Effective_Reads / Effective_Writes
        • Combinations of Flavors of Volatile Variables
      • Constraints on Volatile Variables
      • Constraints on Volatile Functions
      • State Abstraction on Volatile Variables
      • Constraints on Address Attribute
      • Can something be known of volatile variables?
      • Other Concerns in Systems Programming
      • Code Examples / Pitfalls
        • Example #1
        • Example #2
        • Example #3
        • Example #4
        • Example #5
        • Example #6
        • Example #7
        • Example #8
        • Example #9
        • Example #10
    • Concurrency
      • Concurrency ≠ Parallelism
      • Concurrent Program Structure in Ada
      • The problems with concurrency
      • Ravenscar – the Ada solution to concurrency problems
      • Concurrent Program Structure in Ravenscar
      • Ravenscar – the SPARK solution to concurrency problems
      • Concurrency – A trivial example
      • Setup for using concurrency in SPARK
      • Tasks in Ravenscar
      • Communication Between Tasks in Ravenscar
      • Protected Objects in Ravenscar
      • Protected Communication with Procedures & Functions
      • Blocking Communication with Entries
      • Relaxed Constraints on Entries with Extended Ravenscar
      • Interrupt Handlers in Ravenscar
      • Other Communications Between Tasks in SPARK
      • Data and Flow Dependencies of Tasks
      • State Abstraction over Synchronized Variables
      • Synchronized Abstract State in the Standard Library
      • Code Examples / Pitfalls
        • Example #1
        • Example #2
        • Example #3
        • Example #4
        • Example #5
        • Example #6
        • Example #7
        • Example #8
        • Example #9
        • Example #10
    • Object-oriented Programming
      • What is Object Oriented Programming?
      • Prototypes and Scopes in SPARK
      • Classes in SPARK
      • Methods in SPARK
      • Dynamic dispatching in SPARK
        • A trivial example
        • The problems with dynamic dispatching
      • LSP – the SPARK solution to dynamic dispatching problems
        • Verification of dynamic dispatching calls
        • Class-wide contracts and data abstraction
        • Class-wide contracts, data abstraction and overriding
      • Dynamic semantics of class-wide contracts
      • Redispatching and Extensions_Visible aspect
      • Code Examples / Pitfalls
        • Example #1
        • Example #2
        • Example #3
        • Example #4
        • Example #5
        • Example #6
        • Example #7
        • Example #8
        • Example #9
        • Example #10
    • Ghost code
      • What is ghost code?
      • Ghost code – A trivial example
      • Ghost variables – aka auxiliary variables
      • Ghost variables – non-interference rules
      • Ghost statements
      • Ghost procedures
      • Ghost functions
      • Imported ghost functions
      • Ghost packages and ghost abstract state
      • Executing ghost code
      • Examples of use
        • Encoding a state automaton
        • Expressing useful lemmas
        • Specifying an API through a model
      • Extreme proving with ghost code – red black trees in SPARK
      • Positioning ghost code in proof techniques
      • Code Examples / Pitfalls
        • Example #1
        • Example #2
        • Example #3
        • Example #4
        • Example #5
        • Example #6
        • Example #7
        • Example #8
        • Example #9
        • Example #10
    • Test and Proof
      • Various Combinations of Tests and Proofs
      • Test (be)for(e) Proof
        • Activating Run-time Checks
        • Activating Assertions
        • Activating Ghost Code
      • Test for Proof
        • Overflow Checking Mode
      • Test alongside Proof
        • Checking Proof Assumptions
        • Rules for Defining the Boundary
        • Special Compilation Switches
      • Test as Proof
        • Feasibility of Exhaustive Testing
      • Test on top of Proof
        • Combining Unit Proof and Integration Test
      • Test Examples / Pitfalls
        • Example #1
        • Example #2
        • Example #3
        • Example #4
        • Example #5
        • Example #6
        • Example #7
        • Example #8
        • Example #9
        • Example #10

Labs

  • Introduction to Ada: Laboratories
    • Imperative Language
      • Hello World
      • Greetings
      • Positive Or Negative
      • Numbers
    • Subprograms
      • Subtract procedure
      • Subtract function
      • Equality function
      • States
      • States #2
      • States #3
      • States #4
    • Modular Programming
      • Months
      • Operations
    • Strongly Typed Language
      • Colors
      • Integers
      • Temperatures
    • Records
      • Directions
      • Colors
      • Inventory
    • Arrays
      • Constrained Array
      • Colors: Lookup-Table
      • Unconstrained Array
      • Product info
      • String_10
      • List of Names
    • More About Types
      • Aggregate Initialization
      • Versioning
      • Simple todo list
      • Price list
    • Privacy
      • Directions
      • Limited Strings
      • Bonus exercise
        • Colors
        • List of Names
        • Price List
    • Generics
      • Display Array
      • Average of Array of Float
      • Average of Array of Any Type
      • Generic list
    • Exceptions
      • Uninitialized Value
      • Numerical Exception
      • Re-raising Exceptions
    • Tasking
      • Display Service
      • Event Manager
      • Generic Protected Queue
    • Design by contracts
      • Price Range
      • Pythagorean Theorem: Predicate
      • Pythagorean Theorem: Precondition
      • Pythagorean Theorem: Postcondition
      • Pythagorean Theorem: Type Invariant
      • Primary Color
    • Object Oriented Programming
      • Simple type extension
      • Online Store
    • Standard Library: Containers
      • Simple todo list
      • List of unique integers
    • Standard Library: Dates & Times
      • Holocene calendar
      • List of events
    • Standard Library: Strings
      • Concatenation
      • List of events
    • Standard Library: Numerics
      • Decibel Factor
      • Root-Mean-Square
      • Rotation
    • Solutions
      • Imperative Language
        • Hello World
        • Greetings
        • Positive Or Negative
        • Numbers
      • Subprograms
        • Subtract Procedure
        • Subtract Function
        • Equality function
        • States
        • States #2
        • States #3
        • States #4
      • Modular Programming
        • Months
        • Operations
      • Strongly typed language
        • Colors
        • Integers
        • Temperatures
      • Records
        • Directions
        • Colors
        • Inventory
      • Arrays
        • Constrained Array
        • Colors: Lookup-Table
        • Unconstrained Array
        • Product info
        • String_10
        • List of Names
      • More About Types
        • Aggregate Initialization
        • Versioning
        • Simple todo list
        • Price list
      • Privacy
        • Directions
        • Limited Strings
      • Generics
        • Display Array
        • Average of Array of Float
        • Average of Array of Any Type
        • Generic list
      • Exceptions
        • Uninitialized Value
        • Numerical Exception
        • Re-raising Exceptions
      • Tasking
        • Display Service
        • Event Manager
        • Generic Protected Queue
      • Design by contracts
        • Price Range
        • Pythagorean Theorem: Predicate
        • Pythagorean Theorem: Precondition
        • Pythagorean Theorem: Postcondition
        • Pythagorean Theorem: Type Invariant
        • Primary Colors
      • Object-oriented programming
        • Simple type extension
        • Online Store
      • Standard library: Containers
        • Simple todo list
        • List of unique integers
      • Standard library: Dates & Times
        • Holocene calendar
        • List of events
      • Standard library: Strings
        • Concatenation
        • List of events
      • Standard library: Numerics
        • Decibel Factor
        • Root-Mean-Square
        • Rotation
  • Bug Free Coding
    • Let's Build a Stack
      • Background
      • Input Format
      • Constraints
      • Output Format
      • Sample Input
      • Sample Output

AdaCore Technologies Booklets

  • AdaCore Technologies For Airborne Software
    • 1. Introduction
    • 2. The DO-178C/ED-12C Standards Suite
      • 2.1. Overview
      • 2.2. Software Tool Qualification Considerations: DO-330/ED-215
      • 2.3. Model-Based Development and Verification Supplement: DO-331/ED-218
      • 2.4. Object-Oriented Technology and Related Techniques Supplement: DO-332/ED-217
      • 2.5. Formal Methods Supplement: DO-333/ED-216
    • 3. AdaCore Tools and Technologies Overview
      • 3.1. Ada
        • 3.1.1. Background
        • 3.1.2. Language Overview
      • 3.2. SPARK
        • 3.2.1. Flexibility
        • 3.2.2. Powerful Static Verification
        • 3.2.3. Ease of Adoption
        • 3.2.4. Reduced Cost and Improved Efficiency of Executable Object Code (EOC) verification
      • 3.3. GNAT Pro Assurance
        • 3.3.1. Sustained Branches
        • 3.3.2. Configurable Run-Time Libraries
        • 3.3.3. Full Implementation of Ada Standards
        • 3.3.4. Source to Object Traceability
        • 3.3.5. Safety-Critical Support and Expertise
        • 3.3.6. Libadalang
        • 3.3.7. GNATstack
      • 3.4. GNAT Static Analysis Suite (GNAT SAS)
        • 3.4.1. Defects and vulnerability analysis
        • 3.4.2. GNATmetric
        • 3.4.3. GNATcheck
      • 3.5. GNAT Dynamic Analysis Suite (GNAT DAS)
        • 3.5.1. GNATtest
        • 3.5.2. GNATemulator
        • 3.5.3. GNATcoverage
        • 3.5.4. GNATfuzz
        • 3.5.5. TGen
      • 3.6. GNAT Pro for Rust
      • 3.7. Integrated Development Environments (IDEs)
        • 3.7.1. GNAT Studio
        • 3.7.2. VS Code Extensions for Ada and SPARK
        • 3.7.3. Eclipse support - GNATbench
        • 3.7.4. GNATdashboard
    • 4. Compliance with DO-178C / ED-12C Guidance: Analysis
      • 4.1. Overview
      • 4.2. Use case #1a: Coding with Ada 2012
        • 4.2.1. Benefits of the Ada language
        • 4.2.2. Using Ada during the design process
        • 4.2.3. Integration of C components with Ada
        • 4.2.4. Robustness / defensive programming
        • 4.2.5. Defining and Verifying a Code Standard with GNATcheck
        • 4.2.6. Checking source code accuracy and consistency with GNAT SAS
        • 4.2.7. Checking worst case stack consumption with GNATstack
        • 4.2.8. Compiling with the GNAT Pro compiler
        • 4.2.9. Using GNATtest for low-level testing
        • 4.2.10. Using GNATemulator for low-level and software / software integration tests
        • 4.2.11. Structural code coverage with GNATcoverage
        • 4.2.12. Data and control coupling coverage with GNATcoverage
        • 4.2.13. Demonstrating traceability of source to object code
      • 4.3. Use case #1b: Coding with Ada using OOT features
        • 4.3.1. Object orientation for the architecture
        • 4.3.2. Coverage in the case of generics
        • 4.3.3. Dealing with dynamic dispatching and substitutability
        • 4.3.4. Dispatching as a new module coupling mechanism
        • 4.3.5. Memory management issues
        • 4.3.6. Exception handling
        • 4.3.7. Overloading and type conversion vulnerabilities
        • 4.3.8. Accounting for dispatching in performing resource analysis
      • 4.4. Use case #2: Using SPARK and Formal Methods
        • 4.4.1. Using SPARK for design data development
        • 4.4.2. Robustness and SPARK
        • 4.4.3. Contributions to Low-Level Requirement reviews
        • 4.4.4. Contributions to architecture reviews
        • 4.4.5. Contributions to source code reviews
        • 4.4.6. Formal analysis as an alternative to low-level testing
        • 4.4.7. Low-level verification by mixing test and proof ("Hybrid verification")
        • 4.4.8. Alternatives to code coverage when using proofs
        • 4.4.9. Property preservation between source code and object code
        • 4.4.10. SPARK Development Cycle Example
      • 4.5. Parameter Data Items
    • 5. Summary of contributions to DO-178C/ED-12C objectives
      • 5.1. Overall summary: which objectives are met
        • 5.1.1. Mapping of AdaCore's Technologies to DO-178C/ED-12C Objectives
      • 5.2. Detailed summary: which activities are supported
        • 5.2.1. Table A-1: Software Planning Process
        • 5.2.2. Table A-2: Software Development Processes
        • 5.2.3. Table A-4: Verification of Outputs of Software Design Process
        • 5.2.4. Table A-5 Verification of Outputs of Software Requirement Process
        • 5.2.5. Table A-6 Testing of Outputs of Integration Process
        • 5.2.6. Table A-7 Verification of Verification Process Results
      • 5.3. AdaCore Tool Qualification and Library Certification
    • 6. Bibliography
learn.adacore.com
  • Advanced Journey With Ada: A Flight In Progress (UNPUBLISHED)
  • Resource Management

Resource Management

  • Memory Management
    • Maximum allocation size and alignment
      • Code example with scalar type
      • Code example with array type
    • Storage elements
    • Memory pools
    • Memory subpools
    • Secondary stack
  • Containers
    • Aggregate aspect
      • Basic syntax
      • Classification
      • Empty
      • Add_Named
      • Add_Unnamed
      • Assign_Indexed
      • Combining Add_Named and Assign_Indexed
    • User-Defined Iterator Types
  • Standard Containers
    • Linked lists
    • Trees
    • Queue containers
    • Indefinite containers
    • Holder container
  • Restrictions and Profiles
    • Pragmas
    • Language-Defined Restrictions and Profiles
Previous Next

© Copyright 2018 – 2025, AdaCore. All rights reserved.    Creative Commons License
Legal   |   Privacy Policy   |   Report an Issue