Pascal-like language with extremely strong static typing.

Ada provides extremely strong static-typing, sane object-oriented programming, built-in design-by-contract, and formal proofs via SPARK. It is primarily used in resource constrained environments where high-reliability is required.

Hello ada

To do simple text output you could write something like the following:

// hello.adb

with Ada.Text_IO; use Ada.Text_IO;

procedure Hello is
begin
   Put_Line("Hello, there");
end Hello;

To build you run:

$ gnat compile hello
$ gnat bind hello
$ gnat link hello

You can then run the program:

$ ./hello
Hello, there

Safe arrays

Ada allows arbitrary ranges to be used for array access, simplifying a lot adding and subtracting that happens in C in order to fix up array bounds. For example when writing an emulator we might have something like:

subtype Memory_Range is Integer range #0#16 .. #FFF#16;
PC: Memory_Range;
Memory: array (Memory_Range) of Integer;

Safe pointers

Pointers in Ada are called "access types". To define a pointer type you might have something like the following:

Ref: access T;
...
Obj: aliased T;
Ref := Obj'Access;

We first declare Ref to be an access type and Obj to be an aliased value of type T. This tells the compiler than we plan to take pointers to Obj. We then set Ref to point to Obj using Obj'Access to get the pointer.

You can also declare pointers that can never be null as follows:

Ref: access not null T := <Initial value>; // Non-null requires an initial value.
...
Ref := null; // * Constraint_Error at runtime *

SPARK

SPARK is a subset of the Ada language designed for the development of high-integrity software. It disables language features like dynamic dispatch for object-oriented programming that make programs hard to formally analyze. Despite being restricted, a large enough portion of Ada's features remain to make it quite comfortable to develop within.

SPARK works by analyzing the code you write based on contracts you define within the code. In normal Ada the contracts introduce runtime checks, but with SPARK the pre and post conditions are analyzed by the prover at compile time.

// chip8.ads
  
with Interfaces; use Interfaces;

package Chip8 with SPARK_Mode is

   subtype Nibble is Integer range 0 .. 15;
   --  Represents a 4-bit value

   subtype Byte is Interfaces.Unsigned_8;
   --  Represents an 8-bit byte value

   subtype Word is Interfaces.Unsigned_16;
   --  Represents a 16-bit word value

   function To_Hex_String (Value : in Nibble) return String
     with
       Post => To_Hex_String'Result'Length = 1;
   --  Return the string hexadecimal representation of the given nibble.

   function To_Hex_String (Value : in Byte) return String
     with
       Post => To_Hex_String'Result'Length = 2;
   --  Return the string hexadecimal representation of the given byte value.

   function To_Hex_String (Value : in Word) return String
     with
       Post => To_Hex_String'Result'Length = 3;
   --  Return the string hexadecimal representation of the given word value.

end Chip8;

// chip8.adb
  
package body Chip8 with SPARK_Mode is

   -------------------
   -- To_Hex_String --
   -------------------

   function To_Hex_String (Value : in Nibble) return String is
      Hex_Value_Map : array (Nibble) of String (1 .. 1) :=
        (0  => "0",
         1  => "1",
         2  => "2",
         3  => "3",
         4  => "4",
         5  => "5",
         6  => "6",
         7  => "7",
         8  => "8",
         9  => "9",
         10 => "A",
         11 => "B",
         12 => "C",
         13 => "D",
         14 => "E",
         15 => "F");
   begin
      return Hex_Value_Map (Value);
   end To_Hex_String;

   function To_Hex_String (Value : in Byte) return String is
      Result : String (1 .. 2) := "  ";
   begin
      Result (2 .. 2) := To_Hex_String (Nibble (Value and 16#0F#));

      if Value < 16#10# then
         Result (1) := '0';
      else
         Result (1 .. 1) :=
           To_Hex_String (Nibble (Shift_Right (Value, 4) and 16#0F#));
      end if;

      return Result;
   end To_Hex_String;

   function To_Hex_String (Value : in Word) return String is
      Result : String (1 .. 3) := "   ";
   begin
      if Value < 16#100# then
         Result (1) := '0';
      else
         Result (1 .. 1) :=
           To_Hex_String (Nibble (Shift_Right (Value, 8) and 16#00F#));
      end if;

      Result (2 .. 3) := To_Hex_String (Byte (Value and 16#0FF#));

      return Result;
   end To_Hex_String;
end Chip8;

The above contract enforces, for example, that the hex string returned when converting a Nibble value should always be 1 character in length. We don't need a pre-condition check the range of Nibble since that is implied by its ranged definition. We can run the SPARK prover over our implementation of this as follows:

$ gnatprove -P./chip8.gpr -j0 --level=4 --report=all
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
chip8.adb:32:26: info: length check proved
chip8.adb:32:55: info: range check proved
chip8.adb:38:12: info: length check proved
chip8.adb:38:58: info: range check proved
chip8.adb:51:12: info: length check proved
chip8.adb:51:58: info: range check proved
chip8.adb:54:26: info: length check proved
chip8.adb:54:53: info: range check proved
chip8.ads:16:16: info: postcondition proved
chip8.ads:21:16: info: postcondition proved
chip8.ads:26:16: info: postcondition proved

incoming(1): how to

• gnat community edition
• wikibook
• safe and secure - and invitation to ada 2012
• gprbuild docs

Last update on 7E4B18, edited 1 times. 1/1thh