Contents Menu Expand Light mode Dark mode Auto light/dark, in light mode Auto light/dark, in dark mode Skip to content

⚠️ This version of the website contains UNPUBLISHED contents. ⚠️

learn-sandbox.adacore.com
Logo
  • About

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
    • 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
  • Introduction to SPARK
    • Overview
    • Flow Analysis
    • Proof of Program Integrity
    • State Abstraction
    • Proof of Functional Correctness
  • Introduction to Embedded Systems Programming
    • Introduction
    • Low Level Programming
    • Multi-Language Development
    • Interacting with Devices
    • General-Purpose Code Generators
    • Handling Interrupts
    • Conclusion
  • 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
  • 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
  • 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
  • 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
  • Introduction to the GNAT Toolchain
    • GNAT Toolchain Basics
    • GPRbuild
    • GNAT Studio
    • GNAT Tools
  • 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

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
Back to top
View this page
Edit this page

Design by contract¶

  • Contracts
    • Class-wide contracts
    • Default initial conditions
    • Entry index attribute
    • Global Aspect Definition
    • Predicate failure
    • Stable Properties of a Type
Next
Contracts
Previous
Generics
Copyright © 2018 – 2025, AdaCore. All rights reserved
Made with Furo