Contents Menu Expand Light mode Dark mode Auto light/dark, in light mode Auto light/dark, in dark mode Skip to content
learn.adacore.com
Logo
  • About

Ada Courses

  • Introduction to Ada
    • Introduction
    • Imperative Language
    • Subprograms
    • Modular Programming
    • Strongly Typed Language
    • Records
    • Arrays
    • More About Types
    • Access Types
    • More About Records
    • Fixed-Point Types
    • Privacy
    • Generics
    • Exceptions
    • Tasking
    • Design by contracts
    • Interfacing With C
    • Object Oriented Programming
    • Standard Library: Containers
    • Standard Library: Dates & Times
    • Standard Library: Strings
    • Standard Library: Files & Streams
    • Standard Library: Numerics
    • Appendices
  • Advanced Journey With Ada
    • Data types
      • Types
      • Types and Representation
      • Shared variable control
      • Records
      • Aggregates
      • Arrays
      • Strings
      • Numerics
      • Numeric Attributes
    • Control Flow
      • Expressions
      • Statements
      • Subprograms
      • Exceptions
    • Modular programming
      • Packages
      • Subprograms and Modularity
    • Resource Management
      • Access Types
      • Anonymous Access Types
      • Limited Types
      • Controlled Types
  • Ada In Practice
    • Introduction
    • Essential Design Idioms for Packages
    • Abstract Data Types
    • Abstract Data Machines
    • Programming by Extension
    • Constructor Functions For Abstract Data Types
    • Controlling Object Initialization and Creation
    • Type Punning
    • Expressing Inheritance Idioms
    • Providing Component Access to Enclosing Record Objects
    • Interrupt Handling
    • Reducing Object Code from Generic Package Instantiations
    • Resource Acquisition Is Initialization (RAII)
    • Using Streams for API Flexibility
    • Dealing with Silent Task Termination
    • Idioms for Protected Objects
  • Ada for the C++ or Java Developer
    • Preface
    • Basics
    • Compilation Unit Structure
    • Statements, Declarations, and Control Structures
    • Type System
    • Functions and Procedures
    • Packages
    • Classes and Object Oriented Programming
    • Generics
    • Exceptions
    • Concurrency
    • Low Level Programming
    • Conclusion
    • References

SPARK Courses

  • Introduction to SPARK
    • Overview
    • Flow Analysis
    • Proof of Program Integrity
    • State Abstraction
    • Proof of Functional Correctness
  • SPARK Ada for the MISRA C Developer
    • Preface
    • Enforcing Basic Program Consistency
    • Enforcing Basic Syntactic Guarantees
    • Enforcing Strong Typing
    • Initializing Data Before Use
    • Controlling Side Effects
    • Detecting Undefined Behavior
    • Detecting Unreachable Code and Dead Code
    • Conclusion
    • References

Ada for Embedded Courses

  • Introduction to Embedded Systems Programming
    • Introduction
    • Low Level Programming
    • Multi-Language Development
    • Interacting with Devices
    • General-Purpose Code Generators
    • Handling Interrupts
    • Conclusion
  • Ada for the Embedded C Developer
    • Introduction
    • The C Developer's Perspective
    • Concurrency and Real-Time
    • Writing Ada on Embedded Systems
    • Enhancing Verification with SPARK and Ada
    • C to Ada Translation Patterns
    • Handling Variability and Re-usability
    • Performance Considerations
    • Argumentation and Business Perspectives
    • Conclusion
    • Hands-On: Object-Oriented Programming

Ada/SPARK: General Material

  • Guidelines for Safe and Secure Ada/SPARK
    • Introduction
    • Definitions
    • Dynamic Storage Management
      • Common High Integrity Restrictions (DYN01)
      • Traditional Static Allocation Policy (DYN02)
      • Access Types Without Allocators Policy (DYN03)
      • Minimal Dynamic Allocation Policy (DYN04)
      • User-Defined Storage Pools Policy (DYN05)
      • Statically Determine Maximum Stack Requirements (DYN06)
    • Safe Reclamation
      • No Multiple Reclamations (RCL01)
      • Only Reclaim Allocated Storage (RCL02)
      • Only Reclaim To The Same Pool (RCL03)
    • Concurrency
      • Use the Ravenscar Profile (CON01)
      • Use the Jorvik Profile (CON02)
      • Avoid Shared Variables for Inter-task Communication (CON03)
    • Robust Programming Practice
      • No Use of "others" in Case Constructs (RPP01)
      • No Enumeration Ranges in Case Constructs (RPP02)
      • Limited Use of "others" In Aggregates (RPP03)
      • No Unassigned Mode-Out Procedure Parameters (RPP04)
      • No Use of "others" in Exception Handlers (RPP05)
      • Avoid Function Side-Effects (RPP06)
      • Functions Only Have Mode "in" (RPP07)
      • Limit Parameter Aliasing (RPP08)
      • Use Precondition and Postcondition Contracts (RPP09)
      • Do Not Re-Verify Preconditions In Subprogram Bodies (RPP10)
      • Always Use the Result of Function Calls (RPP11)
      • No Recursion (RPP12)
      • No Reuse of Standard Typemarks (RPP13)
      • Use Symbolic Constants For Literal Values (RPP14)
    • Exception Usage
      • Do Not Raise Language-Defined Exceptions (EXU01)
      • No Unhandled Application-Defined Exceptions (EXU02)
      • No Exception Propagation Beyond Name Visibility (EXU03)
      • Prove Absence of Run-time Exceptions (EXU04)
    • Object-Oriented Programming
      • No Class-wide Constructs Policy (OOP01)
      • Static Dispatching Only Policy (OOP02)
      • Limit Inheritance Hierarchy Depth (OOP03)
      • Limit Statically-Dispatched Calls To Primitive Operations (OOP04)
      • Use Explicit Overriding Annotations (OOP05)
      • Use Class-wide Pre/Post Contracts (OOP06)
      • Ensure Local Type Consistency (OOP07)
    • Software Engineering
      • Use SPARK Extensively (SWE01)
      • Enable Optional Warnings and Treat As Errors (SWE02)
      • Use A Static Analysis Tool Extensively (SWE03)
      • Hide Implementation Artifacts (SWE04)
    • References
  • What's New in Ada 2022
    • Introduction
    • 'Image attribute for any type
    • Redefining the 'Image attribute
    • User-Defined Literals
    • Advanced Array Aggregates
    • Container Aggregates
    • Delta Aggregates
    • Target Name Symbol (@)
    • Enumeration representation
    • Big Numbers
    • Interfacing C variadic functions
  • Introduction to the GNAT Toolchain
    • GNAT Toolchain Basics
    • GPRbuild
    • GNAT Studio
    • GNAT Tools

Upcoming Courses

  • Advanced Journey With Ada (UNPUBLISHED)
    • Resource Management
      • Memory Management
      • Containers
      • Standard Containers
      • Restrictions and Profiles
    • Abstraction-oriented programming
      • Strong typing
      • Object-Oriented Programming
      • Generics
    • Design by contract
      • Contracts
    • Initialization
      • Freezing
      • Package Elaboration
      • Elaboration Of Generics
    • Multithreading
      • Tasking
    • Interfacing with the external world
      • File I/O
      • Interfacing with C and C++
    • Appendices
      • Legacy features
  • Advanced SPARK
    • Subprogram Contracts
    • Type Contracts
    • Systems Programming
    • Concurrency
    • Object-oriented Programming
    • Ghost code
    • Test and Proof

Labs

  • Introduction to Ada: Laboratories
    • Imperative Language
    • Subprograms
    • Modular Programming
    • Strongly Typed Language
    • Records
    • Arrays
    • More About Types
    • Privacy
    • Generics
    • Exceptions
    • Tasking
    • Design by contracts
    • Object Oriented Programming
    • Standard Library: Containers
    • Standard Library: Dates & Times
    • Standard Library: Strings
    • Standard Library: Numerics
    • Solutions
  • Bug Free Coding
    • Let's Build a Stack

AdaCore Technologies Booklets

  • AdaCore Technologies For Airborne Software
    • 1. Introduction
    • 2. The DO-178C/ED-12C Standards Suite
    • 3. AdaCore Tools and Technologies Overview
    • 4. Compliance with DO-178C / ED-12C Guidance: Analysis
    • 5. Summary of contributions to DO-178C/ED-12C objectives
  • AdaCore Technologies For Railway Software
    • 1. Introduction
    • 2. CENELEC EN 50128
    • 3. Tools and Technologies Overview
    • 4. AdaCore Contributions to The Software Quality Assurance Plan
    • 5. Technology Usage Guide
    • 6. Technology Annex
  • AdaCore Technologies For Space Systems Software
    • 1. Introduction
    • 2. Programming Languages for Space Software
    • 3. Tools for Space Software Development
    • 4. Compliance with ECSS-E-ST-40C
    • 5. Compliance with ECSS-Q-ST-80C
    • 6. Abbreviations
Back to top
View this page
Edit this page

Contracts¶

Class-wide contracts¶

Default initial conditions¶

Relevant topics

  • Default Initial Conditions

Entry index attribute¶

Relevant topics

  • E'Index mentioned in Preconditions and Postconditions

Global Aspect Definition¶

Relevant topics

  • The Global and Global'Class Aspects

Predicate failure¶

Relevant topics

  • Predicate_Failure mentioned in Subtype Predicates

Stable Properties of a Type¶

In the Ada Reference Manual

  • Stable Properties of a Type

Next
Initialization
Previous
Design by contract
Copyright © 2018 – 2026, AdaCore. All rights reserved
Made with Furo
On this page
  • Contracts
    • Class-wide contracts
    • Default initial conditions
    • Entry index attribute
    • Global Aspect Definition
    • Predicate failure
    • Stable Properties of a Type