This tutorial introduces the SPARK language and its associated analysis tools. It explains key differences from Ada that enable formal verification. Readers learn about adding basic contracts and analyzing code with tools like GNATprove. Advanced topics like state abstraction and ghost code are demonstrated. Numerous examples of varying complexity cement understanding.
Recommended for: Beginner to intermediate readers interested in learning about the SPARK formal verification tool for the Ada programming language. This course is suitable for developers with some prior programming experience, particularly in systems programming or embedded development.
You will:
- Gain a comprehensive understanding of the SPARK language and its key tools, including how it compares to standard Ada
- Learn about SPARK’s core capabilities, such as flow analysis, proof of program integrity, and proof of functional correctness
- Explore advanced SPARK concepts like state abstraction, subprogram contracts, and using SPARK for embedded systems programming
- See numerous code examples and common pitfalls related to developing SPARK-verifiable software
- Understand how SPARK can be used alongside the Ada programming language to enhance safety, security, and reliability of critical systems
Detailed Overview
Created by SPARK experts at AdaCore, the document provides a thorough yet accessible introduction to writing provably correct code. Initial chapters illustrate fundamental SPARK concepts like subprogram contracts and data dependencies. Examples show violations found through flow analysis. Later material addresses state abstraction modeling and ghost code for functional proof. Each major section contains over 10 complete, analyzable programs to demonstrate concepts hands-on. Detailed explanations dissect examples, highlighting contracts, analysis output, and techniques for debugging proof failures. Special attention is given to common pitfalls. The comprehensive yet approachable resource equips both novice and experienced developers with conceptual foundations and practical skills for applying SPARK’s static analysis to develop high-assurance systems.
Citation
Claire Dross and Yannick Moy. Introduction to SPARK. AdaCore, 2024. https://learn.adacore.com/courses/intro-to-spark/index.html
Licensing
This work is licensed under a Creative Commons Attribution 4.0 International (CC BY 4.0) license. The full text of the license is available at https://creativecommons.org/licenses/by/4.0/.
Download
