LEARN.ADACORE.COM

Edit on GitHub

What is Ada and SPARK?

Ada is a state-of-the art programming language that development teams worldwide are using for critical software: from microkernels and small-footprint, real-time embedded systems to large-scale enterprise applications, and everything in between.

SPARK is formally analyzable subset of Ada — and toolset that brings mathematics-based confidence to software verification.

Try Ada Now:

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;

Check out the interactive courses and labs to learn more about Ada and SPARK.

---

• 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
      • Parameter modes
      • Subprogram calls
      • Renaming
    • Modular Programming
      • Packages
      • Using a package
      • Package body
      • Child packages
      • Renaming
    • 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
      • 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
      • Access types (pointers)
      • Mutually recursive types
      • More about records
      • Fixed-point types
      • Character 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
      • 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
      • Private & Limited
      • Classwide access types
    • Standard Library: Containers
      • Vectors
      • Sets
      • Indefinite maps
    • Standard Library: Dates & Times
      • Date and time handling
      • Real-time
    • 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
      • 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
  • 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
  • Introduction to GNAT Toolchain
    • GNAT Community
      • Installation
      • Basic commands
      • Compiler warnings
    • GPRbuild
      • Basic commands
      • Project files
      • Project dependencies
      • Configuration pragma files
      • Configuration packages
    • GNAT Studio
      • Start-up
      • Creating projects
      • Building
      • Debugging
      • Formal verification
    • GNAT Tools
      • gnatchop
      • gnatprep
      • gnatmem
      • gnatmetric
      • gnatdoc
      • gnatpp
      • gnatstub
• Labs
  • Introduction to Ada
    • 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
    • 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
      • 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
  • Bug Free Coding
    • Let's Build a Stack
      • Background
      • Input Format
      • Constraints
      • Output Format
      • Sample Input
      • Sample Output

Download Ada and SPARK tools

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 Studio IDE.

---

We’re calling on developers across the globe to build cool embedded applications using the Ada and SPARK programming languages and are offering over $9,000 in total prizes! Click on the banner above to learn more.