Comparison of SPARK and MISRA C Programming Languages

This document is a technical report that compares SPARK and MISRA C, two programming languages designed for high-assurance applications where reliability is critical. It outlines the features of both languages and evaluates their effectiveness in meeting safety and security requirements. The report begins with an overview of SPARK, a subset of Ada, which emphasizes formal analysis and the absence of unspecified behavior. It details how SPARK incorporates contracts for program properties and supports both proof and testing methodologies. The document then introduces MISRA C, which aims to mitigate the pitfalls of the C programming language through a set of best practices. It specifies over 100 rules to promote safe coding in safety-related applications. The comparison focuses on four criteria: syntax, typing, subsetting, and run-time verification, highlighting the strengths and weaknesses of each language in these areas. The report concludes with a discussion on the implications of these differences for developers working on high-assurance software.