Экосистема: компилятор GNAT и анонс SPARK

На чём пишут и собирают программы на Ada сегодня: свободный компилятор GNAT, инструментарий вокруг него и SPARK — подмножество, которое позволяет не тестировать корректность, а доказывать её.

GNAT — основной свободный компилятор Ada, построенный на инфраструктуре GCC; де-факто стандартная среда для изучения и промышленной разработки на Ada.

Чем компилировать Ada

Язык без доступного компилятора остаётся теорией. К счастью, у Ada есть зрелый, свободный и качественный компилятор — GNAT (GNU NYU Ada Translator). Он построен поверх GCC, той же инфраструктуры, что компилирует C, C++ и Fortran, и потому наследует её зрелую генерацию машинного кода под десятки платформ. GNAT начинался как академический проект в Нью-Йоркском университете в начале 1990-х, а затем его развитие подхватила компания AdaCore, которая по сей день остаётся главным коммерческим двигателем экосистемы Ada, поддерживая и свободную, и платную сертифицированную версии инструментов.

Важная мысль для новичка: то, что главный компилятор Ada свободный и открытый, разрушает миф о «закрытом военном языке». Любой может скачать GNAT, установить и начать писать. Простейшая программа компилируется одной командой:

gnatmake hello.adb

Утилита gnatmake сама разбирается в зависимостях между файлами, компилирует нужные модули и связывает результат в исполняемый файл. В современных проектах вместо неё чаще используют систему сборки gprbuild с файлами проекта (расширение .gpr), которые описывают, где лежат исходники, какие опции компиляции применять и какие зависимости подключать.

Структура исходников: пара файлов на единицу

В мире GNAT принято соглашение об именах файлов, отражающее фундаментальную для Ada идею разделения интерфейса и реализации. Спецификация пакета (его публичный контракт) лежит в файле с расширением .ads (Ada specification), а тело (реализация) — в файле .adb (Ada body). Например, пакет Sensors разместится в sensors.ads и sensors.adb. Имя файла — это имя единицы в нижнем регистре. Такое разделение позволяет публиковать интерфейс отдельно от кода и компилировать модули независимо.

-- файл: counter.ads  (спецификация — что снаружи)
package Counter is
   procedure Increment;
   function Value return Natural;
end Counter;

-- файл: counter.adb  (тело — как именно)
package body Counter is
   Current : Natural := 0;
   procedure Increment is
   begin
      Current := Current + 1;
   end Increment;
   function Value return Natural is
   begin
      return Current;
   end Value;
end Counter;

Тип Natural здесь — стандартный поддиапазон целых, начинающийся с нуля; о нём подробно в следующем разделе. Главное, что нужно увидеть: внешний мир знает только counter.ads и не зависит от того, как именно устроен счётчик внутри. Это та самая модульность, которую требовал Steelman.

Инструментарий вокруг компилятора

Компилятор — лишь часть истории. Вокруг GNAT выстроена богатая экосистема, особенно ценная для критичных систем:

GNAT Studio — интегрированная среда разработки специально под Ada и SPARK: редактор с пониманием семантики, отладчик, навигация по коду, интеграция с анализаторами.
GPRbuild — система сборки на основе проектных файлов .gpr, заменяющая ручной вызов компилятора в больших проектах.
Alire — современный менеджер пакетов и зависимостей для Ada (по духу похож на пакетные менеджеры других языков), сильно упрощающий старт и подключение библиотек.
gnatprove — инструмент формальной верификации для SPARK, о котором ниже.
Различные анализаторы покрытия, метрик и проверки стиля, нужные для сертификации.

Для учебных целей сегодня проще всего начать с Alire: он сам ставит подходящую версию GNAT и создаёт скелет проекта, избавляя от ручной настройки.

SPARK: от тестирования к доказательству

Теперь самое впечатляющее, что отличает мир Ada от почти всех остальных, — SPARK. Это не отдельный язык, а строго определённое подмножество Ada вместе с инструментами, которые позволяют не тестировать программу, а математически доказывать её свойства. Разница принципиальна. Тестирование проверяет поведение на конечном наборе входов: вы запускаете программу на тысяче примеров и надеетесь, что тысяча первый не сломает. Формальное доказательство рассуждает обо всех возможных входах сразу, как теорема в математике.

Из Ada в SPARK исключают то, что мешает рассуждать формально: например, неконтролируемые указатели и некоторые динамические конструкции. Зато добавляют возможность доказать утверждения вроде «эта функция никогда не вызовет переполнения», «выход за границу массива здесь невозможен», «этот контракт выполняется при любых аргументах». Инструмент gnatprove читает ваши контракты (те самые Pre и Post из Ada 2012) и пытается доказать их строго:

function Increment (X : Integer) return Integer
   with Pre  => X < Integer'Last,
        Post => Increment'Result = X + 1;

Предусловие X < Integer'Last говорит: вызывать можно только если X строго меньше максимального целого ('Last — атрибут, дающий верхнюю границу типа). При выполненном предусловии gnatprove докажет, что X + 1 точно не переполнится и постусловие верно — для любого допустимого X, без единого теста. Заметьте операторы < (меньше) и стрелку =>: в исходном коде это обычные символы, но в HTML их обязательно экранируют, иначе разметка ломается. Именно SPARK позволяет железным дорогам и авиации заявлять о доказанном отсутствии целых классов ошибок — то, чего тестированием в принципе достичь нельзя.

Как это всё сочетается под капотом

Логика экосистемы такая. Сначала вы пишете обычную Ada — уже она ловит массу ошибок типами и проверками. Затем, для самых ответственных частей, вы ужесточаете код до подмножества SPARK и доказываете критические свойства gnatprove. Остальное (ввод-вывод, неважные части) можно оставить на полной Ada. Получается градиент строгости: чем опаснее модуль, тем формальнее его гарантии. Эта возможность дозировать строгость — большое практическое достоинство: не нужно доказывать всю программу, достаточно её опасного ядра.

В нашем курсе мы будем изучать полную Ada (SPARK — отдельная большая тема), но важно с самого начала держать в голове, что контракты, которые мы пишем, в мире Ada не декорация: их можно проверять исполнением, а в SPARK — доказывать. Это и есть кульминация философии «дорого ошибиться».

Практика старта: от пустой папки до работающей программы

Полезно представить, как реально выглядит первый запуск, чтобы экосистема перестала быть абстракцией. Сегодня самый гладкий путь — менеджер пакетов Alire. Он скачивает подходящую версию GNAT, создаёт скелет проекта и берёт на себя сборку, избавляя новичка от ручной настройки компилятора. Типичная последовательность команд в терминале выглядит так:

alr init --bin hello      # создать заготовку исполняемой программы
cd hello
alr build                 # собрать проект
alr run                   # запустить

Команда alr init --bin hello разворачивает структуру: каталог с исходниками, файл проекта .gpr и манифест зависимостей. Внутри лежит готовая процедура Hello в файле hello.adb — её можно сразу собрать и запустить, а затем редактировать. Если нужна сторонняя библиотека, её добавляют командой вроде alr with имя_крейта, и Alire сам подтянет совместимую версию и пропишет зависимость. Это разительно отличается от устаревшего образа Ada как языка, требующего тяжёлой ручной возни с компилятором.

За кулисами alr build вызывает gprbuild, который читает файл проекта .gpr. В нём описано, где лежат исходники, какие опции компиляции применять (например, включить все предупреждения и проверки), и какие зависимости подключены. Файл проекта — это, по сути, декларативное описание сборки, понятное и инструментам анализа. Для критичных проектов в нём же включают строгие ключи: предупреждения как ошибки, дополнительные статические проверки, генерацию данных для анализа покрытия. Так одна и та же кодовая база может собираться в «учебном» режиме для экспериментов и в «сертификационном» — с максимальной строгостью.

Стоит подчеркнуть мысль, важную для всего курса: даже на этом первом шаге виден стиль Ada — всё явно и под контролем. Зависимости перечислены в манифесте, опции — в файле проекта, структура исходников отражает разделение спецификации и тела. Ничего не происходит «по магии» за спиной разработчика. Этот контроль над тем, что и как собирается, — продолжение той же философии, что и контроль над типами и памятью: в надёжных системах вы должны точно знать, из чего собран ваш бинарник, вплоть до версий и флагов.

Стоит подчеркнуть и доступность этой экосистемы для обучения, потому что это разрушает последний миф — будто Ada «не для простых смертных». Свободный GNAT, открытый Alire, бесплатная среда GNAT Studio и обширная документация делают порог входа не выше, чем у любого современного языка. Есть учебные ресурсы, онлайн-площадки для экспериментов прямо в браузере, активные форумы сообщества. Иными словами, между «хочу попробовать Ada» и «у меня собирается первая программа» сегодня лежат минуты, а не дни настройки. Это важно держать в голове на старте курса: всё, о чём мы будем говорить — типы, контракты, пакеты, — можно тут же проверить на реальном компиляторе, ничего не покупая и не выпрашивая лицензий. Серьёзность языка и его сертификационная родословная никак не противоречат тому, что начать с ним работать может буквально каждый. Промышленная мощь и доступность здесь идут рука об руку.

Частые ошибки и заблуждения

«Для Ada нет бесплатного компилятора». GNAT свободен, открыт и основан на GCC; начать можно бесплатно, удобнее всего через Alire.
Путать .ads и .adb. .ads — спецификация (интерфейс), .adb — тело (реализация); имя файла должно совпадать с именем единицы в нижнем регистре.
«SPARK — это другой язык». Это подмножество Ada плюс инструмент доказательства; код на SPARK остаётся валидной Ada.
Думать, что доказательство заменяет всё тестирование. Доказывают критические свойства ядра; периферию по-прежнему тестируют. Это дополняющие, а не взаимоисключающие методы.

Итоги

GNAT — основной свободный компилятор Ada на базе GCC; развивается AdaCore, доступен всем желающим.
Исходники делятся на спецификацию .ads (контракт) и тело .adb (реализация), что воплощает принцип разделения интерфейса и реализации.
Вокруг компилятора есть зрелый инструментарий: GNAT Studio, GPRbuild, менеджер пакетов Alire, анализаторы для сертификации.
SPARK — подмножество Ada с инструментом gnatprove, позволяющее не тестировать, а математически доказывать корректность для всех входов.
Экосистема даёт градиент строгости: обычная Ada для большинства кода, SPARK для критического ядра.