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
    • 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
      • Declaring arrays (2)
      • Array slices
    • Modular Programming
      • Packages
      • Using a package
      • Package body
    • Subprograms
      • Subprograms
      • Parameters modes
      • Subprogram calls
    • 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
  • Advanced Ada
    • Typing
      • Overloading
    • Strong Typing
      • Type-based security
      • Table access
      • Multiple indices
    • Access Types
      • Null & Not Null Access
      • Accessibility checks
    • Limited Types
      • Limited types and aggregates
      • Return objects
      • Building objects from constructors
      • Default initialization
    • Generics
      • Formal packages
      • Formal objects
      • Generic interfaces
      • Generic numeric types
    • Interfacing With C/C++
      • Interfacing with C
      • Interfacing with C++
  • 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
    • Type Contracts
      • Type Contracts in Ada 2012 and SPARK 2014
      • Static and Dynamic Predicates
      • Type Invariant
      • Inheritance of Predicates and Type Invariants
      • Other Useful Gotchas on Predicates and Type Invariants
      • Default Initial Condition
      • Code Examples / Pitfalls
    • 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
      • 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
    • 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
    • Object-oriented Programming
      • What is Object Oriented Programming?
      • Prototypes and Scopes in SPARK
      • Classes in SPARK
      • Methods in SPARK
      • Dynamic dispatching in SPARK
      • LSP – the SPARK solution to dynamic dispatching problems
      • Dynamic semantics of class-wide contracts
      • Redispatching and Extensions_Visible aspect
      • Code Examples / Pitfalls
    • 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
      • Extreme proving with ghost code – red black trees in SPARK
      • Positioning ghost code in proof techniques
      • Code Examples / Pitfalls
    • Test and Proof
      • Various Combinations of Tests and Proofs
      • Test (be)for(e) Proof
      • Test for Proof
      • Test alongside Proof
      • Test as Proof
      • Test on top of Proof
      • Test 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 for the MISRA-C Developer
    • Preface
    • Enforcing Basic Program Consistency
      • Taming Text-Based Inclusion
      • Hardening Link-Time Checking
      • Going Towards Encapsulation
    • Recovering Basic Syntactic Guarantees
      • Distinguishing Code and Comments
      • Handling Specially Function Parameters and Result
      • Ensuring Control Structures Are Not Abused
    • Retrofitting Strong Typing Rules
      • Enforcing Strong Typing for Pointers
      • Enforcing Strong Typing for Scalars
    • Initializing Data Before Use
      • Detecting Read of Uninitialized Data
      • Detecting Partial or Redundant Initialization of Arrays and Structures
    • Controlling Side-Effects
      • Preventing Undefined Behavior
      • Reducing Programmer Confusion
      • Control of Side-Effects in SPARK
    • Detecting Undefined Behavior
      • Undefined Behavior in SPARK
      • Proof of Absence of Runtime Errors in SPARK
    • Detecting Unreachable Code and Dead Code
    • Conclusion
    • References
      • About MISRA-C
      • About SPARK
      • About MISRA-C and SPARK

---

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.

---