This technical resource compares the SPARK subset of the Ada programming language and its verification tools to the MISRA C coding standard. It outlines issues in C like weak typing and undefined behaviors that make analysis difficult. The document shows how SPARK/Ada addresses these through language features and principles, enforcing properties like absence of unintended behaviors that are challenging to check with MISRA C alone. Code examples demonstrate SPARK’s strict type checking and initialized variable enforcement through static analysis.
Recommended for: Intermediate to advanced readers who are familiar with the C programming language and are interested in transitioning to the Ada and SPARK programming languages. This course is suitable for C developers who want to learn how to apply MISRA C guidelines in a more formal and rigorous programming environment.
You will:
- Understand the key differences between C and Ada/SPARK in terms of language features, type system, and programming paradigms.
- Learn how to apply MISRA C guidelines in an Ada/SPARK context to write safe, secure, and reliable software.
- Explore the SPARK subset of Ada and how it can be used to formally verify the absence of run-time errors and prove high-level functional properties of your code.
- Gain practical experience with the GNAT toolchain and its capabilities for building, analyzing, and verifying Ada/SPARK applications.
- Discover techniques for interfacing Ada/SPARK code with existing C libraries and systems.
- Understand the benefits and tradeoffs of adopting Ada and SPARK in an embedded systems or safety-critical software development context.
Detailed Overview
The document begins by outlining issues in the C language that can lead to bugs and vulnerabilities, such as its textual file inclusion model, lack of consistency checks across files, weak encapsulation, and undefined behaviors. These issues complicate comprehensive static analysis. It then examines how SPARK/Ada addresses these problems through language principles and features like semantic module import, global namespaces, compiler-enforced abstraction, contract-based specifications, and strong typing. The document demonstrates how SPARK can enforce properties like initialized variables, absence of unintended behaviors, and elimination of dead/unreachable code – which are difficult to fully check with MISRA C. It provides specific code examples illustrating SPARK’s enforcement of type guarantees, initialization checking, controlling side effects through specifications, and detection of undefined behaviors and dead code via interactive static analysis at the function level. Overall, the document serves as both a SPARK tutorial and technical reference, introducing SPARK as a strict Ada subset that builds upon MISRA C goals with stronger guarantees through Ada language principles and analysis tools.
Citation
Yannick Moy, Ben Brosgol, SPARK Ada for the MISRA C Developer (AdaCore, 2022), https://learn.adacore.com/courses/SPARK_for_the_MISRA_C_Developer/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
