Ada - język, w którym błędy mają być trudniejsze do popełnienia

Ada jest dziwnym językiem.

Nie dlatego, że jej składnia jest szczególnie egzotyczna.

Jeżeli znasz Pascala, C, Javę, Go albo nawet trochę Pythona, większość podstawowych konstrukcji zrozumiesz bardzo szybko.

Dziwne jest raczej to, czego Ada oczekuje od programisty.

W wielu popularnych językach filozofia brzmi mniej więcej:

napisz kod, a potem sprawdzimy, czy działa.

Ada bardzo często zachęca do odwrotnego podejścia:

najpierw opisz dokładnie, jakie wartości mają sens, co funkcja może dostać, co musi zwrócić i czego programowi nie wolno zrobić.

Dopiero potem pisz implementację.

To język zaprojektowany dla dużych, długo żyjących systemów, w których:

"jakoś działa"

nie jest wystarczającym standardem jakości.

Ada jest używana między innymi w domenach takich jak:

awionika,
lotnictwo,
kolej,
systemy wojskowe,
systemy czasu rzeczywistego,
kosmos,
medycyna,
systemy embedded,
oprogramowanie o wysokich wymaganiach bezpieczeństwa i niezawodności.

Ale nie jest wyłącznie językiem „do rakiet”.

Można w niej napisać:

program CLI,
serwer,
bibliotekę,
aplikację embedded,
grę,
program wielowątkowy,
narzędzie systemowe.

I oczywiście:

zgadywankę liczby od 0 do 100.

Ten artykuł pokaże Adę od podstaw aż do rzeczy, które czynią ją wyjątkową:

silne typowanie,
typy i podtypy,
zakresy,
rekordy,
pakiety,
generyki,
kontrolę reprezentacji danych,
tasking,
protected objects,
kontrakty,
SPARK,
formalną weryfikację.

Powiązane materiały TechHandbooka:

Skąd wzięła się Ada?

W latach 70. Departament Obrony Stanów Zjednoczonych miał problem.

W różnych projektach używano ogromnej liczby języków i dialektów programowania.

Każdy system mógł mieć własne:

narzędzia,
kompilatory,
biblioteki,
konwencje,
język.

Dla systemów rozwijanych i utrzymywanych przez dziesięciolecia był to koszmar.

Departament Obrony rozpoczął więc proces projektowania jednego nowego języka przeznaczonego do dużych systemów.

Wymagania były bardzo ambitne.

Język miał wspierać między innymi:

modularność,
silne typowanie,
niezawodność,
współbieżność,
systemy czasu rzeczywistego,
duże zespoły,
długotrwałe utrzymanie kodu.

Zwycięski projekt stworzył zespół kierowany przez:

Jean Ichbiah

Język nazwano:

Ada

na cześć:

Augusta Ada Lovelace

związanej z maszyną analityczną Charlesa Babbage'a i często nazywanej pierwszą programistką.

Ada nie jest skrótem

W przeciwieństwie do nazw takich jak:

BASIC
COBOL
FORTRAN

Ada nie rozwija się do żadnej dłuższej nazwy.

To po prostu imię.

Poprawny zapis:

Ada

a nie:

ADA

Wersje języka

Ada jest językiem standaryzowanym.

Najważniejsze wersje:

Ada 83

Pierwszy pełny standard.

Wprowadził między innymi:

pakiety,
generyki,
wyjątki,
tasking,
silne typowanie.

Ada 95

Bardzo ważna modernizacja.

Dodano między innymi:

programowanie obiektowe,
hierarchiczne biblioteki,
protected objects,
wiele rozszerzeń czasu rzeczywistego.

Ada 2005

Rozszerzenia między innymi dla:

OOP,
interfejsów,
systemów czasu rzeczywistego,
kontenerów.

Ada 2012

Bardzo ważna wersja z punktu widzenia współczesnej Ady.

Pojawiły się między innymi:

preconditions,
postconditions,
type invariants,
subtype predicates,
bardziej rozbudowane kontrakty.

Ada 2022

Obecna generacja standardu.

Standard Ada 2022 został opublikowany jako:

ISO/IEC 8652:2023

Nazwa:

Ada 2022

pozostała nazwą rewizji języka.

Ada to nie SPARK

To ważne rozróżnienie.

Ada

Pełny język programowania.

SPARK

Język i zestaw metod formalnej analizy oparty na podzbiorze Ady.

Można myśleć:

Ada
┌───────────────────────────────────┐
│                                   │
│        SPARK                      │
│        ┌────────────────┐         │
│        │ weryfikowalny  │         │
│        │ podzbiór       │         │
│        └────────────────┘         │
│                                   │
└───────────────────────────────────┘

SPARK ogranicza pewne konstrukcje Ady, które utrudniają matematyczne dowodzenie właściwości programu.

W zamian otrzymujemy możliwość dużo silniejszej analizy.

GNAT

Najważniejszym współczesnym kompilatorem Ady jest:

GNAT

GNAT jest częścią:

GNU Compiler Collection

czyli GCC.

To oznacza, że Ada nie jest wyłącznie językiem jednego zamkniętego kompilatora.

Można używać otwartego toolchainu GNAT FSF.

Najważniejsze narzędzia:

gcc        - zawiera frontend Ada
gnatmake   - prosty build pojedynczych projektów
gprbuild   - system budowania projektów
gnatbind   - binder Ady
gnatlink   - linker

Po co Ada ma binder?

Kompilacja Ady nie zawsze jest po prostu:

source -> object -> linker

Ada posiada dodatkowy etap:

binding

Binder analizuje między innymi:

zależności jednostek,
kolejność elaboracji pakietów,
inicjalizację programu.

Uproszczony proces:

Ada source
    |
    v
compiler
    |
    v
object files
    |
    v
binder
    |
    v
linker
    |
    v
program

gnatmake i gprbuild robią to automatycznie.

Alire

Współczesny projekt Ada bardzo wygodnie prowadzić przez:

Alire

Polecenie:

alr

Alire jest jednocześnie:

menedżerem pakietów,
katalogiem bibliotek,
menedżerem zależności,
narzędziem do tworzenia projektów,
menedżerem toolchainów.

Można go porównać do:

cargo - Rust
npm   - JavaScript
pip   - Python
opam  - OCaml

choć oczywiście szczegóły działania są inne.

Dwie sensowne drogi instalacji

Mamy dwa główne podejścia.

Droga 1 - systemowy GNAT

Dobra do:

nauki,
prostych programów,
systemów Linux,
środowisk, w których chcemy używać pakietów dystrybucji.

Droga 2 - Alire

Lepsza do:

nowych projektów,
zależności,
kontrolowania wersji kompilatora,
bibliotek,
SPARK,
projektów przenośnych.

W tym artykule poznamy obie.

Instalacja - Linux / Debian

Najprostsza instalacja systemowa

Na Debianie:

sudo apt update
sudo apt install gnat gprbuild

Sprawdzenie:

gnat --version

albo:

gnatmake --version

oraz:

gprbuild --version

W zależności od wersji Debiana pakiet może zawierać określoną wersję GNAT GCC.

Instalacja Alire - Linux

Alire publikuje archiwum z programem:

alr

Pobieramy aktualne wydanie ze strony:

https://alire.ada.dev/

Po rozpakowaniu dodajemy katalog bin do PATH.

Przykład:

export PATH="$HOME/tools/alire/bin:$PATH"

Na stałe można dodać wpis do:

~/.profile

lub konfiguracji używanego shella.

Sprawdzenie:

alr --version

Przy pierwszym projekcie Alire może zaproponować wybór kompilatora GNAT i GPRbuild.

Linux ARM

Oficjalne gotowe toolchainy Alire są najwygodniejsze na wspieranych platformach x86-64.

Jeżeli pracujesz na Linux ARM/AArch64, możesz używać:

systemowego GNAT,
kompilatora zbudowanego dla tej platformy,
Alire z systemowym toolchainem.

To ważne szczególnie dla:

Raspberry Pi
ARM servers

Instalacja - Windows

Najwygodniejszą współczesną drogą jest Alire.

Strona:

https://alire.ada.dev/

Dla Windows dostępny jest instalator.

Instalator dodaje alr do środowiska.

Sprawdzenie w PowerShell:

alr --version

Przy pierwszym użyciu Alire może zaproponować instalację:

MSYS2

Jest to sensowne, ponieważ część bibliotek i narzędzi potrzebuje programów typowych dla środowiska Unix:

git
make
curl

Alire potrafi wykorzystać własne środowisko MSYS2.

Alternatywa Windows - MSYS2

Ada jest również dostępna bezpośrednio w ekosystemie MSYS2.

Można używać pakietów GCC Ada i GPRbuild.

To opcja dla osób, które już pracują w MSYS2 i chcą mieć jeden spójny toolchain MinGW.

Do zwykłego nowego projektu Ada wygodniejszy jest jednak Alire.

Instalacja - macOS

Alire udostępnia archiwum dla macOS.

Po rozpakowaniu:

export PATH="/ścieżka/do/alire/bin:$PATH"

macOS może oznaczyć pobrany plik atrybutem quarantine.

W takim przypadku oficjalna instrukcja Alire pokazuje usunięcie atrybutu:

xattr -d com.apple.quarantine bin/alr

Sprawdzenie:

alr --version

macOS i Apple Silicon

Tu trzeba uważać.

Gotowe community toolchainy Alire są przede wszystkim publikowane dla:

macOS x86-64

Na Apple Silicon:

M1
M2
M3
M4
...

może być potrzebny:

community toolchain dla AArch64,
systemowy/native GNAT,
kompilacja narzędzi ze źródeł.

Dlatego na macOS ARM warto sprawdzić aktualną dokumentację konkretnego wydania Alire.

Pierwszy program - Hello World

Utwórz:

hello.adb

Kod:

with Ada.Text_IO;

procedure Hello is
begin
   Ada.Text_IO.Put_Line ("Hello from Ada!");
end Hello;

Kompilacja:

gnatmake hello.adb

Uruchomienie Linux/macOS:

./hello

Windows:

.\hello.exe

`with`

Linia:

with Ada.Text_IO;

oznacza, że nasza jednostka zależy od:

Ada.Text_IO

Można to porównać bardzo luźno do:

import
include
use module

ale model bibliotek Ady ma własne zasady.

Pełna nazwa

Bez use piszemy:

Ada.Text_IO.Put_Line ("Hello");

To bardzo czytelne.

Od razu wiadomo, skąd pochodzi Put_Line.

`use`

Możemy napisać:

with Ada.Text_IO;
use Ada.Text_IO;

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

use sprawia, że nazwy z pakietu są bezpośrednio widoczne.

To wygodne, ale w dużych programach może zwiększać ryzyko konfliktów nazw.

Dlatego często zobaczysz kod bez globalnego:

use

Struktura procedury

Najprostszy program:

procedure Main is
begin
   null;
end Main;

Mamy:

procedure Main is

część deklaracyjną,

begin

część wykonywalną,

end Main;

koniec jednostki.

`null`

Instrukcja:

null;

oznacza:

celowo nic nie rób.

To odpowiednik pustej operacji.

Przydaje się np.:

if Something then
   null;
end if;

Średniki

Ada używa średników:

X := 10;
Put_Line ("Hello");

Ale struktury kończą się słownie:

end if;
end loop;
end Main;

To bardzo charakterystyczne.

Komentarze

Komentarz:

-- To jest komentarz

Nie ma klasycznego blokowego:

/* ... */

Standardowa Ada używa komentarza od:

--

do końca linii.

Ada jest case-insensitive

Te identyfikatory oznaczają to samo:

Counter
COUNTER
counter
CoUnTeR

W praktyce kod pisze się według konwencji:

This_Is_A_Name

a słowa kluczowe często:

procedure
begin
end

Przypisanie

Ada używa:

:=

Przykład:

X := 10;

Natomiast:

oznacza porównanie.

if X = 10 then
   ...
end if;

To eliminuje klasyczny błąd z języków rodziny C:

if (x = 10)

zamiast:

if (x == 10)

Deklarowanie zmiennych

Age : Integer := 46;

Schemat:

Nazwa : Typ := Wartość;

Możemy zadeklarować bez inicjalizacji:

Age : Integer;

ale w bezpiecznym kodzie warto bardzo świadomie podchodzić do inicjalizacji.

Stałe

Pi : constant Float := 3.14159;

Po inicjalizacji nie można zmienić wartości:

Pi := 4.0;

To błąd.

Podstawowe typy

Typowe predefiniowane typy:

Integer
Float
Boolean
Character
String
Natural
Positive

Przykład:

Age     : Integer := 46;
Height  : Float := 1.80;
Enabled : Boolean := True;
Letter  : Character := 'A';
Name    : String := "Ada";

Natural i Positive

Ada ma predefiniowane podtypy:

Natural

czyli liczby całkowite:

>= 0

oraz:

Positive

czyli:

> 0

Przykład:

Count : Natural := 0;
Index : Positive := 1;

Już na poziomie deklaracji mówimy coś o sensie danych.

Typ to nie tylko rozmiar

To jedna z najważniejszych idei Ady. W C:

typedef float Meters;
typedef float Seconds;

obie nazwy są w praktyce aliasami tego samego typu.

Ada pozwala stworzyć naprawdę różne typy:

type Meters is new Float;
type Seconds is new Float;

Teraz:

Distance : Meters := 10.0;
Time     : Seconds := 5.0;

Nie możemy bezmyślnie zrobić:

Distance := Time;

ani:

Distance + Time

tylko dlatego, że oba są reprezentowane jako liczby zmiennoprzecinkowe.

Dlaczego to jest świetne?

Wyobraź sobie:

meters
feet
seconds
milliseconds
volts
amps
degrees
radians

Dla CPU wszystko może być liczbą.

Dla programu:

10 metrów + 5 sekund

nie ma sensu.

Ada pozwala zakodować tę wiedzę w systemie typów.

Jawne konwersje

Jeżeli naprawdę chcesz zamienić jeden typ na drugi, robisz to jawnie.

type Celsius is new Float;
type Fahrenheit is new Float;

C : Celsius := 20.0;
F : Fahrenheit;

F := Fahrenheit (C);

Nie oznacza to oczywiście automatycznego przeliczenia skali temperatury.

To tylko jawna konwersja reprezentacji.

Właściwe przeliczenie trzeba napisać samemu.

Typ wyliczeniowy

type Traffic_Light is
  (Red,
   Yellow,
   Green);

Zmienna:

Light : Traffic_Light := Red;

Nie przechowujemy magicznej liczby:

0
1
2

Program operuje domenowymi wartościami.

`case`

Typy wyliczeniowe świetnie współpracują z:

case

Przykład:

case Light is
   when Red =>
      Stop;

   when Yellow =>
      Prepare;

   when Green =>
      Go;
end case;

Kompilator wymaga obsłużenia wszystkich możliwości.

To bardzo cenna właściwość.

Jeżeli później dodamy:

Blinking_Yellow

kompilator może wskazać miejsca, które trzeba zaktualizować.

Podtypy

Typ:

Integer

jest ogromnym zbiorem wartości.

Czasem domena dopuszcza tylko fragment.

Przykład:

subtype Percentage is Integer range 0 .. 100;

Teraz:

Progress : Percentage := 75;

ma jasno opisane ograniczenie.

Podtyp nie jest nowym typem

To ważne.

subtype Percentage is Integer range 0 .. 100;

tworzy ograniczony widok typu Integer.

Natomiast:

type Percentage is range 0 .. 100;

tworzy nowy typ całkowity.

To dwa różne mechanizmy.

Sprawdzanie zakresów

Przykład:

subtype Percentage is Integer range 0 .. 100;

P : Percentage;
X : Integer := 120;

begin
   P := X;

Jeżeli podczas działania wartość nie mieści się w zakresie, zostanie wykonany runtime check.

Może zostać zgłoszony:

Constraint_Error

Ada domyślnie wykonuje wiele takich kontroli.

Błąd wykryty wcześniej

Jeżeli kompilator może udowodnić już podczas kompilacji, że statyczna wartość łamie ograniczenie:

P : Percentage := 150;

może zgłosić problem jeszcze przed uruchomieniem programu.

To dokładnie filozofia Ady:

wykryj błąd tak wcześnie, jak się da

Zakres jako część modelu

Zamiast:

Temperature : Integer;

możemy napisać:

subtype Engine_Temperature is Integer range -40 .. 150;

Temperature : Engine_Temperature;

Kod sam dokumentuje:

legalne temperatury w tym modelu to -40..150.

To więcej niż komentarz.

Kompilator i runtime mogą wykorzystać tę informację.

Typ modularny

Ada posiada typy modularne.

Przykład 8-bitowej wartości:

type Byte is mod 2 ** 8;

Zakres:

0..255

Po przepełnieniu wynik zawija się modulo 256.

Przykład:

B : Byte := 255;

B := B + 1;

wynik:

To bardzo przydatne w:

embedded,
kryptografii,
pracy bitowej,
protokołach.

Operacje bitowe na typach modularnych

Możemy używać operacji:

and
or
xor
not

Przykład:

type Byte is mod 2 ** 8;

A : Byte := 16#F0#;
B : Byte := 16#0F#;
C : Byte;

C := A xor B;

Wynik:

16#FF#

Zapis liczb w innych podstawach

Ada ma bardzo czytelny zapis liczb.

Hex:

16#FF#

Binarnie:

2#1111_0000#

Ósemkowo:

8#377#

Podkreślenia poprawiają czytelność:

1_000_000

Floating point

Możemy definiować własne typy zmiennoprzecinkowe.

type Real is digits 12;

digits określa wymaganą precyzję dziesiętną.

To inny model niż bezpośrednie:

float32
float64

znane z wielu języków.

Fixed point

Ada ma natywne typy fixed-point.

Przykład:

type Money is delta 0.01 digits 12;

Taki typ jest przydatny, gdy chcemy kontrolować krok reprezentacji.

W finansach nie zawsze chcemy polegać na typowym floating point.

Typy fizyczne? Nie bezpośrednio, ale...

Ada nie posiada w standardzie automatycznego systemu jednostek SI.

Ale silne typowanie pozwala bardzo skutecznie tworzyć osobne typy:

type Meters      is new Float;
type Meters_Per_Second is new Float;
type Seconds     is new Float;

i definiować tylko operacje, które mają sens.

Atrybuty

Ada ma bardzo potężny mechanizm:

attributes

Zapisywany apostrofem:

Type'Attribute

Przykłady:

Integer'First
Integer'Last

zwracają granice typu.

`'First` i `'Last`

subtype Score is Integer range 0 .. 100;

Możemy użyć:

Score'First

czyli:

oraz:

Score'Last

czyli:

Kod nie musi powtarzać magicznych wartości.

`'Range`

Dla tablicy:

for I in Values'Range loop
   ...
end loop;

Zamiast:

for I in 1 .. 100 loop

program automatycznie dostosuje się do rzeczywistego zakresu tablicy.

To jeden z najprzyjemniejszych elementów Ady.

`'Length`

Values'Length

zwraca długość tablicy.

`'Image`

Integer'Image (42)

tworzy tekstową reprezentację wartości.

Przykład:

Put_Line (Integer'Image (42));

W nowych wersjach Ady mechanizm obrazowania został mocno rozbudowany.

`'Value`

Odwrotność:

Integer'Value ("42")

zwraca liczbę:

Jeżeli tekst nie reprezentuje poprawnej wartości, może zostać zgłoszony wyjątek.

Instrukcja `if`

if Temperature > 100 then
   Put_Line ("Too hot");
end if;

`elsif`

Ada używa:

elsif

nie:

else if
elseif
elif

Przykład:

if X < 0 then
   Put_Line ("Negative");

elsif X = 0 then
   Put_Line ("Zero");

else
   Put_Line ("Positive");
end if;

Boolean

Operatory logiczne:

and
or
xor
not

Ada posiada też:

and then
or else

które wykonują short-circuit evaluation.

Przykład:

if Ptr /= null and then Ptr.all > 0 then
   ...
end if;

Drugi warunek nie zostanie wykonany, jeżeli pierwszy jest fałszywy.

Pętla nieskończona

loop
   Do_Something;
end loop;

`exit`

loop
   exit when Finished;
   Work;
end loop;

Bardzo czytelny zapis.

`while`

while Count > 0 loop
   Count := Count - 1;
end loop;

`for`

for I in 1 .. 10 loop
   Put_Line (Integer'Image (I));
end loop;

Zmienna I jest tworzona automatycznie.

Nie deklarujemy jej wcześniej.

`reverse`

for I in reverse 1 .. 10 loop
   ...
end loop;

Wykonuje iterację w odwrotnej kolejności.

Pętla po tablicy

for I in Values'Range loop
   Values (I) := 0;
end loop;

Nie musimy znać indeksu początkowego.

To ważne, bo Ada nie wymaga, aby tablica zaczynała się od:

ani nawet:

Tablice z własnym indeksem

type Day is
  (Monday,
   Tuesday,
   Wednesday,
   Thursday,
   Friday,
   Saturday,
   Sunday);

type Temperatures is array (Day) of Float;

Teraz:

T : Temperatures;

T (Monday) := 20.0;
T (Friday) := 25.0;

Indeksem jest:

Day

a nie liczba.

To bardzo Ada.

Tablice o nieustalonym rozmiarze

Możemy zadeklarować typ:

type Integer_Array is array (Positive range <>) of Integer;

<> oznacza:

zakres zostanie określony później.

Potem:

A : Integer_Array (1 .. 10);
B : Integer_Array (100 .. 200);

To ten sam typ tablicy z różnymi bounds.

Tablice wielowymiarowe

type Matrix is
  array (Positive range <>,
         Positive range <>) of Float;

Przykład:

M : Matrix (1 .. 3, 1 .. 3);

Dostęp:

M (2, 3)

String jest tablicą

Standardowy:

String

jest tablicą znaków.

Przykład:

Name : String (1 .. 5) := "Ada!!";

I tu pojawia się ważna cecha.

Standardowy String ma określony rozmiar.

Pułapka String

Name : String := "Ada";

tworzy string długości:

Nie możesz potem zrobić po prostu:

Name := "Ada Lovelace";

bo nowy tekst ma inną długość.

To częste zaskoczenie dla ludzi przychodzących z Pythona.

Unbounded_String

Do dynamicznych tekstów służy między innymi:

Ada.Strings.Unbounded

Przykład:

with Ada.Strings.Unbounded;

procedure Example is
   use Ada.Strings.Unbounded;

   Name : Unbounded_String :=
     To_Unbounded_String ("Ada");

begin
   Name := Name & " Lovelace";
end Example;

Rekordy

Odpowiednik struktury danych:

type Point is record
   X : Float;
   Y : Float;
end record;

Obiekt:

P : Point :=
  (X => 10.0,
   Y => 20.0);

Dostęp:

P.X
P.Y

Named aggregates

Ada bardzo lubi jawne nazwy pól.

P :=
  (X => 10.0,
   Y => 20.0);

To czytelniejsze niż poleganie wyłącznie na kolejności:

(10.0, 20.0)

Przy dużych rekordach znacząco redukuje ryzyko pomyłki.

`others`

Możemy ustawić pozostałe pola:

Config :=
  (Enabled => True,
   others  => <>);

Dokładne znaczenie <> zależy od kontekstu i wartości domyślnych.

Discriminated records

Ada pozwala tworzyć rekordy, których struktura zależy od discriminant.

Przykład:

type Shape_Kind is
  (Circle,
   Rectangle);

type Shape
  (Kind : Shape_Kind := Circle)
is record
   case Kind is
      when Circle =>
         Radius : Float := 0.0;

      when Rectangle =>
         Width  : Float := 0.0;
         Height : Float := 0.0;
   end case;
end record;

To bezpieczniejszy model wariantów danych niż ręczne uniony znane z C.

Funkcja

function Add
  (A : Integer;
   B : Integer)
   return Integer
is
begin
   return A + B;
end Add;

Użycie:

Result := Add (10, 20);

Procedura

Procedura nie musi zwracać wartości.

procedure Greet (Name : String) is
begin
   Put_Line ("Hello " & Name);
end Greet;

Wywołanie:

Greet ("Ada");

Parametry `in`

Domyślny tryb parametrów skalarnych to:

in

Przykład:

procedure Show (X : in Integer);

Procedura traktuje parametr jako wejście.

`out`

procedure Get_Result
  (Result : out Integer);

Parametr służy do przekazania wyniku na zewnątrz.

`in out`

procedure Increment
  (X : in out Integer)
is
begin
   X := X + 1;
end Increment;

Wywołanie:

Value : Integer := 10;

Increment (Value);

Po operacji:

Value = 11

Czytelność wywołań

Możemy wywołać:

Move
  (X     => 10,
   Y     => 20,
   Speed => 5);

zamiast:

Move (10, 20, 5);

Named parameters są bardzo przydatne przy funkcjach z wieloma argumentami tego samego typu.

Wartości domyślne parametrów

procedure Log
  (Message : String;
   Level   : Natural := 1);

Możemy wywołać:

Log ("Started");

lub:

Log
  (Message => "Failed",
   Level   => 3);

Przeciążanie

Ada obsługuje overload.

procedure Print (X : Integer);
procedure Print (X : Float);
procedure Print (X : String);

Kompilator wybiera wersję na podstawie typów.

Operator jako funkcja

Operatory również mogą być przeciążane.

Możemy zdefiniować działanie:

"+"

dla własnych typów.

To przydatne w typach domenowych:

Vector
Matrix
Distance
Money

Packages

Jednym z fundamentów dużych programów Ada są:

packages

Pakiet zwykle ma:

specification
body

Plik specyfikacji:

.ads

Plik implementacji:

.adb

Specification

calculator.ads:

package Calculator is

   function Add
     (A : Integer;
      B : Integer)
      return Integer;

end Calculator;

To publiczny interfejs.

Body

calculator.adb:

package body Calculator is

   function Add
     (A : Integer;
      B : Integer)
      return Integer
   is
   begin
      return A + B;
   end Add;

end Calculator;

Program używający pakietu

main.adb:

with Ada.Text_IO;
with Calculator;

procedure Main is
   Result : Integer;
begin
   Result := Calculator.Add (10, 20);

   Ada.Text_IO.Put_Line
     (Integer'Image (Result));
end Main;

Kompilator widzi zależność przez:

with Calculator;

Specyfikacja jako kontrakt

To ważny element filozofii Ady.

Klient pakietu powinien potrzebować przede wszystkim:

.ads

a nie implementacji:

.adb

Specyfikacja mówi:

jakie typy istnieją,
jakie operacje są dostępne,
jakie są parametry,
jakie są kontrakty.

Implementacja może się zmieniać bez zmiany użytkowników pakietu.

Private types

Możemy ukryć implementację typu.

accounts.ads:

package Accounts is

   type Account is private;

   function Balance
     (A : Account)
      return Integer;

private

   type Account is record
      Current_Balance : Integer := 0;
   end record;

end Accounts;

Kod poza pakietem wie, że istnieje:

Account

ale nie zna jego wewnętrznej reprezentacji.

Limited private

Jeszcze silniejsze ograniczenie:

type Device is limited private;

Klient nie może swobodnie kopiować wartości.

To przydatne dla obiektów reprezentujących:

uchwyty,
urządzenia,
mutexy,
zasoby systemowe.

Child packages

Ada ma hierarchiczne nazwy bibliotek.

Przykład:

Network
Network.HTTP
Network.HTTP.Client
Network.HTTP.Server

To naturalny sposób organizowania dużych systemów.

Generyki

Ada posiada potężny system:

generics

Przykład generycznej procedury swap.

generic
   type T is private;

procedure Generic_Swap
  (A : in out T;
   B : in out T);

Body:

procedure Generic_Swap
  (A : in out T;
   B : in out T)
is
   Temp : T := A;
begin
   A := B;
   B := Temp;
end Generic_Swap;

Instancja:

procedure Swap_Integer is
  new Generic_Swap (Integer);

Teraz mamy typowaną wersję dla:

Integer

Kontenery

Standardowa biblioteka Ady posiada kontenery.

Przykłady:

Ada.Containers.Vectors
Ada.Containers.Doubly_Linked_Lists
Ada.Containers.Hashed_Maps
Ada.Containers.Ordered_Maps
Ada.Containers.Hashed_Sets
Ada.Containers.Ordered_Sets

Wiele z nich jest generycznych.

Vector

Przykład:

with Ada.Containers.Vectors;

procedure Example is

   package Integer_Vectors is
     new Ada.Containers.Vectors
       (Index_Type   => Natural,
        Element_Type => Integer);

   V : Integer_Vectors.Vector;

begin
   V.Append (10);
   V.Append (20);
   V.Append (30);
end Example;

Access types

Ada posiada odpowiednik wskaźników:

access types

Przykład:

type Integer_Access is
  access all Integer;

X : aliased Integer := 10;
P : Integer_Access := X'Access;

Dostęp do wartości:

P.all

`null`

Access value może być:

null

Przed dereferencją należy mieć pewność, że wskaźnik jest poprawny.

Dlaczego Ada nie traktuje wskaźników lekko?

Wskaźniki są jedną z głównych przyczyn błędów w językach niskopoziomowych.

Ada daje do nich dostęp, ale:

wymaga jawnych typów access,
wykonuje kontrole,
mocno rozróżnia typy,
posiada zasady accessibility,
pozwala ograniczyć ich użycie.

W kodzie high-integrity często świadomie ogranicza się dynamiczną alokację.

Unchecked_Access i Unsafe World

Ada pozwala ominąć część zabezpieczeń.

Istnieją mechanizmy w rodzaju:

Unchecked_Access
Unchecked_Conversion
Unchecked_Deallocation

Słowo:

Unchecked

jest bardzo uczciwe.

Język mówi:

możesz to zrobić, ale właśnie wychodzisz poza normalny model bezpieczeństwa.

Wyjątki

Ada posiada wbudowany system wyjątków.

Przykład:

begin
   Dangerous_Operation;

exception
   when Constraint_Error =>
      Put_Line ("Constraint failed");

   when others =>
      Put_Line ("Unknown error");
end;

Standardowe wyjątki

Typowe:

Constraint_Error
Program_Error
Storage_Error
Tasking_Error

Własny wyjątek

Invalid_Temperature : exception;

Rzucenie:

raise Invalid_Temperature;

Możemy również dodać komunikat:

raise Invalid_Temperature
  with "Temperature outside allowed range";

Constraint_Error nie jest tylko błędem

Przykład:

subtype Percentage is Integer range 0 .. 100;

Próba przypisania wartości:

może zakończyć się:

Constraint_Error

To celowe zabezpieczenie semantyki programu.

Język nie chce udawać, że:

150%

jest poprawną wartością typu, który zdefiniowaliśmy jako:

0..100

Runtime checks

Ada może sprawdzać podczas działania między innymi:

zakresy,
indeksy tablic,
dzielenie przez zero,
overflow w określonych sytuacjach,
poprawność access values,
kontrakty.

To zwiększa szansę wykrycia błędu blisko miejsca, gdzie naprawdę powstał.

Array bounds

W C:

int a[10];
a[100] = 5;

może prowadzić do undefined behavior.

Ada:

A : array (1 .. 10) of Integer;

A (100) := 5;

jest naruszeniem zakresu.

Runtime może zgłosić:

Constraint_Error

Design by Contract

Jedna z najciekawszych cech współczesnej Ady.

Możemy opisać:

co musi być prawdą przed wywołaniem

co ma być prawdą po wykonaniu

Precondition

procedure Withdraw
  (Balance : in out Natural;
   Amount  : Positive)
with
  Pre => Amount <= Balance;

To mówi:

Withdraw wolno wywołać tylko wtedy, gdy Amount nie przekracza Balance.

Postcondition

procedure Withdraw
  (Balance : in out Natural;
   Amount  : Positive)
with
  Pre  => Amount <= Balance,
  Post => Balance =
            Balance'Old - Amount;

Balance'Old oznacza:

wartość Balance sprzed wywołania

Kontrakt mówi więc:

po wykonaniu saldo musi być równe stare saldo minus wypłata.

Implementacja

procedure Withdraw
  (Balance : in out Natural;
   Amount  : Positive)
with
  Pre  => Amount <= Balance,
  Post => Balance =
            Balance'Old - Amount
is
begin
   Balance := Balance - Amount;
end Withdraw;

Interfejs i zachowanie są powiązane formalnie.

Włączenie assertion checks w GNAT

Przy klasycznej kompilacji GNAT można włączyć sprawdzanie assertions opcją:

-gnata

Przykład:

gnatmake -gnata main.adb

Wtedy preconditions, postconditions i assertions mogą być sprawdzane podczas działania.

`pragma Assert`

pragma Assert (Balance >= 0);

Jeżeli warunek nie jest spełniony, assertion zgłasza problem.

Assertions świetnie dokumentują założenia programu.

Subtype predicates

Możemy opisać dodatkową własność wartości.

subtype Even_Integer is Integer
with
  Dynamic_Predicate =>
    Even_Integer mod 2 = 0;

Obiekt:

X : Even_Integer;

ma reprezentować tylko liczby parzyste.

Static_Predicate

Dla warunków możliwych do statycznej analizy istnieje:

Static_Predicate

Przykład:

subtype Day_Number is Integer
  with Static_Predicate =>
    Day_Number in 1 .. 31;

W praktyce prosty zakres lepiej oczywiście zapisać zwykłym:

range

Predicates są ciekawsze przy bardziej złożonych zbiorach wartości.

Type invariants

Typ prywatny może definiować właściwość, która ma pozostać prawdziwa.

Idea:

Balance nigdy nie jest ujemne
Start <= End
Lista zachowuje spójność

Invariant jest bardziej formalnym odpowiednikiem:

obiekt tego typu zawsze powinien być poprawny.

Dlaczego kontrakt jest lepszy od komentarza?

Komentarz:

-- Amount should not exceed Balance

kompilator ignoruje.

Kontrakt:

with Pre => Amount <= Balance

może być:

czytany przez człowieka,
sprawdzany runtime,
analizowany statycznie,
formalnie dowodzony przez GNATprove.

To ogromna różnica.

SPARK

Teraz dochodzimy do rzeczy, z której Ada jest szczególnie znana.

SPARK jest podzbiorem Ady oraz zestawem narzędzi umożliwiających formalną analizę kodu.

Główne narzędzie:

GNATprove

Co znaczy „formalna weryfikacja”?

Test mówi:

dla tych danych program zachował się poprawnie

Formalny dowód próbuje wykazać:

dla wszystkich wartości spełniających założenia określona właściwość jest prawdziwa

To nie jest magiczne:

prove program is perfect

Dowodzimy konkretnych właściwości.

Przykład

procedure Increment
  (X : in out Integer)
with
  Pre  => X < Integer'Last,
  Post => X = X'Old + 1;

Precondition mówi:

X nie może być już maksymalnym Integer

bo:

X + 1

spowodowałoby overflow.

Postcondition mówi:

wynik jest dokładnie o 1 większy

GNATprove

GNATprove może analizować:

przepływ danych,
inicjalizację,
możliwość runtime errors,
preconditions,
postconditions,
assertions,
zależności danych.

Przykładowe polecenie:

gnatprove

W prawdziwym projekcie zwykle uruchamiamy je w kontekście pliku projektu GPR.

Flow analysis

SPARK analizuje między innymi:

czy zmienna została zainicjalizowana,
czy przypisanie jest używane,
jakie dane funkcja czyta,
jakie dane modyfikuje.

To może znaleźć problemy bez wykonywania programu.

Absence of Run-Time Errors

Jednym z bardzo ważnych celów proof jest:

AoRTE

czyli:

Absence of Run-Time Errors

Możemy próbować dowieść, że kod nie spowoduje np.:

dzielenia przez zero,
wyjścia poza tablicę,
overflow,
naruszenia zakresu.

Test kontra proof

Załóżmy:

function Divide
  (A : Integer;
   B : Integer)
   return Integer
is
begin
   return A / B;
end Divide;

Testy mogą sprawdzić:

10 / 2
20 / 5
0 / 1

Ale mogą nie sprawdzić:

B = 0

Proof spróbuje wykazać, czy dzielenie jest bezpieczne dla wszystkich dopuszczalnych wejść.

Dodajemy precondition

function Divide  (A : Integer;
   B : Integer)
   return Integer
with
  Pre => B /= 0;

Teraz wymaganie jest jawne.

GNATprove może analizować każde miejsce wywołania i sprawdzać:

czy caller potrafi udowodnić, że B nie jest zerem?

To zmienia sposób projektowania API

Zamiast pisać defensywnie wszędzie:

if bad input
   return error

możemy określić:

legalne warunki użycia funkcji

i wymagać ich od klienta.

Nie znaczy to, że każda aplikacja powinna porzucić obsługę błędnego wejścia użytkownika.

Kontrakty opisują granice między komponentami i odpowiedzialności.

Instalacja GNATprove przez Alire

W projekcie Alire możemy dodać:

alr with gnatprove

Alire pobierze właściwe narzędzie, jeżeli dostępny jest build dla platformy.

Potem można wykonać narzędzie w środowisku projektu.

Przykład:

alr exec -- gnatprove

`SPARK_Mode`

Kod może jawnie deklarować użycie SPARK.

Przykład:

package Math
with
  SPARK_Mode => On
is
   ...
end Math;

Możemy też kontrolować SPARK_Mode na poziomie różnych jednostek.

Pozwala to mieszać:

pełną Adę
+
weryfikowany kod SPARK

w jednym systemie.

Nie wszystko musi być SPARK

To bardzo praktyczne.

Przykładowy system może mieć:

UI          - Ada
network     - Ada
driver      - Ada
core logic  - SPARK

Najbardziej krytyczna część otrzymuje silniejsze gwarancje.

Nie trzeba formalnie dowodzić całego świata.

Tasking

Ada posiada współbieżność jako część języka.

Nie jako zewnętrzną bibliotekę.

Podstawowa jednostka:

task

Najprostszy task

with Ada.Text_IO;
use Ada.Text_IO;

procedure Demo is

   task Worker;

   task body Worker is
   begin
      Put_Line ("Worker");
   end Worker;

begin
   Put_Line ("Main");
end Demo;

Worker może wykonywać się współbieżnie z kodem głównym.

Dlaczego to było wyjątkowe?

Ada 83 już posiadała natywny model współbieżności.

W epoce, gdy wiele języków traktowało concurrency jako bibliotekę lub systemowe rozszerzenie, Ada miała:

tasking

w specyfikacji języka.

Rendezvous

Tasks mogą komunikować się przez:

entries

Przykład ideowy:

task Server is
   entry Send (Value : Integer);
end Server;

Klient:

Server.Send (42);

Task może zaakceptować:

accept Send
  (Value : Integer)
do
   ...
end Send;

To synchronizowany rendezvous.

Protected objects

Do synchronizacji współdzielonych danych Ada posiada:

protected objects

To bardzo ważny mechanizm.

Przykład:

protected Counter is

   procedure Increment;
   function Value return Natural;

private

   Count : Natural := 0;

end Counter;

Body:

protected body Counter is

   procedure Increment is
   begin
      Count := Count + 1;
   end Increment;

   function Value return Natural is
   begin
      return Count;
   end Value;

end Counter;

Ada zapewnia odpowiednią synchronizację dostępu.

Dlaczego nie zwykły mutex?

Możesz myśleć o protected object jako o:

dane + dozwolone operacje + synchronizacja

w jednym językowym mechanizmie.

To ogranicza możliwość przypadkowego używania locka w niewłaściwy sposób.

Real-time

Ada ma rozbudowane mechanizmy dla systemów czasu rzeczywistego.

Pakiet:

Ada.Real_Time

udostępnia między innymi monotoniczny zegar odpowiedni do planowania czasowego.

Przykład ideowy:

delay until Next_Time;

zamiast:

śpij mniej więcej 10 ms

To ważne przy cyklicznych zadaniach.

Ravenscar

Ada posiada profil:

Ravenscar

ograniczający tasking do podzbioru łatwiejszego do analizy w systemach real-time i high-integrity.

Ada 2022 posiada również bardziej elastyczny profil:

Jorvik

Idea jest bardzo Ada:

ogranicz część języka, aby uzyskać bardziej przewidywalny system.

Representation clauses

Ada pozwala bardzo precyzyjnie kontrolować fizyczny układ danych.

To niezwykle ważne w:

embedded,
protokołach,
sterownikach,
rejestrach sprzętowych.

Rozmiar typu

Przykład:

type Byte is mod 2 ** 8;

for Byte'Size use 8;

Mówimy kompilatorowi, że reprezentacja ma mieć 8 bitów.

Record representation

Przykład:

type Device_Register is record
   Enabled : Boolean;
   Ready   : Boolean;
   Error   : Boolean;
end record;

Możemy zdefiniować pozycje bitów:

for Device_Register use record
   Enabled at 0 range 0 .. 0;
   Ready   at 0 range 1 .. 1;
   Error   at 0 range 2 .. 2;
end record;

To bardzo mocne przy pracy ze sprzętem.

Memory-mapped I/O

W embedded urządzenie może mieć rejestr pod konkretnym adresem.

Ada pozwala kontrolować:

typ,
adres,
volatile,
reprezentację.

Dzięki temu możemy pracować blisko sprzętu bez rezygnacji z systemu typów.

`Volatile`

Jeżeli wartość może zmieniać się poza kontrolą programu:

hardware register
DMA
interrupt

należy poinformować kompilator.

Ada posiada aspekt:

Volatile

Przykład:

Status : Interfaces.Unsigned_32
with
  Volatile;

`Atomic`

Ada posiada również mechanizm:

Atomic

do określania atomowego dostępu do obiektów, jeśli implementacja to wspiera zgodnie z regułami języka.

Import C

Ada może współpracować z C.

Przykład:

procedure C_Function
with
  Import,
  Convention    => C,
  External_Name => "c_function";

To mówi:

implementacja tej procedury znajduje się poza Adą i używa konwencji C.

Export do C

Możemy też wystawić funkcję Ada dla kodu C:

procedure Ada_Function
with
  Export,
  Convention    => C,
  External_Name => "ada_function";

To ważne w projektach mieszanych.

`Interfaces.C`

Standardowa biblioteka zawiera:

Interfaces.C

z typami odpowiadającymi typom języka C.

Na przykład:

Interfaces.C.int
Interfaces.C.char
Interfaces.C.double

To dużo bezpieczniejsze niż zgadywanie rozmiarów.

Ada i assembler

Ada może również współpracować z kodem niskopoziomowym.

Typowy system embedded może wyglądać:

Ada/SPARK
    |
    +---- C library
    |
    +---- startup assembler
    |
    +---- hardware registers

Ada nie próbuje udawać, że sprzęt nie istnieje.

Próbuje pozwolić pracować z nim w bardziej kontrolowany sposób.

Zobacz:

Assembler od podstaw

Ada i C - najważniejsza różnica filozofii

C często mówi:

programista wie, co robi.

Ada częściej mówi:

niech programista opisze, co wolno zrobić, a kompilator i runtime pomogą tego pilnować.

int temperature;

Ada:

subtype Engine_Temperature is
  Integer range -40 .. 150;

Temperature : Engine_Temperature;

To pokazuje różnicę bardzo dobrze.

Ada i Rust

Ada i Rust rozwiązują część podobnych problemów, ale ich filozofie są inne.

Rust bardzo mocno skupia się na:

ownership,
borrowing,
bezpieczeństwie pamięci,
concurrency safety.

Ada bardzo mocno skupia się na:

semantyce typów,
zakresach,
kontraktach,
runtime checks,
real-time,
high-integrity,
formalnej weryfikacji przez SPARK.

Nie ma sensu pytać:

który jest „lepszy”?

To różne narzędzia wyrosłe w innych epokach i z innych problemów.

Ada i Go

Go mówi mniej więcej:

język powinien być mały i prosty.

Ada mówi:

język powinien pozwolić dokładnie opisać model systemu i jego ograniczenia.

Go ma mało konstrukcji.

Ada ma ich dużo.

Obie filozofie mogą prowadzić do czytelnego kodu, ale inną drogą.

Ada i Pascal

Składniowo Ada odziedziczyła sporo ducha świata ALGOL/Pascal.

Widać:

begin
end
procedure
function
record

Ale Ada jest znacznie większym i bardziej przemysłowym językiem niż klasyczny Pascal.

Ada i Python

Python:

x = 10

Ada:

X : Integer := 10;

Python pozwala bardzo szybko eksperymentować.

Ada wymaga wcześniej powiedzieć więcej o danych.

To różnica priorytetów:

szybkość tworzenia prototypu
vs
jawność modelu i ograniczeń

Obsługa wejścia

Najprościej możemy użyć:

Ada.Text_IO

Dla liczb istnieją wyspecjalizowane pakiety.

Przykład:

with Ada.Integer_Text_IO;

Potem:

Ada.Integer_Text_IO.Get (X);

Generics w Text_IO

Ada posiada również generyczne pakiety IO dla własnych typów.

Możemy stworzyć tekstowe IO dla własnego typu liczbowego.

To bardzo elegancko współpracuje z systemem typów.

Zgadnij liczbę 0-100

Czas na nasz standardowy test.

Użyjemy generycznego pakietu:

Ada.Numerics.Discrete_Random

Kod

Plik:

guess.adb

with Ada.Text_IO;
with Ada.Numerics.Discrete_Random;

procedure Guess is

   subtype Guess_Range is
     Integer range 0 .. 100;

   package Random_Guess is
     new Ada.Numerics.Discrete_Random
       (Guess_Range);

   Generator : Random_Guess.Generator;
   Secret    : Guess_Range;

begin

   Random_Guess.Reset (Generator);
   Secret := Random_Guess.Random (Generator);

   Ada.Text_IO.Put_Line
     ("Zgadnij liczbe od 0 do 100.");

   loop

      Ada.Text_IO.Put ("Twoj strzal: ");

      declare

         Line  : constant String :=
           Ada.Text_IO.Get_Line;

         Guess_Value : Integer;

      begin

         Guess_Value := Integer'Value (Line);

         if Guess_Value not in Guess_Range then

            Ada.Text_IO.Put_Line
              ("Zakres to 0..100.");

         elsif Guess_Value < Secret then

            Ada.Text_IO.Put_Line
              ("Za malo!");

         elsif Guess_Value > Secret then

            Ada.Text_IO.Put_Line
              ("Za duzo!");

         else

            Ada.Text_IO.Put_Line
              ("Brawo!");

            exit;

         end if;

      exception

         when Constraint_Error =>

            Ada.Text_IO.Put_Line
              ("Podaj poprawna liczbe.");

      end;

   end loop;

end Guess;

Kompilacja klasyczna

gnatmake guess.adb

Uruchomienie:

Linux/macOS:

./guess

Windows:

.\guess.exe

Co ciekawego jest w tej wersji?

Już w tak małym programie widzimy wiele cech Ady.

Subtype

subtype Guess_Range is
  Integer range 0 .. 100;

Domena gry jest częścią kodu.

Generyk

Ada.Numerics.Discrete_Random

instancjonujemy dokładnie dla:

Guess_Range

Generator nie losuje „jakichś Integerów”.

Losuje wartość naszego konkretnego zakresu.

Jawne wyjątki

Niepoprawny tekst:

banana

w Integer'Value zgłosi:

Constraint_Error

Obsługujemy go lokalnie.

Membership

Guess_Value not in Guess_Range

jest niezwykle czytelne.

Ten sam projekt w Alire

Tworzymy projekt:

alr init --bin ada_guess

Wchodzimy:

cd ada_guess

Wygenerowana struktura będzie podobna do:

ada_guess/
├── alire.toml
├── ada_guess.gpr
└── src/
    └── ada_guess.adb

Wstawiamy kod do:

src/ada_guess.adb

Budujemy:

alr build

Uruchamiamy:

alr run

`alire.toml`

To manifest projektu.

Może zawierać między innymi:

name
version
description
authors
licenses
dependencies

Bardzo podobna idea do:

Cargo.toml
package.json
pyproject.toml

Dodawanie biblioteki

Przykład:

alr with some_library

Alire dodaje zależność do projektu i rozwiązuje jej zależności.

Szukanie bibliotek

alr search json

albo:

alr search http

Ekosystem jest oczywiście mniejszy niż npm czy PyPI, ale istnieje normalny współczesny katalog pakietów.

Toolchain Alire

Możemy wybrać kompilator:

alr toolchain --select

Alire potrafi utrzymywać kilka toolchainów.

To świetne, jeśli różne projekty wymagają różnych wersji GNAT.

GPRbuild

Większe projekty Ada często używają:

GPR project files

Przykład:

project My_App is
   for Source_Dirs use ("src");
   for Object_Dir use "obj";
   for Main use ("main.adb");
end My_App;

Plik:

my_app.gpr

Budowanie:

gprbuild -P my_app.gpr

Dlaczego oddzielny system projektów?

Duży projekt potrzebuje konfiguracji:

źródeł,
targetu,
kompilatora,
flag,
bibliotek,
języków,
ścieżek,
build modes.

GPRbuild może obsługiwać projekty wielojęzykowe.

Debug build i release build

Możemy tworzyć różne scenariusze kompilacji.

Debug:

checks
debug symbols
mniejsza optymalizacja

Release:

optimizacja
świadomie dobrane checks

W Ada wyłączanie checks powinno być przemyślaną decyzją.

W projektach SPARK część checks można formalnie udowodnić jako niemożliwe do naruszenia.

Debugger

GNAT współpracuje z:

GDB

Przykład:

gdb ./program

Typowe komendy:

break
run
next
step
print
backtrace

GNAT Studio

AdaCore rozwija IDE:

GNAT Studio

Jest mocno zintegrowane z:

GNAT,
GPRbuild,
SPARK,
debuggerem.

Nie jest jednak konieczne.

Visual Studio Code

Ada ma rozszerzenia dla VS Code i Language Server.

Jeśli już pracujesz w VS Code, nie musisz zmieniać całego workflow.

W typowym projekcie:

VS Code
+
Ada Language Server
+
Alire
+
GNAT

jest całkiem normalnym zestawem.

Zobacz:

Visual Studio Code

Formatowanie kodu

Ada ma bardzo charakterystyczny styl.

Przykład:

procedure Withdraw
  (Balance : in out Natural;
   Amount  : Positive)
is
begin
   Balance := Balance - Amount;
end Withdraw;

Kod jest zwykle pionowo rozłożony i bardzo jawny.

Nie chodzi o minimalizowanie liczby znaków.

Chodzi o czytelność.

Nazewnictwo

Typowy styl:

Engine_Temperature
Current_Balance
Read_Message
Maximum_Retry_Count

Ada bardzo dobrze wygląda z opisowymi nazwami.

W safety-critical software kilka dodatkowych znaków jest małym kosztem.

Nie walcz z językiem

Jeżeli próbujesz pisać Adę dokładnie jak C:

wszystko Integer
wszędzie access
wszędzie unchecked
brak zakresów
brak pakietów
brak kontraktów

tracisz większość jej wartości.

Ada działa najlepiej, gdy pozwolisz systemowi typów opisać problem.

Przykład złego modelu

Mode : Integer;

Znaczenie:

0 = off
1 = standby
2 = run
3 = emergency

Teraz legalne jest również:

-500
42
999999

Lepszy model

type Operating_Mode is
  (Off,
   Standby,
   Run,
   Emergency);

Mode : Operating_Mode := Off;

Nie da się przypadkiem ustawić:

bo 42 nie jest trybem pracy.

Jeszcze lepszy model domeny

type Celsius is
  range -273 .. 10_000;

type Pressure_Pascal is
  range 0 .. 1_000_000;

type Operating_Mode is
  (Off,
   Standby,
   Run,
   Emergency);

Program zaczyna mówić językiem domeny.

Range checks jako dokumentacja

subtype Port_Number is
  Integer range 0 .. 65_535;

To jednocześnie:

typ,
dokumentacja,
runtime constraint,
informacja dla analizatora.

Komentarz byłby znacznie słabszy.

Enumeration zamiast boolean

Czasem:

Enabled : Boolean;

jest wystarczające.

Ale czasem dwa stany to za mało.

Zamiast:

Is_Ready : Boolean;

może lepiej:

type Device_State is
  (Starting,
   Ready,
   Failed,
   Shutdown);

Model staje się bardziej precyzyjny.

Named ranges

Zamiast:

for I in 0 .. 99 loop

lepiej często:

for I in Buffer'Range loop

Kod przestaje zależeć od konkretnego rozmiaru.

Unconstrained parameters

Funkcja może przyjąć dowolny String.

procedure Print_Name
  (Name : String)
is
begin
   ...
end Print_Name;

Nie trzeba znać jego długości przy kompilacji procedury.

Name'First, Name'Last, Name'Range opisują konkretny obiekt.

`declare` blocks

Ada pozwala otworzyć lokalny blok deklaracji:

declare

   X : Integer := 10;

begin

   Put_Line
     (Integer'Image (X));

end;

Zmienne istnieją tylko w tym zakresie.

To świetne do ograniczania scope.

Nested procedures

Procedury mogą być zagnieżdżone.

procedure Main is

   procedure Helper is
   begin
      ...
   end Helper;

begin

   Helper;

end Main;

Helper może mieć dostęp do danych otaczającej procedury.

Scope

Ada bardzo mocno kontroluje widoczność nazw.

To ważne w dużych systemach.

Mniej globalnego stanu oznacza mniej niespodzianek.

Elaboracja

Pakiety Ady mogą mieć kod inicjalizacyjny.

Przykład:

package body Config is

begin

   Load_Config;

end Config;

Ten kod jest wykonywany podczas elaboracji jednostki.

Ada musi ustalić poprawną kolejność elaboracji zależności.

Stąd między innymi rola binder-a.

Finalization

Ada ma mechanizmy kontrolowanej inicjalizacji i finalizacji obiektów.

Pakiet:

Ada.Finalization

pozwala tworzyć typy z operacjami:

Initialize
Adjust
Finalize

To odpowiednik części idei znanych z:

RAII,
destruktorów,
resource management.

Determinizm

Ada jest często wybierana tam, gdzie program musi zachowywać się przewidywalnie.

Nie oznacza to:

każdy program Ada jest automatycznie deterministyczny.

Ale język i jego profile oferują mechanizmy sprzyjające analizowalności:

zakresy,
statyczne typowanie,
kontrolowane tasking,
real-time,
ograniczenia języka,
formalna analiza.

Safety kontra security

To dwie różne rzeczy.

Safety

Program nie może spowodować niebezpiecznego zachowania systemu.

Przykład:

sterowanie pociągiem
autopilot
urządzenie medyczne

Security

Program ma być odporny na celowe działania przeciwnika.

Przykład:

atak sieciowy
złośliwe dane wejściowe
eskalacja uprawnień

Ada i SPARK są używane w obu kontekstach.

Certification

Ada jest często spotykana w projektach podlegających rygorystycznym standardom.

Przykładowe domeny stosują standardy takie jak:

DO-178C
EN 50128 / EN 50657
ISO 26262
IEC 61508
ECSS

Sam fakt użycia Ady nie certyfikuje programu.

Certyfikacji podlega proces, artefakty, narzędzia i dowody zgodności.

Język może jednak ułatwić osiąganie wymaganych właściwości.

Nie istnieje magiczny bezpieczny język

Ada nie usuwa potrzeby:

dobrego projektu,
testów,
code review,
analizy wymagań,
bezpiecznej architektury,
właściwego procesu.

Można napisać zły program w Adzie.

Różnica polega na tym, że język daje dużo narzędzi utrudniających pewne klasy błędów.

Dlaczego Ada nie podbiła całego świata?

Kilka powodów.

Historia

Język długo kojarzył się z:

wojskiem
kontraktami rządowymi
drogimi kompilatorami

Rozmiar języka

Ada jest duża.

Ma dużo mechanizmów.

To może odstraszać ludzi szukających minimalistycznego języka.

Ekosystem

Nie ma ekosystemu wielkości:

npm
PyPI
Maven

Rynek

Większość aplikacji webowych nie potrzebuje poziomu rygoru typowego dla avionics.

JavaScript wystarczy do wielu problemów.

Ale Ada nie umarła

To bardzo ważne.

Ada nadal posiada:

aktywny standard,
GCC GNAT,
Alire,
GPRbuild,
SPARK,
GNATprove,
biblioteki,
współczesne IDE,
projekty przemysłowe.

To język niszowy.

Nie martwy.

Mały projekt domenowy

Załóżmy system baterii.

Zamiast:

Charge : Integer;
Voltage : Float;
Mode : Integer;

tworzymy:

subtype Charge_Percent is
  Integer range 0 .. 100;

type Volts is new Float;

type Battery_Mode is
  (Charging,
   Discharging,
   Idle,
   Fault);

Dane:

Charge  : Charge_Percent := 80;
Voltage : Volts := 12.5;
Mode    : Battery_Mode := Idle;

Kod od razu jest bardziej zrozumiały.

Kontrakt baterii

procedure Consume
  (Charge : in out Charge_Percent;
   Amount : Positive)
with
  Pre => Amount <= Charge;

Nie musimy pisać komentarza:

Amount cannot be larger than current charge

Warunek jest częścią programu.

SPARK-owa wersja

Możemy dodać:

procedure Consume
  (Charge : in out Charge_Percent;
   Amount : Positive)
with
  Pre  => Amount <= Charge,
  Post => Charge =
            Charge'Old - Amount;

Teraz specyfikacja mówi również dokładnie, jaki ma być rezultat.

Testowanie

Formal proof nie zastępuje wszystkich testów.

Test nadal sprawdza rzeczy takie jak:

integracja,
sprzęt,
UI,
zachowanie systemu,
timing,
biblioteki zewnętrzne,
realne środowisko.

Najsilniejsze podejście często łączy:

types
contracts
static analysis
formal proof
unit tests
integration tests
system tests

AUnit

Ekosystem Ada posiada framework testowy:

AUnit

Może być używany do klasycznych unit tests.

W Alire można wyszukać dostępne biblioteki testowe i dodać je jako zależność.

`pragma Assert`

Do małych testów wystarczy czasem:

pragma Assert
  (Add (2, 3) = 5);

Przy włączonych assertions błąd będzie widoczny podczas uruchamiania.

Fuzzing

Ada nie wyklucza fuzzingu.

Wręcz przeciwnie.

Runtime checks mogą sprawić, że błędne zachowanie zostanie wykryte jako jawny exception zamiast cichego uszkodzenia pamięci.

To może być bardzo użyteczne w testowaniu odporności.

Wydajność

Ada jest językiem kompilowanym do kodu natywnego.

GNAT korzysta z infrastruktury GCC.

Nie ma fundamentalnego powodu, dla którego program Ada musi być wolny.

Koszt mogą dodawać:

runtime checks,
tasking,
abstrakcje,
konkretna implementacja.

Ale kompilator może również optymalizować wiele konstrukcji bardzo skutecznie.

Checks kontra wydajność

Ada pozwala kontrolować checks.

Ale zasada powinna brzmieć:

nie wyłączaj kontroli tylko dlatego, że możesz.

Najpierw:

zmierz,
znajdź problem,
zrozum konsekwencje,
ewentualnie użyj proof,
dopiero wtedy rozważ wyłączenie konkretnej kontroli.

`pragma Suppress`

Ada posiada mechanizmy wyłączania części runtime checks.

Przykład:

pragma Suppress (Range_Check);

To potężne narzędzie.

I łatwy sposób na odebranie sobie części zalet Ady.

Używać tylko świadomie.

Bezpieczeństwo pamięci

Ada posiada wiele mechanizmów chroniących pamięć:

bounds checks,
range checks,
silne typy,
kontrolowane access types,
runtime checks.

Nie znaczy to jednak:

Ada jest językiem całkowicie memory-safe w każdym możliwym programie.

Mechanizmy:

Unchecked_*
address clauses
FFI
low-level system code

mogą ominąć część ochrony.

`System.Address`

W niskopoziomowym kodzie możemy pracować z:

System.Address

To świat fizycznych/logicznych adresów.

Powinien być używany tam, gdzie rzeczywiście jest potrzebny.

Nie jako zamiennik normalnego modelu typów.

Embedded bez runtime?

Ada może być używana w bardzo małych środowiskach.

Istnieją runtime'y o różnych profilach:

pełne,
light,
minimalne,
bare metal.

To pozwala stosować język także tam, gdzie nie ma pełnego systemu operacyjnego.

Cross compilation

Alire i GNAT mają toolchainy cross dla różnych targetów.

Typowe rodziny:

ARM
RISC-V
AVR

Dzięki temu Ada może być używana bezpośrednio na mikrokontrolerach.

Ada Drivers Library

W świecie embedded istnieją biblioteki i przykłady pokazujące bezpośrednią pracę z peryferiami MCU.

To dobry kolejny krok po opanowaniu języka.

Gry i grafika

Ada nie jest pierwszym językiem, który przychodzi do głowy przy gamedevie.

Ale istnieją bindingi i biblioteki.

W Alire znajdziemy np. bindingi dla:

raylib
SDL
OpenGL

Można więc napisać normalną prostą grę.

Backend

Ada nadaje się również do serwerów.

Istnieją biblioteki:

HTTP,
sockets,
TLS bindings,
JSON,
XML,
bazy danych.

Ekosystem jest mniejszy niż Go czy Java, ale technicznie nie ma przeszkody, by stworzyć backend.

CLI

CLI jest bardzo naturalnym zastosowaniem.

Pakiet:

Ada.Command_Line

pozwala pobierać argumenty.

Przykład:

with Ada.Command_Line;

if Ada.Command_Line.Argument_Count > 0 then
   ...
end if;

Pliki

Standardowa biblioteka oferuje operacje IO.

Między innymi:

Ada.Text_IO
Ada.Sequential_IO
Ada.Direct_IO
Ada.Streams

W zależności od rodzaju danych.

Streams

Streams pozwalają serializować i przesyłać wartości.

Ada ma językowe atrybuty związane ze strumieniami:

'Read
'Write
'Input
'Output

To kolejny przykład, jak dużo mechanizmów integracyjnych język posiada w standardzie.

Unicode

Ada 2022 definiuje szeroki model znaków zgodny z Unicode/ISO 10646.

W praktyce sposób kodowania plików i IO zależy również od implementacji i środowiska.

Nie należy zakładać, że każdy stary program Ada automatycznie działa jak współczesna biblioteka UTF-8.

`Wide_Character` i `Wide_Wide_Character`

Ada posiada typy:

Character
Wide_Character
Wide_Wide_Character

oraz odpowiadające typy stringów.

To element standardowej obsługi większych zestawów znaków.

Dynamic allocation

Można używać:

new

Przykład:

type Node;
type Node_Access is access Node;

type Node is record
   Value : Integer;
   Next  : Node_Access;
end record;

P : Node_Access :=
  new Node'
    (Value => 10,
     Next  => null);

Ale w high-integrity i real-time dynamic allocation często jest ograniczana.

Deterministyczna pamięć

W systemach czasu rzeczywistego chcemy wiedzieć:

ile pamięci potrzebujemy
kiedy jest alokowana
ile trwa operacja

Dlatego często preferuje się:

statyczną alokację,- pule pamięci,
kontrolowane storage pools,
ograniczone profile runtime.

Storage pools

Ada pozwala kontrolować sposób alokacji obiektów access.

To zaawansowany temat, ale ważny dla embedded i real-time.

Można implementować własne:

storage pools

zamiast polegać na ogólnym heapie.

Generics kontra templates

Ada generics przypominają częściowo:

C++ templates,
Java generics,
Rust generics.

Ale model jest inny.

W Ada generyk jawnie deklaruje, jakie właściwości formalnego typu lub funkcji są potrzebne.

To bardzo precyzyjny kontrakt kompilacyjny.

Generic package

Przykład ideowy:

generic

   type Element_Type is private;

package Stack is

   procedure Push
     (Value : Element_Type);

   function Pop
     return Element_Type;

end Stack;

Potem:

package Integer_Stack is
  new Stack (Integer);

OOP

Ada 95 dodała rozbudowany model programowania obiektowego.

Podstawą są:

tagged types

Przykład:

type Shape is tagged record
   X : Float;
   Y : Float;
end record;

Możemy tworzyć rozszerzenia:

type Circle is new Shape with record
   Radius : Float;
end record;

Dispatching

Operacje na tagged types mogą być dispatching operations.

To odpowiednik dynamicznego polimorfizmu znanego z języków OOP.

Ada nie wymaga jednak, aby cały program był zorganizowany obiektowo.

Możesz używać:

proceduralnego stylu,
pakietów,
generyków,
OOP,

tam, gdzie pasują.

Interfaces

Ada posiada również interfejsy podobne ideowo do interfejsów Javy/C#.

Można budować hierarchie zachowań bez wymuszania jednej implementacji danych.

Nie wszystko jest obiektem

To odróżnia Adę od Smalltalka czy części języków OOP.

Ada jest:

multi-paradigm

Nie zmusza do klas jako podstawowej jednostki każdego programu.

Operator overloading

Dla własnego typu:

type Vector is record
   X : Float;
   Y : Float;
end record;

możemy zdefiniować:

function "+"
  (Left  : Vector;
   Right : Vector)
   return Vector;

Dzięki temu:

C := A + B;

może mieć naturalne znaczenie domenowe.

Syntactic noise?

Ada jest bardziej rozwlekła niż Go czy Python.

Przykład:

if X > 10 then
   Do_Something;
end if;

zamiast:

if (x > 10) {
    doSomething();
}

Ale czytelnik widzi:

koniec if

a nie tylko:

Przy długich funkcjach ma to realną wartość.

Czy Ada jest trudna?

Podstawy:

nie

Duża część składni jest bardzo regularna.

Trudniejsze są:

pełny system typów,
access types,
tasking,
representation clauses,
generics,
SPARK,
real-time,
pełny standard.

Ale nie trzeba znać całej Ady, aby napisać przydatny program.

Minimalny zestaw do zwykłej aplikacji

Wystarczy:

procedures
functions
types
subtypes
arrays
records
packages
exceptions
containers
Alire

Reszta może przyjść później.

Minimalny zestaw do embedded

Dodaj:

modular types
representation clauses
volatile
address clauses
real-time
tasking/protected objects
cross compiler

Minimalny zestaw do SPARK

Dodaj:

Pre
Post
Global
Depends
SPARK_Mode
GNATprove
proof levels
loop invariants

Loop invariants

Formalny proof pętli wymaga czasem powiedzenia proverowi, jaka własność pozostaje prawdziwa po każdej iteracji.

To:

loop invariant

Przykład ideowy:

pragma Loop_Invariant
  (Sum >= 0);

W prawdziwym dowodzie invariant musi być wystarczająco precyzyjny, aby prover mógł udowodnić końcową właściwość.

Prover nie czyta w myślach

To ważne.

Kod może być logicznie poprawny, ale GNATprove może nie mieć wystarczających informacji, by to automatycznie udowodnić.

Wtedy trzeba dostarczyć:

kontrakt,
invariant,
lemma,
mocniejszy typ,
lepszą strukturę kodu.

Formalna weryfikacja jest współpracą:

programista
+
specyfikacja
+
automatyczny prover

Proof levels

GNATprove oferuje różne poziomy i tryby analizy.

Możemy wykonywać szybkie:

flow/check

albo głębszy:

prove

W dużym projekcie nie zawsze uruchamiamy najdroższy proof po każdej zmianie.

False alarm kontra nieudowodniona właściwość

Jeżeli prover mówi:

cannot prove

to nie zawsze znaczy:

program na pewno ma błąd

Może znaczyć:

błąd istnieje,
kontrakt jest za słaby,
prover potrzebuje dodatkowej informacji,
konstrukcja jest trudna do automatycznego dowodu.

Natomiast udany proof konkretnej właściwości daje znacznie silniejszą gwarancję niż pojedynczy test.

Kontrakt nie jest pełną specyfikacją świata

Jeżeli napiszesz zły kontrakt i poprawnie go udowodnisz, możesz nadal otrzymać program spełniający złą specyfikację.

Formalny proof odpowiada:

czy implementacja spełnia to, co opisałeś?

Nie odpowiada automatycznie:

czy to, co opisałeś, jest tym, czego naprawdę chciał klient?

Przykład błędnej specyfikacji

Jeżeli wymaganie brzmi:

saldo po wypłacie ma się zmniejszyć

a napiszesz:

Post => Balance = Balance'Old + Amount

prover może udowodnić implementację dodającą pieniądze.

Problem leży w specyfikacji.

Formal methods nie zastępują rozumienia domeny.

Największa siła: warstwy zabezpieczeń

Ada działa najlepiej, gdy nakładamy wiele warstw:

typ
+
zakres
+
kontrakt
+
runtime check
+
static analysis
+
proof
+
test

Nie każda aplikacja potrzebuje wszystkich.

Ale język daje możliwość ich użycia.

Porównanie filozofii czterech języków

C

masz pełną kontrolę
uważaj

Go

dajmy mało mechanizmów
żeby kod pozostał prosty

Rust

ownership i borrow checker
mają wyeliminować całe klasy błędów pamięci

Ada

opisz dokładnie domenę,
ograniczenia i kontrakty,
a narzędzia będą ich pilnować

Co Ada daje, czego łatwo nie docenić?

Największą wartością często nie jest pojedyncza funkcja języka.

Jest nią możliwość zapisania intencji programisty w kodzie.

Porównaj:

X : Integer;

subtype Retry_Count is
  Integer range 0 .. 5;

Retries : Retry_Count := 0;

Drugi zapis mówi znacznie więcej.

Kod jako model świata

Dobry program Ada próbuje odzwierciedlać domenę.

Zamiast:

int
int
int
bool

mamy:

Altitude
Airspeed
Temperature
Engine_State
Valve_Position

Kompilator może wtedy wychwycić mieszanie rzeczy, które przypadkiem mają ten sam fizyczny format.

Czy warto uczyć się Ady w 2026?

Jeżeli celem jest:

maksymalna liczba ofert frontendowych

nie.

TypeScript da lepszy zwrot.

Jeżeli interesują Cię:

języki programowania,
systemy,
safety-critical,
embedded,
formal methods,
silne systemy typów,
projektowanie niezawodnego software,

Ada jest niezwykle ciekawa.

Ada jako język edukacyjny

Ada uczy bardzo dobrych nawyków:

nazywania typów,
jawnych zakresów,
projektowania API,
myślenia o invariants,
rozdzielenia specyfikacji od implementacji,
kontrolowania side effects.

Nawet jeśli potem wrócisz do C, Go czy TypeScriptu, część tych nawyków zostanie.

Mini-projekt do dalszej nauki

Dobrym projektem po zgadywance jest:

symulator konta bankowego

Typy:

type Money is delta 0.01 digits 12;

subtype Percentage is
  Integer range 0 .. 100;

Operacje:

Deposit
Withdraw
Transfer
Balance

Kontrakty:

Amount > 0
Amount <= Balance
suma środków po transferze się nie zmienia

To świetne laboratorium dla:

Ada + SPARK

Drugi projekt: sterownik temperatury

Model:

Temperature
Target_Temperature
Heater_State
Sensor_State

Zakresy:

-40..150

Kontrakty:

heater cannot turn on when sensor is failed

Protected object:

shared sensor state

Periodic task:

read every 100 ms

To już zaczyna przypominać prawdziwy system embedded.

Trzeci projekt: C64? Tak

Po artykule assemblerowym można zrobić bardzo dziwny eksperyment:

6502/C64 + Ada

Nie jest to najbardziej naturalny współczesny target GNAT, ale świetnie pokazuje różnicę filozofii:

Assembler:

maksymalnie blisko hardware

Ada:

maksymalnie dużo semantyki i kontroli

W praktyce sensowniejszym embedded targetem dla współczesnej Ady będzie:

ARM
RISC-V
AVR

Szybka ściąga składni

Zmienna

X : Integer := 10;

Stała

Max : constant Integer := 100;

Typ

type Meters is new Float;

Podtyp

subtype Percentage is
  Integer range 0 .. 100;

Enumeration

type State is
  (Off, On, Failed);

If

if X > 0 then
   ...
elsif X = 0 then
   ...
else
   ...
end if;

Case

case State is
   when Off =>
      ...

   when On =>
      ...

   when Failed =>
      ...
end case;

Loop

loop
   ...
   exit when Done;
end loop;

While

while X > 0 loop
   ...
end loop;

For

for I in 1 .. 10 loop
   ...
end loop;

Function

function Add
  (A : Integer;
   B : Integer)
   return Integer;

Procedure

procedure Increment
  (X : in out Integer);

Record

type Point is record
   X : Float;
   Y : Float;
end record;

Array

type Values is
  array (Positive range <>)
  of Integer;

Exception

Invalid_Value : exception;

Raise

raise Invalid_Value;

Contract

with
  Pre  => X > 0,
  Post => Result > 0;

Ściąga narzędzi

Narzędzie	Do czego służy
`gnat`	toolchain kompilatora Ada
`gnatmake`	prosty automatyczny build
`gprbuild`	budowanie projektów GPR
`alr`	Alire - pakiety, toolchain, projekty
`gnatprove`	formalna analiza SPARK
`gdb`	debugger
GNAT Studio	IDE
Ada Language Server	obsługa IDE/editorów

Ściąga rozszerzeń plików

Rozszerzenie	Znaczenie
`.adb`	body / procedura / implementacja
`.ads`	specification
`.gpr`	projekt GPRbuild
`alire.toml`	manifest Alire

Typowy nowy projekt 2026

Najprościej:

alr init --bin my_app
cd my_app
alr build
alr run

Edytujemy:

src/my_app.adb

Dodajemy bibliotekę:

alr with nazwa_crate

Jeżeli chcemy SPARK:

alr with gnatprove

i uruchamiamy narzędzia w środowisku projektu.

Typowy prosty projekt bez Alire

Pliki:

main.adb
calculator.ads
calculator.adb

Budowanie:

gnatmake main.adb

GNAT odnajdzie zależności i zbuduje wymagane jednostki.

Typowy większy projekt

my-project/
├── alire.toml
├── my_project.gpr
├── src/
│   ├── main.adb
│   ├── network.ads
│   ├── network.adb
│   ├── storage.ads
│   └── storage.adb
├── tests/
└── README.md

Build:

alr build

Testy:

osobny test crate
lub framework AUnit

Co czytać dalej?

Jeżeli chcesz nauczyć się Ady naprawdę:

1. Podstawy

typy,
zakresy,
procedury,
funkcje,
pakiety.

2. Model danych

arrays,
records,
discriminants,
access types.

3. Modularność

packages,
private types,
generics.

4. Runtime

exceptions,
tasks,
protected objects.

5. Low-level

representation clauses,
volatile,
interfacing C,
embedded.

6. High integrity

contracts,
SPARK,
GNATprove,
real-time profiles.

Najważniejsze rzeczy do zapamiętania

Jeżeli zapomnisz większość artykułu, zapamiętaj te punkty:

Ada jest normalnym współczesnym językiem kompilowanym.
GNAT jest częścią świata GCC.
Alire daje współczesny workflow pakietów i toolchainów.
Ada jest bardzo silnie typowana.
Nowy typ naprawdę jest nowym typem.
Podtyp może ograniczyć legalny zakres wartości.
Bounds i range checks są fundamentalną częścią modelu.
Pakiet ma oddzielną specyfikację i implementację.
Kontrakty mogą być częścią kodu, nie komentarzem.
Tasking jest wbudowany w język.
Protected objects wspierają bezpieczniejszą współbieżność.
Ada potrafi zejść bardzo blisko hardware.
SPARK umożliwia formalne dowodzenie konkretnych właściwości programu.
Formal proof nie zastępuje poprawnych wymagań ani wszystkich testów.
Ada nie jest martwa - jest niszowa i bardzo wyspecjalizowana.

Jedno zdanie, które najlepiej opisuje Adę

Jeżeli C mówi:

ufam programiście, to Ada mówi:

opisz dokładnie, co programowi wolno zrobić, żebym mogła pomóc Ci zauważyć, kiedy robi coś innego.

To właśnie jest jej największa siła.

Powiązane materiały TechHandbooka

Oficjalne źródła i dokumentacja

Stan sekcji narzędziowej: wrzesień 2026.

Standard

Ada 2022 documents: https://www.adaic.org/ada-resources/standards/ada22/
Ada 2022 Reference Manual: https://www.adaic.org/resources/add_content/standards/22rm/html/RM-TTL.html

Nauka języka

AdaCore Learn: https://learn.adacore.com/
Introduction to Ada: https://learn.adacore.com/courses/intro-to-ada/

GNAT / GCC

GCC Ada: https://gcc.gnu.org/onlinedocs/gnat_ugn/
GCC: https://gcc.gnu.org/

Alire

Alire: https://alire.ada.dev/
Getting Started: https://alire.ada.dev/docs/getting-started
Toolchain management: https://alire.ada.dev/docs/toolchains

SPARK

Introduction to SPARK: https://learn.adacore.com/courses/intro-to-spark/
SPARK User's Guide: https://docs.adacore.com/spark2014-docs/html/ug/

AdaCore

AdaCore: https://www.adacore.com/
GNAT Studio: https://github.com/AdaCore/gnatstudio

Koniec serii językowej

Ta czteroczęściowa seria pokazuje cztery bardzo różne spojrzenia na programowanie:

1. Współczesne języki

Świat, z którym spotkasz się w codziennej pracy:

Python
JavaScript
TypeScript
Java
C
C++
Go
Rust
...

2. Historyczne języki

Skąd wzięły się pomysły, które dziś wydają się oczywiste:

FORTRAN
COBOL
ALGOL
Lisp
Pascal
Smalltalk
Prolog
...

3. Assembler

Co znajduje się pod wszystkimi abstrakcjami:

CPU
rejestry
pamięć
stos
instrukcje

4. Ada

Co się dzieje, gdy język zostaje zaprojektowany z myślą:

kod ma być nie tylko działający,
ale możliwie łatwy do analizowania,
ograniczania i weryfikowania

Razem te cztery teksty pokazują coś ważniejszego niż składnia poszczególnych języków.

Pokazują, że język programowania jest przede wszystkim:

sposobem myślenia o problemie i zestawem kompromisów, które twórcy języka uznali za najważniejsze.

Praktyczna baza wiedzy technicznej.

Ada - język, w którym błędy mają być trudniejsze do popełnienia

Skąd wzięła się Ada?

Ada nie jest skrótem

Wersje języka

Ada 83

Ada 95

Ada 2005

Ada 2012

Ada 2022

Ada to nie SPARK

Ada

SPARK

GNAT

Po co Ada ma binder?

Alire

Dwie sensowne drogi instalacji

Droga 1 - systemowy GNAT

Droga 2 - Alire

Instalacja - Linux / Debian

Najprostsza instalacja systemowa

Instalacja Alire - Linux

Linux ARM

Instalacja - Windows

Alternatywa Windows - MSYS2

Instalacja - macOS

macOS i Apple Silicon

Pierwszy program - Hello World

with

Pełna nazwa

use

Struktura procedury

null

Średniki

Komentarze

Ada jest case-insensitive

Przypisanie

Deklarowanie zmiennych

Stałe

Podstawowe typy

Natural i Positive

Typ to nie tylko rozmiar

Dlaczego to jest świetne?

Jawne konwersje

Typ wyliczeniowy

case

Podtypy

Podtyp nie jest nowym typem

Sprawdzanie zakresów

Błąd wykryty wcześniej

Zakres jako część modelu

Typ modularny

Operacje bitowe na typach modularnych

Zapis liczb w innych podstawach

Floating point

Fixed point

Typy fizyczne? Nie bezpośrednio, ale...

Atrybuty

'First i 'Last

'Range

'Length

'Image

'Value

Instrukcja if

elsif

Boolean

Pętla nieskończona

exit

while

for

reverse

Pętla po tablicy

Tablice z własnym indeksem

Tablice o nieustalonym rozmiarze

Tablice wielowymiarowe

String jest tablicą

Pułapka String

Unbounded_String

Rekordy

Named aggregates

`with`

`use`

`null`

`case`

`'First` i `'Last`

`'Range`

`'Length`

`'Image`

`'Value`

Instrukcja `if`

`elsif`

`exit`

`while`

`for`

`reverse`

`others`

Parametry `in`

`out`

`in out`

`null`

`pragma Assert`

`SPARK_Mode`

`Volatile`

`Atomic`