SPARK Ada programming language
Before I joined SAnToS Lab, I heard about Ada programming language only a few times. I thought it is an ancient language, that nobody is using anymore. I assumed, that only reason why somebody may bother are some legacy applications written 30 years ago. I thought that safety-critical and high-assurance systems are developed in C/C++ or even Assembly language.
I was wrong.
Ada programming language
First version of Ada programming language - Ada 83 - was designed to meet the US Department of Defence Requirements formalized in "Steelman" document. Since that time, Ada evolved. There were Ada 95, Ada 2005 and Ada 2012 (released in December 10, 2012). Ada is activelly used in many Real-World projects, e.g. Aviation (Boeing 777's Software is written in Ada), Railway Transportation, Commercial Rockets, Satellites and even Banking. One of the main goals of Ada is to ensure software correctness and safety. The picture below, shows what is the goal of Ada: prevent the Developer from introducing bugs into system by rich tooling and language properties.
Ada does not use curly braces. The code listing below shows "Hello, World" in Ada:
The table below, shows C# code, and equivalent Ada code.
The equivalent for C# class - in Ada - is package. It has two files: specification (.ads file) and body (.adb file). It is like header (.h) and implementation (.cpp) files for class definition in C++. Additionally:
- class variables in C# conforms to 'global' variables in Ada package (the name 'global' in Ada package means that variable is visible for entire package, not entire application like in C/C++)
- C# class have methods, which returns value or not (
void). In Ada, methods are called subprograms. There are two distinguished types of them: functions (returns something) and procedures (does not return anything).
Here is sample C# class:
And its equivalent package in Ada:
SPARK programming language is based on Ada. Thus, it is usually referred as "SPARK Ada".
SPARK is a programming language and static verification technology designed specifically for the development of high integrity software. First version was designed over 20 years ago. SPARK excludes some Ada constructs (i.e. pointers, dynamic memory allocation or recursion) to make static analysis feasible. Additionally SPARK contains tool-set for Software Verification:
- Examiner - analyze code and ensures that it conforms to the SPARK language; also verify program to some extent using Verification Conditions (e.g. array index out of range, type range violation, division by zero, numerical overflow etc.)
- Simplifier - simplify Verification Conditions generated by Examiner
- Proof Checker - prove the Verification Conditions
Using SPARK, a developer takes a Z specification and performs a stepwise refinement from the specification to SPARK code. For each refinement step a tool is used to produce verification conditions (VC's), which are mathematical theorems. If the VC's can be proved then the refinement step will be known to be valid. However if the VC's cannot be proved then the refinement step may be erroneous.
First version of SPARK (SPARK 83) was based on Ada 83. The second version (SPARK 95) - on Ada 95. Current version - SPARK 2005 - is based on Ada 2005. It is a subset of Ada 2005 with annotations. The annotation language support flow analysis and formal verification. Annotations are encoded in Ada comments (via the prefix
--#). It makes every SPARK 2005 program, valid Ada 2005 program. Code listing below shows example SPARK 2005 package specification.
It is an interface for simple Odometer. There are 4 subprograms (2 procedures and 2 functions):
Zero_Tripprocedure - reset Odometer to 0
Read_Tripfunction - returns current distance
Read_Totalfunction - returns total distance traveled
Incprocedure- increment total and current distance by 1
global means that subprogram uses some global variable. Postfix
in out means that particular variable is read, write or read and write respectively. Annotation
derives says that some variable value depends on other variables. E.g. in procedure
Trip is dependent on its current value (before procedure call). Annotations
post define pre- and postconditions of procedure (only
post is present in above example). We can see, that in
Zero_Trip procedure postcondition requires that variable
Trip is equal to 0. In procedure
Inc, postconditions requires that variables
Total are incremented by 1 ('
~' is the value of variable before procedure call). Annotation
own expose private variables for use in public methods specification.
We can see, that SPARK contracts describe the functionality of particular subprograms. It is like documentation. You can find more about SPARK contracts in Tokeneer Discovery tutorial and SPARK 2005 to SPARK 2014 Mapping Specification.
The next version, SPARK 2014 (based on Ada 2012) is under development. There is partial tool support (in GNAT Programming Studio), but some language features are still not supported. It is worth to mention, that Ada 2012 contains code contracts. Thus SPARK 2014 is just subset of Ada 2012. There are no additional constructs like annotations in SPARK 2005, because now, contracts are part of the language.
In real-world applications, the embedded critical components are written in SPARK while the non-critical components are written in Ada.
I am working with SPARK Ada for more than 1 year. My (beginner) thoughts are as follows:
- I don't like the syntax. It is not developer friendly. You need to do a lot of repetitions, of the same code (e.g. subprograms declaration/definition). Syntax is very verbose, e.g. code blocks starts with
beginand ends with
endkeywords. It means more writing than in case when you use 'curly braces' for that.
- It is very hard to create valid and working SPARK program. There are many rules and limitations (e.g. no dynamic allocation).
- Quite steep learning curve. Additionally, it is not easy to find some resources like tutorials, books, videos.
- SPARK Ada IDE - GNAT Programming Studio - is very specific, and different than the most popular IDEs (e.g. Visual Studio or Eclipse). It is also less powerful, in case of e.g. intellisense, key shortcuts or project manipulations.
From my perspective, SPARK is a temporary subset of Ada, chosen for software verification. Once, verification techniques evolves, more features of Ada are getting included in SPARK. Maybe, in some day, there will be no SPARK, but just Ada, and tools will be able to verify (reason about) all its features.
More about Ada you can find at Ada Programming at Wikibooks, AdaCore University (video tutorials) and at ada2012.org website. Good place to start getting familiar with SPARK is Tokeneer Discovery tutorial (SPARK 2005) and SPARK 2014 tutorial. This lecture gives SPARK overview in nutshell. More about SPARK 2014 can be found in SPARK 2014 website, SPARK 2014 Toolset User's Guide and SPARK 2014 Reference Manual. To go deeper, there is a book SPARK: THE PROVEN APPROACH TO HIGH INTEGRITY SOFTWARE by John Barnes.