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.
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
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;This restricts both
PCvalues and array access into
Memoryto the range specified with the compiler handling selecting an appropriately sized basic type for the range given. This also allows for compile time checks and the raising of a
Constraint_Errorat runtime if
PCoverflows during addition. Overflow issues can also be caught before runtime by running the SPARK prover.
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
to be an
aliased value of type
T. This tells the
compiler than we plan to take pointers to
Obj. We then
Ref to point to
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 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
Nibble value should always be 1 character in
length. We don't need a pre-condition check the range of
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
Last update on 7E4B18, edited 1 times. 1/1thh