The Ada programming language was originally designed to meet the US Department of Defense Requirements for programming military applications. Since its first version (Ada 83) it has evolved through multiple versions: Ada 95, Ada 2005 and Ada 2012 (released in December 10, 2012).17 Ada is actively used in many real-world projects in critical application domains,18 e.g. Aviation (Boeing19), Railway Transportation, Commercial Rockets, Satellites and even Banking. One of the main goals of Ada is to ensure software correctness
and safety. Ada includes features that eliminate common errors involving pointers, array bounds violations and unprincipled control flow, in comparison to other programming languages (see Figure 2.6). This is achieved not only by language capabilities, but also by tools for testing and verification.
SPARK is a programming language and static verification technology designed specifically for the development of high integrity software. It is a "safe" subset of Ada, designed to be amenable to state analysis and formal methods, by collection of analysis and verification tools. Some Ada constructs are excluded from SPARK to make static analysis feasible [IEC+06]. SPARK 2005 does not include constructs such as pointers, dynamic memory allocation or recursion [IEC+06].
Defines standard
Replaced/Superseded by document(s)
Cancelled by
Amended by
| File | MIME type | Size (KB) | Language | Download | |
|---|---|---|---|---|---|
| JakubJedryszek2014.pdf | application/pdf | 2.75 MB | English | DOWNLOAD! |
Provides definitions
Introduction
Software is present in all aspects of our lives, from the simple program in alarm clocks to iPads, through cars, refrigerators and computers. Furthermore, our lives are getting more and more dependent on software. Usually when we think about software, we think about applications for PC or smart phone, e.g. calculator, word processor or stock market application. In this case, rapid development and smooth operation is a key.