SPARK Ada programming language

Date: April 10, 2014

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 responsibilities

Ada does not use curly braces. The code listing below shows "Hello, World" in Ada:

with Ada.Text_IO; 
use Ada.Text_IO;

procedure Hello is 
begin   
  Put_Line ("Hello, world!"); 
end Hello;

Basic constructs

The table below, shows C# code, and equivalent Ada code.

C#	Ada
`x = 5;`	`x := 5;`
`x == 5`	`x = 5`
`x != 5`	`x /= 5`
`// comment`	`-- comment`
`int i = 2; Console.WriteLine(i);`	`i : Integer := 2; Put_Line(Integer'Image(i));`
`if (a > b) { Console.WriteLine("Condition met"); } else { Console.WriteLine("Condition not met"); }`	`if a > b then Put_Line("Condition met"); else Put_Line("Condition not met"); end if;`
`switch(i) { case 0: Console.WriteLine("zero"); break; case 1: Console.WriteLine("one"); break; case 2: Console.WriteLine("two"); break; default: Console.WriteLine("none"); }`	`case i is when 0 => Put_Line("zero"); when 1 => Put_Line("one"); when 2 => Put_Line("two"); when others => Put_Line("none"); end case;`
`for (int i=1; i<=10; ++i) { Console.WriteLine("Iteration: "); Console.WriteLine(i); Console.WriteLine(""); }`	`for i in 1 .. 10 loop Put_Line("Iteration: "); Put_Line(Integer'Image(i)); Put_Line(""); end loop;`
`while(a != b) { Console.WriteLine("Waiting"); }`	`while a /= b loop Put_Line("Waiting"); end loop;`
`do { a++; } while(a!=10);`	`loop a := a + 1; exit when a = 10; end loop;`

Packages

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:

class Person  
{
  public int publicVar;

  private int privateVar;

  void MyMethod(int param)
  {
    // do stuff
  }

  public int MultiplyBy(int param) 	
  {
    return param * 2
  }
}

And its equivalent package in Ada:

-- person.ads
package Person is
  publicVar : Integer; 	

  procedure MyMethod(Param : Integer);   
   
  function MultiplyBy(Param : Integer) return Integer; 
end Person;

-- person.adb
package body Person is 	
  privateVar : Integer;

  procedure MyMethod(Param : Integer)
  is
  begin
    -- do stuff
  end;

  function MultiplyBy(Param : Integer)
  is
    Result : Integer;
  begin
    Result := Param * 2;
    return Result;
  end;
end Person;

SPARK 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.

package Odometer
--# own Trip, Total : Integer;
is
	procedure Zero_Trip;
	--# global out Trip;
	--# derives Trip from ;
	--# post Trip = 0;

	function Read_Trip return Integer;
	--# global in Trip;

	function Read_Total return Integer;
	--# global in Total;

	procedure Inc;
	--# global in out Trip, Total;
	--# derives Trip from Trip & Total from Total;
	--# post Trip = Trip~ + 1 and Total = Total~ + 1;

end Odometer;

It is an interface for simple Odometer. There are 4 subprograms (2 procedures and 2 functions):

Zero_Trip procedure - reset Odometer to 0
Read_Trip function - returns current distance
Read_Total function - returns total distance traveled
Inc procedure- increment total and current distance by 1

Annotation global means that subprogram uses some global variable. Postfix in, out or 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 Inc variable Trip is dependent on its current value (before procedure call). Annotations pre and 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 Trip and 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 most popular IDE for SPARK Ada development is GNAT Programming Studio. There is also Eclipse plugin GNATbench.

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.

Summary

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 begin and ends with end keywords. 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.

Tags: programming