Comparison of SPARK and MISRA C Programming Languages

This document is a technical report that compares the programming languages SPARK and MISRA C, both of which are designed for high-assurance applications where reliability and safety are critical. It outlines the features of SPARK, a subset of Ada, which is tailored for formal analysis and aims to eliminate common programming errors through its restrictions. The report details how SPARK supports contracts for program properties and integrates formal methods with traditional testing. It also provides an overview of MISRA C, which sets guidelines to mitigate the pitfalls of the C programming language in safety-related applications. The comparison focuses on four criteria essential for high-assurance software: syntax, typing, subsetting, and run-time verification. The document highlights the advantages of SPARK in avoiding common coding traps and its superior type system, which allows for more reliable and general capabilities than those provided by MISRA C. The analysis aims to inform developers about the strengths and weaknesses of both languages in the context of high-assurance software development.