LEARN.ADACORE.COM

Edit on GitHub

Learn.adacore.com is an interactive learning platform designed to teach the Ada and SPARK programming languages.

with Ada.Text_IO; use Ada.Text_IO; procedure Learn is subtype Alphabet is Character range 'A' .. 'Z'; begin Put_Line ("Learning Ada from " & Alphabet'First & " to " & Alphabet'Last); end Learn;

• About
• Courses
  • Introduction to Ada
    • Introduction
      • History
      • Ada today
      • Philosophy
      • SPARK
    • Imperative Language
      • Hello world
      • Imperative language - If/Then/Else
      • Imperative language - Loops
      • Imperative language - Case statement
      • Imperative language - Declarative regions
      • Imperative language - conditional expressions
    • Subprograms
      • Subprograms
      • Parameters modes
      • Subprogram calls
    • Modular Programming
      • Packages
      • Using a package
      • Package body
    • Strongly Typed Language
      • What is a type?
      • Integers
      • Unsigned types
      • Enumerations
      • Floating-point types
      • Strong typing
      • Derived types
      • Subtypes
    • Records
      • Record type declaration
      • Aggregates
      • Component selection
    • 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
    • More About Types
      • Aggregates: A primer
      • Overloading and qualified expressions
      • Access types (pointers)
      • Mutually recursive types
      • More about records
      • Fixed-point types
      • Character types
    • Privacy
      • Basic encapsulation
      • Abstract data types
      • Limited types
    • Generics
      • Introduction
      • Examples of using generics
    • Exceptions
      • Exception declaration
      • Raising an exception
      • Handling an exception
      • Predefined exceptions
    • Tasking
      • Tasks
      • Protected objects
      • Task and protected types
    • Design by contracts
      • Pre- and postconditions
      • Predicates
      • Type invariants
    • Interfacing With C
      • Multi-language project
      • Type convention
      • Foreign subprograms
      • Foreign variables
      • Generating bindings
    • Object Oriented Programming
      • Derived types
      • Tagged types
      • Classwide types
      • Dispatching operations
      • Dot notation
    • Standard Library
      • Standard package
      • Containers
      • Dates & Times
      • Strings
      • Files and streams
      • Numerics
    • Appendices
      • Appendix A: Generic Formal Types
      • Appendix B: Containers
  • Introduction to SPARK
    • Overview
      • What is it?
      • What do the tools do?
      • Key Tools
      • A trivial example
      • The Programming Language
      • Limitations
      • Designating SPARK Code
      • Code Examples / Pitfalls
    • Flow Analysis
      • What does flow analysis do?
      • Errors Detected
      • Additional Verifications
      • Shortcomings
      • Code Examples / Pitfalls
    • Proof of Program Integrity
      • Runtime Errors
      • Modularity
      • Contracts
      • Debugging Failed Proof Attempts
      • Code Examples / Pitfalls
    • 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
      • Subprogram Contracts
      • Initialization of Local Variables
      • Code Examples / Pitfalls
    • Proof of Functional Correctness
      • Beyond Program Integrity
      • Advanced Contracts
      • Guide Proof
      • Code Examples / Pitfalls
• Books
  • 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 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
      • Ensuring Control Structures Are Not Abused
    • Enforcing Strong Typing
      • Enforcing Strong Typing for Pointers
      • Enforcing Strong Typing for Scalars
    • 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
  • Getting Started with GNAT Toolchain
    • Introduction
    • GNAT Community
      • Installation
      • Basic commands
    • GPRbuild
      • Basic commands
      • Project files
    • GNAT Programming Studio (GPS)
      • Start-up
      • Creating projects
      • Building
      • Debugging
      • Formal verification

---

Try Ada and SPARK now with GNAT Community edition.

GNAT Community includes the Ada compiler and toolchain, the SPARK verifier and provers, and the GNAT Programming Studio IDE.