Притягательность языка Ada — типы как язык проектирования и опора для ПО, работающего десятилетиями
· Го Комура · Ada, Язык программирования, Строгая типизация, SPARK, GNAT, Alire, Высококритичные системы, Встраиваемые системы, Высокая надёжность
1. Что нужно понять в первую очередь
Приходилось ли вам слышать название языка Ada?
У многих сложилось впечатление: «старый язык», «военный язык», «просто слышал название на паре».
Но Ada — это язык, который остаётся действующим и сегодня.
В мире программ, где остановка стоит человеческих жизней — системы управления полётом самолётов, железнодорожная сигнализация, ракеты, авиадиспетчерские системы, искусственные спутники, медицинское оборудование — Ada применяется уже несколько десятилетий подряд.
При знакомстве с Ada важно держать в голове следующее.
Ada — язык, который направил все усилия на то, чтобы «убивать баги» до выполнения программы
Типы — не просто контейнеры для данных, а инструмент выражения замысла проектирования
Разделение спецификации и реализации, контракты и параллелизм встроены в язык
Ada не стала модной, но её философия проектирования унаследована современными языками
В этой статье мы разберём историю Ada, синтаксис, строгую типизацию, ограничения диапазона, пакеты, контрактное проектирование, задачи (task), SPARK, среду разработки и даже слабые стороны языка — одним словом, всё, что составляет притягательность Ada.
Цель статьи — чтобы читатели, которые обычно пишут на C#, C++ или Java, унесли с собой ощущение того, что такое «выражать проектные решения через типы».
Фрагменты кода, которые встречаются в этой статье, опубликованы на GitHub в виде справочного набора, разложенного по файлам согласно главам.
ada-language-appeal - komurasoft-blog-samples (GitHub)
2. Что такое Ada — происхождение названия и история
Ada — это язык программирования общего назначения, появившийся в конце 1970-х годов по инициативе Министерства обороны США (DoD).
В то время Министерство обороны столкнулось с проблемой: в каждом проекте использовался свой язык, из-за чего расходы на сопровождение ПО стремительно росли.
Поэтому был объявлен международный конкурс на разработку стандартного языка, пригодного в том числе для встраиваемых систем и систем реального времени.
Победил проект команды под руководством Жана Ишбиа (Jean Ichbiah).
Название языка, Ada, происходит от имени Ады Лавлейс (Августа Ада Кинг, графиня Лавлейс) — женщины, которую называют первым в мире программистом.
Кратко историю Ada можно представить так.
1980 год принята первая спецификация под названием MIL-STD-1815
1983 год Ada 83 (стандарт ANSI)
1987 год становится стандартом ISO
1995 год Ada 95 (введены объектная ориентация и защищённые объекты)
2005 год Ada 2005 (интерфейсы, расширение библиотеки контейнеров)
2012 год Ada 2012 (контрактное проектирование введено как возможность языка)
2022 год Ada 2022 (актуальный стандарт)
Ada 95 стала одним из самых первых объектно-ориентированных языков, стандартизированных ISO.
А в Ada 2012 в спецификацию языка было включено контрактное проектирование (Design by Contract) — предусловия, постусловия и инварианты типов.
Ada — не «устаревший язык», а язык, который пересматривается уже более 40 лет.
3. Где используется Ada
Область, в которой Ada применяется непрерывно, — это системы, требующие высокой критичности (High Integrity).
Системы управления полётом и авионика гражданских самолётов
Системы управления воздушным движением
Системы сигнализации и обеспечения безопасности на железных дорогах
Ракеты и искусственные спутники
Оборонные системы
Медицинское оборудование
Некоторые критически важные системы в финансовой и промышленной сферах
У этих областей есть общие черты.
Ошибка напрямую приводит к гибели людей или огромным потерям
Сертификация и аудит требуют доказательств правильности
После развёртывания система работает десятилетиями
Стоимость исправления после релиза чрезвычайно высока
Это мир, где не работает подход «сначала выпустим, потом исправим».
Проектирование Ada отвечает именно на эти требования.
Через весь язык проходит одна идея: ошибки, которые можно найти во время компиляции, ловятся во время компиляции; то, что можно обнаружить только во время выполнения, — проверками во время выполнения; а то, что можно доказать математически, — устраняется доказательством.
Эта философия стоит того, чтобы её изучали и разработчики, пишущие обычные веб- или десктопные приложения.
4. Начнём с Hello, World
Посмотрим на код Ada.
with Ada.Text_IO;
procedure Hello is
begin
Ada.Text_IO.Put_Line ("Hello, Ada!");
end Hello;
Скорее всего, вы сразу заметите следующее.
with подключает библиотечный модуль
Тело программы — это процедура (procedure)
begin / end образуют границы блока
После end имя повторяется
Операторы завершаются точкой с запятой
Именно повтор имени в конце, как в end Hello;, — характерная черта Ada.
Даже когда блоки вложены глубоко, сразу понятно, «какому именно блоку принадлежит этот end».
Компилятор тоже проверяет соответствие имён, поэтому неправильное закрытие блока становится ошибкой компиляции.
Мелочь, но она прекрасно показывает философию Ada: язык поддерживает человека именно там, где тот склонен ошибаться при чтении кода.
5. Синтаксис, ориентированный на читаемость
Синтаксис Ada спроектирован так, что читаемость важнее, чем удобство написания.
В основе — идея, что программу читают гораздо чаще, чем пишут.
Например, циклы и условные конструкции выглядят так.
for I in 1 .. 5 loop
Ada.Text_IO.Put_Line (Integer'Image (I * I));
end loop;
if Temperature > 80.0 then
Start_Cooling;
elsif Temperature < 20.0 then
Start_Heating;
else
Keep_Current_State;
end if;
У оператора case есть характерная для Ada особенность.
case Today is
when Mon .. Fri =>
Put_Line ("Weekday");
when Sat | Sun =>
Put_Line ("Weekend");
end case;
Вот ключевые моменты.
case должен охватывать все значения, иначе это ошибка компиляции
Неявного проваливания (fall-through), как в языках C-семейства, не существует
Условия можно группировать через диапазоны (Mon .. Fri) и перечисления значений (Sat | Sun)
Если добавить значение в перечисление, все case, не охватывающие его, становятся ошибками компиляции.
Ощущение, что «компилятор сам перечисляет все места, затронутые изменением спецификации», однажды попробовав, уже не хочется терять.
Кроме того, аргументы можно передавать по имени.
Draw_Rectangle (Left => 10, Top => 20, Width => 100, Height => 50);
Это предотвращает путаницу аргументов, а код вызова сам становится документацией.
Присваивание — это :=, а сравнение — =, поэтому путаница вроде if (a = b) из C-подобных языков на уровне синтаксиса просто не может произойти.
6. Строгая типизация — превращаем путаницу единиц измерения в ошибку компиляции
Главная притягательность Ada — это её строгая типизация.
Слова «строгая типизация» используются во многих языках, но в Ada это понятие идёт на ступень глубже.
В Ada типы, объявленные под разными именами, — это разные типы, даже если их структура полностью совпадает.
type Meters is new Float;
type Seconds is new Float;
Distance : Meters := 100.0;
Time : Seconds := 9.58;
По сути оба этих типа — числа с плавающей точкой, но смешивать их нельзя.
Distance := Time; -- ошибка компиляции
Distance := Distance + Time; -- ошибка компиляции
Преобразование пишется явно, только когда оно действительно нужно.
Speed : constant Float := Float (Distance) / Float (Time);
Зачем такая строгость?
Немало реальных аварий в софтверном мире случились именно из-за «путаницы единиц измерения».
Известный пример — потеря марсианского зонда Mars Climate Orbiter в 1999 году из-за смешения имперской и метрической систем.
Ответ Ada прост.
Сделать метры и футы разными типами
Сделать их смешение ошибкой компиляции
Заставить писать преобразование явно
Не «быть внимательным», не «найти на ревью», не «поймать в тестах» — а сделать так, чтобы сборка просто не проходила.
В этом и заключается базовая позиция Ada.
7. Ограничения диапазона — блокируем некорректные значения на уровне типа данных
В Ada тип может нести на себе диапазон допустимых значений.
subtype Percentage is Integer range 0 .. 100;
Progress : Percentage := 50;
Попытка присвоить переменной типа Percentage значение вне диапазона вызывает во время выполнения исключение Constraint_Error.
Progress := 120; -- Constraint_Error во время выполнения
Нарушения, которые можно выявить во время компиляции, обнаруживаются именно тогда.
Неявные допущения вроде «значение должно быть от 0 до 100» или «значение должно быть не меньше 1» можно выразить не комментарием, а типом.
Более того, в стандартной библиотеке Ada заранее определены часто используемые типы с ограничениями.
Natural = Integer range 0 .. Integer'Last
Positive = Integer range 1 .. Integer'Last
А начиная с Ada 2012 к типу можно прикрепить произвольное условие в виде предиката.
subtype Even is Integer
with Dynamic_Predicate => Even mod 2 = 0;
В язык встроены и типы, ориентированные на управление аппаратурой, например типы с фиксированной точкой.
type Temperature is delta 0.1 range -50.0 .. 150.0;
Во многих языках проверка недопустимых значений часто выглядит так.
Валидация через if в начале функции
Пропущенные проверки остаются на совести код-ревью
Непонятно, какие функции уже получают проверенные значения
В Ada можно сказать так: «раз значение имеет этот тип, диапазон уже гарантирован».
Когда ответственность за валидацию переходит к типу данных, логика функции может сосредоточиться на своей настоящей задаче.
8. Массивы и индексы — проверка границ и индексация перечислениями
В массивах Ada можно свободно выбирать тип индекса.
type Day is (Mon, Tue, Wed, Thu, Fri, Sat, Sun);
type Hours_Array is array (Day) of Natural;
Work_Hours : Hours_Array := (Mon .. Fri => 8, others => 0);
Это массив, индексированный перечислением Day.
К нему можно обращаться как Work_Hours (Wed), и не нужно помнить, «что означает этот числовой индекс».
Циклы тоже можно писать в соответствии с типом индекса.
for D in Work_Hours'Range loop
Put_Line (Day'Image (D) & ":" & Natural'Image (Work_Hours (D)));
end loop;
Атрибуты 'Range, 'First, 'Last, 'Length в любой момент дают информацию о границах массива.
Поскольку границы нигде не зашиты жёстко, изменение размера массива не затрагивает циклы.
И, что важно, доступ к массиву всегда проверяется на выход за границы.
Buffer : String (1 .. 10);
Index : Integer := 11;
Buffer (Index) := 'x'; -- Constraint_Error во время выполнения
Переполнение буфера в C/C++ десятилетиями остаётся одной из главных причин уязвимостей.
В Ada выход за границы — это не неопределённое поведение, а определённое исключение.
Вместо того чтобы молча повредить память и вызвать загадочный сбой где-то в другом месте, программа сразу же громко останавливается там, где возникла проблема.
Если учесть стоимость расследования инцидентов в системах с долгим сроком эксплуатации, разница оказывается огромной.
9. Пакеты — разделение спецификации и реализации
Модульный механизм Ada — это пакет (package).
Пакет делится на два файла: спецификацию (spec) и тело (body).
counters.ads спецификация: интерфейс, открытый вовне
counters.adb тело: детали реализации
Спецификация пишется так.
package Counters is
type Counter is private;
procedure Increment (C : in out Counter);
function Value (C : Counter) return Natural;
private
type Counter is record
Count : Natural := 0;
end record;
end Counters;
Тело пишется так.
package body Counters is
procedure Increment (C : in out Counter) is
begin
C.Count := C.Count + 1;
end Increment;
function Value (C : Counter) return Natural is
begin
return C.Count;
end Value;
end Counters;
Обратите внимание на следующее.
Если объявить тип как private, вызывающая сторона не сможет трогать его внутреннюю структуру
Прочитав только спецификацию (.ads), можно полностью понять, как пользоваться пакетом
Изменение тела (.adb) при неизменной спецификации требует минимальной перекомпиляции у пользователей пакета
Это похоже на заголовочные файлы C/C++, но, в отличие от текстового включения через #include, согласованность здесь проверяется на уровне спецификации языка.
Расхождение между спецификацией и телом — это ошибка компиляции.
Кроме того, у каждого аргумента обязательно указывается режим: in, out или in out.
procedure Increment (C : in out Counter);
Достаточно взглянуть на сигнатуру, чтобы понять: аргумент только читается, только записывается или же читается и записывается.
Направление потока данных считывается без каких-либо знаний об указателях и ссылках.
10. Записи и дискриминанты
Аналог структуры в Ada — это запись (record).
type Point is record
X : Float := 0.0;
Y : Float := 0.0;
end record;
P : Point := (X => 1.0, Y => 2.0);
Поля могут иметь значения по умолчанию, а инициализация возможна через именованный агрегат.
Характерная для Ada возможность — дискриминант (discriminant).
type Buffer (Size : Positive) is record
Data : String (1 .. Size);
Length : Natural := 0;
end record;
Small : Buffer (Size => 16);
Large : Buffer (Size => 4096);
Дискриминант — это параметр, определяющий «форму» записи.
Buffer (16) и Buffer (4096) — один и тот же тип, но размер внутреннего массива фиксируется в момент объявления и больше не меняется.
Это похоже на «структуру с членом переменной длины плюс поле размера» в C, только здесь язык сам безопасно управляет этим как типом.
Рассогласование между размером и фактическими данными — классическая уязвимая точка в C — здесь попросту не может возникнуть.
11. Дженерики
У Ada дженерики (generic) были уже в самом первом стандарте 1983 года.
Это намного раньше, чем шаблоны C++ (1990-е) или дженерики Java (2004 год).
generic
type Element is private;
procedure Swap (Left, Right : in out Element);
procedure Swap (Left, Right : in out Element) is
Temp : constant Element := Left;
begin
Left := Right;
Right := Temp;
end Swap;
Пользователь создаёт конкретную реализацию, инстанцируя дженерик конкретным типом.
procedure Swap_Integers is new Swap (Element => Integer);
procedure Swap_Floats is new Swap (Element => Float);
Особенность дженериков Ada в том, что требуемые операции указываются явно.
generic
type Element is private;
with function "<" (Left, Right : Element) return Boolean is <>;
function Max (Left, Right : Element) return Element;
В спецификации прямо написано: «эта обобщённая функция требует от типа Element операцию сравнения».
Проблема, которая долго мучила шаблоны C++, — «ошибка выясняется только при инстанцировании», — в Ada попросту не возникает.
То, что пытались решить concepts из C++20 и границы трейтов (trait bounds) в Rust, у Ada был ответ уже 40 лет назад.
12. Обработка исключений
В Ada есть обработка исключений.
with Ada.Text_IO;
with Ada.Exceptions;
procedure Read_Config is
begin
Load_File ("config.txt");
exception
when Ada.Text_IO.Name_Error =>
Ada.Text_IO.Put_Line ("Конфигурационный файл не найден");
when E : others =>
Ada.Text_IO.Put_Line (Ada.Exceptions.Exception_Information (E));
raise;
end Read_Config;
В конце блока пишется раздел exception, где обработчики перечисляются по видам исключений.
Среди определённых языком исключений можно выделить следующие.
Constraint_Error нарушение ограничения диапазона, выход за границы массива, деление на ноль и т. п.
Program_Error нарушение правил языка (например, достижение точки, куда попадать нельзя)
Storage_Error нехватка памяти
Tasking_Error сбой во взаимодействии между задачами (task)
Важно, что нарушения ограничений диапазона и проверок границ полностью интегрированы в этот механизм исключений.
Если нарушено «ограничение, записанное в типе», возникает Constraint_Error.
Иными словами, ограничения диапазона, которые мы видели в главе 7, работают как автоматически сгенерированные утверждения времени выполнения (run-time assertions).
Не нужно самому разбрасывать по коду проверки через if.
13. Контрактное проектирование — предусловия и постусловия как возможность языка
Главная особенность Ada 2012 — поддержка контрактного проектирования (Design by Contract) на уровне языка.
Для подпрограмм можно писать предусловия (Pre) и постусловия (Post) прямо в коде.
package Stacks is
type Stack is private;
function Is_Full (S : Stack) return Boolean;
function Is_Empty (S : Stack) return Boolean;
function Count (S : Stack) return Natural;
procedure Push (S : in out Stack; Item : Integer)
with Pre => not Is_Full (S),
Post => Count (S) = Count (S)'Old + 1;
procedure Pop (S : in out Stack; Item : out Integer)
with Pre => not Is_Empty (S),
Post => Count (S) = Count (S)'Old - 1;
private
-- детали реализации
end Stacks;
Pre — это «обещание, которое должна соблюдать вызывающая сторона», Post — «обещание, которое гарантирует реализация».
Атрибут 'Old позволяет обратиться к значению до вызова.
Эти контракты можно включить как проверки времени выполнения через опцию компилятора (-gnata в GNAT).
При нарушении контракта возникает исключение Assertion_Error, и становится ясно, какая сторона нарушила обещание.
Нарушение Pre -> ошибка вызывающей стороны
Нарушение Post -> ошибка реализации
Чем это отличается от комментария в духе «этот метод нельзя вызывать для пустого стека»?
Комментарий может разойтись с реализацией, и никто этого не заметит
Контракт проверяется компилятором по синтаксису и типам
Контракт можно автоматически проверить во время выполнения
Контракт становится входными данными для статического доказательства через SPARK (глава 16)
Спецификация существует внутри кода в проверяемой форме.
Именно так устроен мир Ada 2012 и последующих версий.
С помощью инвариантов типа (Type_Invariant) можно записать и такое ограничение: «значение этого типа всегда удовлетворяет данному свойству».
14. Задачи (task) — параллелизм, встроенный в язык
Ещё одна значительная притягательность Ada — то, что параллелизм является частью спецификации языка.
Если C/C++ полагаются на API операционной системы или библиотеки (pthread, std::thread), то Ada встроила задачи (task) в язык ещё в 1983 году.
with Ada.Text_IO;
procedure Task_Demo is
task Worker;
task body Worker is
begin
for I in 1 .. 3 loop
Ada.Text_IO.Put_Line ("worker:" & Integer'Image (I));
delay 0.5;
end loop;
end Worker;
begin
for I in 1 .. 3 loop
Ada.Text_IO.Put_Line ("main :" & Integer'Image (I));
delay 0.5;
end loop;
end Task_Demo;
Как только объявляется task, параллельное выполнение начинается одновременно со стартом охватывающего блока.
И важно, что блок не завершится, пока не завершатся все задачи внутри него.
Целый класс ошибок вроде «забыли join у потока, и при завершении процесса происходит что-то странное» здесь структурно невозможен.
Для синхронизации между задачами в языке есть механизм рандеву (rendezvous).
task Logger is
entry Write (Message : String);
end Logger;
task body Logger is
begin
loop
select
accept Write (Message : String) do
Ada.Text_IO.Put_Line (Message);
end Write;
or
terminate;
end select;
end loop;
end Logger;
Со стороны вызывающего кода это выглядит как обычный вызов процедуры: Logger.Write ("hello");.
Взаимодействие между задачами через обмен сообщениями можно писать, вообще не имея понятия о блокировках.
Для систем реального времени стандартизированы и политика планирования, и управление приоритетами, а для повышения проверяемости — даже отдельный профиль Ravenscar, ограничивающий возможности задач.
15. Защищённые объекты — взаимоисключение как тип
Для взаимоисключающего доступа к разделяемым данным в Ada 95 введены защищённые объекты (protected object).
protected Shared_Counter is
procedure Increment;
function Value return Natural;
private
Count : Natural := 0;
end Shared_Counter;
protected body Shared_Counter is
procedure Increment is
begin
Count := Count + 1;
end Increment;
function Value return Natural is
begin
return Count;
end Value;
end Shared_Counter;
К данным защищённого объекта можно обратиться только через определённые для него операции.
А взаимоисключение гарантирует сам язык.
procedure чтение и запись разрешены, выполняется монопольно
function только чтение, допускает одновременное выполнение несколькими задачами
entry может заставить вызывающую сторону ждать выполнения условия (барьера)
Во многих языках взаимоисключение часто держится на дисциплине программиста.
Перед обращением к этим данным нужно захватить этот мьютекс
Не забыть освободить блокировку
Соблюдать порядок захвата блокировок
В защищённых объектах Ada «код, забывший захватить блокировку», написать попросту невозможно.
Потому что данные и защищающее их взаимоисключение объявляются как единый тип.
Используя барьерные условия entry, можно писать условную синхронизацию — например, «ждать, пока в очередь не поступят данные» — без ручного управления флагами или переменными условия.
16. SPARK — путь к формальной верификации
В мире Ada есть мощный союзник — SPARK.
SPARK — это подмножество Ada, спроектированное так, чтобы свойства программы можно было доказывать математически.
procedure Increment (X : in out Integer)
with SPARK_Mode,
Pre => X < Integer'Last,
Post => X = X'Old + 1;
Инструмент SPARK (GNATprove) доказывает следующее для такого кода, не выполняя его.
Что не произойдёт переполнение
Что не произойдёт нарушение ограничения диапазона
Что не произойдёт деление на ноль
Что не будет чтения неинициализированной переменной
Что Pre и Post согласованы между собой
Отличие от тестирования принципиально.
Тестирование подтверждает корректную работу для выбранных входных данных
Доказательство показывает, что свойство выполняется для всех входных данных
Контракты (Pre/Post), которые мы видели в главе 13, в SPARK становятся прямым объектом доказательства.
Контракт, написанный как проверка времени выполнения, впоследствии можно «повысить» до статуса доказанного.
SPARK накопил опыт в авиационной и оборонной сфере, а в последние годы его применение расширяется и в индустрии в целом — например, NVIDIA использует его для защиты прошивок.
Стереотип «формальные методы слишком академичны для практического применения» экосистема Ada/SPARK продолжает тихо опровергать.
17. Взаимодействие с C и C++
Ada — не изолированный язык.
Взаимодействие с C стандартизировано на уровне спецификации языка (приложение B).
Например, чтобы вызвать из Ada функцию Sleep из Windows API, пишут так.
with Interfaces.C;
procedure Sleep_Demo is
procedure Sleep (Milliseconds : Interfaces.C.unsigned)
with Import,
Convention => Stdcall,
External_Name => "Sleep";
begin
Sleep (1000);
end Sleep_Demo;
Вот ключевые моменты.
Import подключает внешнюю реализацию
Convention задаёт соглашение о вызовах (C, Stdcall и т. п.)
External_Name задаёт имя символа для компоновщика
Interfaces.C предоставляет типы, соответствующие типам C (int, unsigned, char* и т. п.)
Возможно и обратное направление.
С помощью Export процедуру, написанную на Ada, можно открыть как функцию, вызываемую из C.
Это позволяет использовать поэтапный подход.
Использовать существующую библиотеку C из Ada
Написать на Ada/SPARK только ключевую часть системы, оставив периферию на C/C++
Собрать код Ada в DLL и вызывать его из других языков
Ada — не язык, для которого единственный путь — «переписать всё с нуля»: с ним можно сосуществовать с уже существующими наработками, постепенно повышая надёжность начиная с самых важных частей.
18. Среда разработки — GNAT и Alire (работает и в Windows)
Может показаться, что для знакомства с Ada нужны дорогие инструменты.
На деле сегодня доступна полноценная бесплатная среда разработки.
GNAT Ada-компилятор, входящий в состав GCC (бесплатный)
Alire менеджер пакетов и инструмент сборки для Ada
GNAT Studio IDE от AdaCore
VS Code с расширением Ada Language Server — автодополнение и переход к определению
Именно появление Alire (команда alr) сделало знакомство с Ada заметно проще.
Опыт близок к cargo в Rust.
alr init --bin hello_ada
cd hello_ada
alr build
alr run
alr init создаёт проект, alr build собирает его, alr run запускает.
Сам тулчейн (компилятор GNAT) тоже подтягивает Alire, поэтому устанавливать компилятор вручную вообще не требуется.
Всё это работает и в Windows, и в Linux, и в macOS.
Если вы разрабатываете под Windows, кратчайший путь такой.
1. Скачать установщик для Windows с официального сайта Alire
2. Создать шаблон проекта командой alr init --bin
3. Установить в VS Code расширение Ada (от AdaCore)
4. Собрать и запустить проект командой alr build
Библиотеки тоже добавляются одной командой alr with <имя библиотеки>.
Времена, когда всё заканчивалось на этапе настройки окружения, прошли.
19. Слабые стороны Ada и на что обратить внимание
Мы рассказали о притягательных сторонах Ada, но у неё есть и слабости.
Разберём их честно.
Маленькая экосистема
Мало вариантов веб-фреймворков, GUI-библиотек, облачных SDK и т. п.
Число пакетов в Alire на порядки меньше, чем у основных языков
Мало специалистов и информации
Информации на русском языке особенно мало
Для внедрения в командную разработку нужно закладывать расходы на обучение
Синтаксис может казаться избыточным
Объявление типов и разделение спецификации/тела ощущаются тяжеловесными для мелких скриптов
Не подходит для задач по принципу «лишь бы заработало»
Рынок труда ограничен
Смещён в сторону авиакосмической отрасли, обороны, железных дорог и подобных сфер
История также учит, что тезис «используешь Ada — значит, ты в безопасности» неверен в такой упрощённой форме.
Взрыв первой ракеты Ariane 5 в 1996 году произошёл в том числе из-за программного обеспечения, написанного на Ada.
Код, написанный для Ariane 4, повторно использовали в Ariane 5 с другими лётными характеристиками: неожиданно большое значение при преобразовании вызвало Constraint_Error, оно не было корректно обработано, и система остановилась.
Эта авария показывает следующее.
Проверки времени выполнения языка обнаружили проблему (система не сломалась молча)
Но условия эксплуатации изменились, а повторная проверка не была проведена
Проектирование поведения после исключения (fail-safe) оказалось недостаточным
Ни система типов, ни контракты не заменяют процесс пересмотра исходных допущений.
Язык — часть инженерии безопасности, но не вся инженерия безопасности целиком.
Пожалуй, это самое честное предостережение, которое стоит держать в голове при изучении Ada.
20. Долгоживущее ПО и Ada — взгляд со стороны сопровождения
На этом сайте мы часто разбираем сопровождение и продление жизни существующих Windows-решений.
С этой точки зрения у Ada есть и другая притягательность.
Системы, написанные на Ada, нередко продолжают работать десятилетиями.
И само проектирование языка Ada рассчитано на долгосрочное сопровождение.
Разделение спецификации (.ads) и реализации (.adb)
-> сопровождающий через 20 лет сможет понять интерфейс, прочитав только спецификацию
Строгие типы и ограничения диапазона
-> неявные допущения остаются в коде, а не передаются устно или через комментарии
Контракты (Pre/Post)
-> «обещания» функции сохраняются в проверяемой форме
Проверка полноты case
-> компилятор сам перечисляет места, затронутые изменением спецификации
Обратная совместимость важна даже при пересмотре стандарта
-> значительная часть кода Ada 83 компилируется современными компиляторами
Всё это можно напрямую переносить как принципы проектирования и при долгосрочном сопровождении систем на C# или C++.
Определять осмысленные типы (тип для ID, тип с единицей измерения) вместо голого int
Проектировать типы, для которых невозможно создать некорректное значение (проверка в конструкторе)
Осознанно разделять публичный интерфейс и реализацию
Выражать предусловия и постусловия через assert-ы и тесты
Писать switch по enum исчерпывающе и относиться к предупреждениям как к ошибкам
Даже если вам никогда не доведётся использовать Ada в работе, изучать её философию проектирования по-прежнему стоит.
Как учебный материал для того, чтобы почувствовать, что значит «выражать проектные решения через типы», Ada и сегодня остаётся первоклассным примером.
21. Итоги
Мы разобрали притягательность Ada.
Подведём итоги.
Ada — работающий язык, который уже более 40 лет используется в высоконадёжных системах
Название происходит от имени Ada Lovelace, актуальный стандарт — Ada 2022
Типы с одинаковой структурой, но разными именами — разные типы; смешение единиц становится ошибкой компиляции
Ограничения диапазона предотвращают некорректные значения на уровне типа
Массивы проверяются по границам, переполнение буфера не превращается в неопределённое поведение
Пакеты разделяют спецификацию и реализацию, а режимы параметров явно показывают направление потока данных
Дженерики фиксируют требуемые операции прямо в спецификации, поэтому ошибки использования становятся очевидны
Контракты (Pre/Post) в Ada 2012 сохраняют спецификацию в коде в проверяемой форме
Задачи (task) и защищённые объекты позволяют безопасно писать параллелизм как встроенную возможность языка
С помощью SPARK контракты можно поднять с проверок времени выполнения до математического доказательства
Благодаря GNAT и Alire язык можно сразу и бесплатно попробовать даже в Windows
Слабые стороны — небольшая экосистема и нехватка специалистов
Механизмы безопасности языка не заменяют процесс пересмотра исходных допущений
С точки зрения популярности Ada так и не стала массовым языком.
Но многое из того, что современные языки преподносят как «новые возможности» — null-безопасность, проверка полноты, контракты, строгость, близкая к владению (ownership), — Ada имела уже десятилетия назад.
Суть Ada можно свести к одной фразе.
Баги — это не то, что нужно находить; это то, что типы и контракты делают «невозможным написать».
Попробуйте на выходных создать в Alire один проект и написать небольшую программу, пока компилятор вас ругает.
Когда вы поймёте, что каждая из этих ошибок компиляции — это «баг, пойманный до того, как он стал бы сбоем в продакшене», притягательность Ada станет для вас по-настоящему понятной.
Справочные материалы
- Reference code collection for this article, organized by chapter - komurasoft-blog-samples (GitHub)
- Ada Programming Language - AdaCore
- Learn Ada - AdaCore (learn.adacore.com)
- Introduction to Ada - learn.adacore.com
- Ada Reference Manual (Ada 2022)
- Alire - Ada Library Repository
- GNAT User’s Guide - GCC
- SPARK - AdaCore
- Introduction to SPARK - learn.adacore.com
- Ada Conformity Assessment Authority
- Ariane 501 Inquiry Board Report (ESA)
Похожие статьи
Недавние статьи с теми же тегами помогут подробнее изучить близкие темы.
Дженерики в Ada ── контракты через типы и повторное использование без накладных расходов
Систематическое руководство по обобщённому программированию в Ada: обобщённые подпрограммы и пакеты, формальные параметры-подпрограммы, к...
Введение в формальную верификацию с SPARK ── От контрактов Ada к математическому доказательству
Практическое введение в формальную верификацию с помощью SPARK — подмножества языка Ada. В статье рассматривается переход от контрактов (...
Программирование систем реального времени на Ada — приоритеты, периодичность и контроль времени выполнения на практике
Изучаем Annex D Ada (системы реального времени) на 8 практических примерах кода: приоритеты задач, протокол Ceiling_Locking, периодическо...
Безопасная конкурентность в Ada — практическое руководство по задачам и защищённым объектам
Вводная статья о встроенной в язык Ada конкурентности — задачах и защищённых объектах. Рассматриваем рандеву (entry/accept), выборочный a...
Обработка ошибок и повторные попытки в Power Automate — как не допустить, чтобы работающий поток незаметно остановился
Сборник паттернов проектирования, которые не дают потокам Power Automate незаметно останавливаться: значения политики повторов по умолчан...
Связанные темы
Эти страницы показывают тему статьи в более широком контексте услуг и решений.
Технические темы Windows
Раздел о разработке Windows, расследовании сбоев и использовании существующих активов.
Частые вопросы
Вопросы, которые часто возникают при консультациях по теме статьи.
- Используется ли язык Ada сегодня?
- Да, используется. Ada десятилетиями применяется в высоконадёжных системах, где ошибка напрямую угрожает человеческим жизням или ведёт к огромным потерям: в системах управления полётом гражданских самолётов, в авиадиспетчерских системах, в системах сигнализации и обеспечения безопасности на железных дорогах, в ракетах и искусственных спутниках, в оборонных системах, в медицинском оборудовании. Ada — язык, который пересматривается уже более 40 лет: начиная с Ada 83 в 1983 году, через Ada 95, Ada 2005 и Ada 2012, до актуального стандарта Ada 2022.
- Чем строгая типизация в Ada отличается от других языков?
- В Ada типы, объявленные под разными именами, считаются разными типами, даже если их структура полностью совпадает. Например, если типы Meters и Seconds оба созданы на основе Float, смешать их в одном выражении нельзя — это ошибка компиляции, а преобразование нужно писать явно. Кроме того, через subtype тип можно снабдить ограничением диапазона значений (например, 0–100), и его нарушение во время выполнения приводит к исключению Constraint_Error. Такая конструкция не полагается на «будьте внимательны» — она устроена так, что ошибки вроде путаницы единиц измерения попросту не дают собрать программу.
- Как бесплатно попробовать Ada?
- Полноценную бесплатную среду разработки можно собрать на Windows, Linux и macOS с помощью GNAT (бесплатного Ada-компилятора, входящего в состав GCC) и Alire (менеджера пакетов и инструмента сборки для Ada, команда alr). Установщик Alire берётся с официального сайта, после чего alr init --bin создаёт шаблон проекта, alr build собирает его, а alr run запускает — опыт, близкий к cargo в Rust. Сам компилятор устанавливать вручную не нужно: тулчейн тоже подтягивает Alire. Для VS Code есть расширение Ada от AdaCore.
- В чём слабые стороны Ada?
- Экосистема невелика: вариантов веб-фреймворков, GUI-библиотек и облачных SDK меньше, чем у основных языков. Специалистов и информации, особенно на русском языке, мало, поэтому при внедрении в команду нужно закладывать расходы на обучение. Объявление типов и разделение спецификации и тела ощущаются избыточными для небольших скриптов. Рынок труда смещён в сторону авиакосмической отрасли, обороны и железных дорог. Кроме того, как показала авария ракеты Ariane 5 в 1996 году, механизмы безопасности языка не заменяют процесс пересмотра исходных допущений — об этом стоит помнить.
Об авторе
Страница с профилем автора статьи.
Го Комура
Представитель KomuraSoft LLC
Специализируется на разработке программного обеспечения для Windows, техническом консалтинге и расследовании сбоев, особенно в проектах с унаследованными системами и трудно воспроизводимыми ошибками.
Публичные ссылки