LEARN.ADACORE.COM¶
Edit on GitHubWhat 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:¶
Check out the interactive courses and labs to learn more about Ada and SPARK.
- About
- Courses
- Introduction to Ada
- Introduction
- Imperative Language
- Subprograms
- Modular Programming
- Strongly Typed Language
- Records
- Arrays
- More About 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
- Introduction to SPARK
- Ada for the C++ or Java Developer
- 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
- Introduction to GNAT Toolchain
- Introduction to Ada
- Labs
- Introduction to Ada
- 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
- 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
- Introduction to Ada
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.
GNAT Academic Program¶
Teachers and graduate students who are interested in teaching or using Ada or SPARK can take advantage of AdaCore's GNAT Academic Program (GAP).
GAP's primary objective is to help put Ada and SPARK at the forefront of university study by building a community of academic professionals. GAP members receive a comprehensive toolset and professional support package specifically designed to provide the tools needed to teach and use Ada and SPARK in an academic setting. Best of all, AdaCore provides the GAP Package to eligible members at no cost. Register for membership today and join over 100 member universities in 35 countries currently teaching Ada and SPARK using GAP.
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.