Учебник Ada для начинающих

Программа курса

1. 1 Что такое Ada и философия надёжности

   1. Зачем понадобился ещё один язык: история и заказ DoD

      Как Министерство обороны США в 1970-х пришло к идее единого языка, требования Steelman и конкурс, породивший Ada в честь Ады Лавлейс.

   2. Эволюция языка: от Ada 83 до Ada 2022

      Четыре крупных ревизии стандарта Ada: ООП в 95, контракты в 2012, параллелизм в 2022 — что и зачем добавляли, сохраняя совместимость.

   3. Где живёт Ada: авионика, космос, железные дороги, медицина

      Реальные системы на Ada: Boeing 777, Ariane, метро, кардиостимуляторы. Почему критичные отрасли с высокой ценой отказа выбирают этот язык.

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

      Свободный компилятор GNAT на базе GCC, инструменты AdaCore и SPARK — подмножество Ada для математического доказательства корректности.

2. 2 Основы языка

   1. Структура программы: главная процедура, with и use

      Анатомия программы на Ada: где точка входа, почему главная единица — процедура, и как with/use подключают пакеты стандартной библиотеки.

   2. Переменные, константы и присваивание :=

      Объявление переменных с обязательным типом, инициализация, неизменяемые константы и почему присваивание обозначается := а не =.

   3. Базовый ввод-вывод: семейство Text_IO

      Печать строк через Put и Put_Line, вывод чисел специализированными пакетами, преобразование Image и базовое чтение Get_Line.

   4. Стандартная библиотека и первая полноценная программа

      Обзор иерархии Ada: Numerics, Calendar, Containers, Strings — и сборка работающей программы с вводом, расчётом и форматированным выводом.

3. 3 Система типов — сердце Ada

   1. Сильная типизация: почему 1 и 1.0 несовместимы

      Скалярные типы Ada и принцип строгой типизации: значения разных типов нельзя смешивать без явного преобразования, и это ловит ошибки рано.

   2. Поддиапазоны и производные типы

      Subtype сужает диапазон, оставаясь совместимым; type ... is new создаёт несовместимый тип, чтобы развести метры и секунды на уровне компилятора.

   3. Перечисления и модульные типы

      Перечисления заменяют магические числа именами, Boolean и Character — тоже перечисления; модульные типы (mod) дают циклическую арифметику для битов и счётчиков.

   4. Атрибуты типов: 'First, 'Last, 'Range, 'Image

      Атрибуты — встроенные запросы свойств типа через апостроф; опора на них вместо вписанных констант делает код устойчивым к изменениям.

4. 4 Управление и подпрограммы

   1. Ветвление: if и case с полным покрытием

      Оператор if с elsif и явным end if, оператор case с обязательным покрытием всех значений, when others и null, сокращённые and then / or else.

   2. Циклы: for, while и loop с exit

      Единая конструкция loop и формы for (по диапазону), while (по условию), loop ... exit; защищённый счётчик и именованные циклы для выхода из вложенности.

   3. Подпрограммы и режимы параметров in/out/in out

      Процедуры и функции, режимы параметров in, out, in out как видимый и проверяемый контракт направления данных, чистые функции и выражения-функции.

   4. Перегрузка, именованные аргументы и условные выражения

      Перегрузка имён по типам и даже по результату, именованные аргументы для читаемых вызовов, значения по умолчанию и выражения if/case, возвращающие значение.

5. 5 Составные типы

   1. Массивы: ограниченные, неограниченные и атрибуты

      Массивы Ada с индексацией любым дискретным типом, атрибуты границ и длины, неограниченные массивы (range box) и проверка границ против переполнения буфера.

   2. Агрегаты: составное значение одним выражением

      Агрегаты задают массив или запись целиком: позиционно, по именам, с диапазонами и others; компилятор проверяет полноту покрытия компонентов.

   3. Записи: поля, дискриминанты и варианты

      Записи объединяют разнородные поля; записи с дискриминантом параметризуют структуру, а вариантные записи меняют набор полей типобезопасно, в отличие от union в C.

   4. Строки: String и Unbounded_String

      String как массив символов фиксированной длины со срезами и атрибутами, Unbounded_String для текста переменной длины и осознанный выбор между ними.

6. 6 Пакеты и инкапсуляция

   1. Пакеты: спецификация и тело

      Спецификация и тело пакета в Ada: как разделить видимый контракт и скрытую реализацию, раздельная компиляция, директива use и инкапсуляция состояния.

   2. Приватные типы: абстрактные типы данных

      Приватные типы Ada (private): абстрактные типы данных с скрытым представлением, видимая и приватная части спецификации, операции по умолчанию, много экземпляров.

   3. Ограниченные приватные типы (limited private)

      Ограниченные приватные типы Ada (limited private): запрет присваивания и сравнения, защита уникальных ресурсов, build-in-place и расширенный return, аналогия с move-семантикой.

   4. Дочерние пакеты и инициализация

      Дочерние пакеты Ada (Parent.Child): расширение родителя с доступом к его приватной части, иерархии библиотек, приватные потомки и порядок инициализации (elaboration).

7. 7 Надёжность: исключения и контракты

   1. Исключения: обработка нештатных ситуаций

      Исключения в Ada: raise, раздел exception и when, своё исключение с сообщением, Ada.Exceptions, сворачивание стека, zero-cost модель и идиомы безопасной обработки ошибок.

   2. Проверки времени выполнения и Constraint_Error

      Предопределённые проверки Ada: границы массивов, диапазоны подтипов, переполнение, разыменование null. Constraint_Error, узкие подтипы, модульные типы и атрибуты 'Range/'Valid.

   3. Контракты Ada 2012: Pre, Post, инварианты

      Контракты Ada 2012: предусловия Pre, постусловия Post с 'Result/'Old/for all, Type_Invariant и предикаты подтипов, Design by Contract и связь с формальной верификацией SPARK.

   4. Обзор SPARK: формальная верификация

      SPARK — верифицируемое подмножество Ada: GNATprove доказывает отсутствие ошибок времени выполнения и соответствие контрактам для всех входов, аспекты Global/Depends, уровни Stone–Platinum.

8. 8 Обобщённое программирование (generics)

   1. Generic-пакеты и подпрограммы: основы

      Обобщённые единицы Ada: generic-пакеты и подпрограммы как шаблоны, инстанцирование через new, независимые экземпляры, типобезопасность и двусторонняя проверка по контракту параметров.

   2. Формальные параметры: типы, значения, операции

      Формальные параметры generic в Ada: лесенка формальных типов (private, (<>), range <>), формальные значения и формальные подпрограммы (with function), умолчания is <> и проверка по контракту.

   3. Инстанцирование и переиспользуемые компоненты

      Инстанцирование generic в Ada как композиция: экземпляр-библиотека, формальные пакеты (with package), вложение обобщённых единиц и стандартные контейнеры Ada.Containers.Vectors.

   4. Generics против ООП: два полиморфизма

      Generics как основа переиспользуемых компонентов Ada: статический против динамического полиморфизма, паттерны (Итератор, Стратегия) через обобщения, границы подхода и сочетание с ООП.

9. 9 Параллелизм, встроенный в язык

   1. Задачи (task): параллелизм как часть языка

      Задачи Ada (task): встроенный в язык параллелизм, спецификация и тело задачи, автоматический запуск, структурированная зависимость, delay и отображение на потоки ОС или голое железо.

   2. Рандеву: entry, accept и select

      Рандеву в Ada: точки входа entry, оператор accept, синхронная встреча задач, select со сторожевыми условиями и terminate, таймированные и условные вызовы, модель в духе CSP.

   3. Защищённые объекты, очереди и барьеры

      Защищённые объекты Ada (protected): встроенный монитор, function/procedure/entry, автоматическое взаимное исключение, барьеры входов (when) для условной синхронизации, сравнение с рандеву.

   4. Ravenscar-профиль для реального времени

      Ravenscar-профиль Ada: детерминированное подмножество задач для жёсткого реального времени, pragma Profile, delay until для периодичности, протокол потолка приоритета и анализ планируемости.

10. 10 ООП и системное программирование

    1. Тэгированные типы: основа ООП

       Тэгированные типы Ada (tagged): объекты с рантайм-тегом, примитивные операции как методы, точечная нотация, атрибут 'Tag и Ada.Tags, таблица диспетчеризации под капотом.

    2. Наследование, диспетчеризация и интерфейсы

       Наследование и полиморфизм в Ada: расширение типа (new ... with record), overriding, class-wide типы 'Class и динамическая диспетчеризация, абстрактные типы и интерфейсы без ромбовидной проблемы.

    3. Access-типы, безопасность и представление данных

       Системное программирование в Ada: access-типы как безопасные указатели (accessibility, storage pools, без адресной арифметики), Unchecked_Deallocation и владение, rep clauses для точной раскладки битов.

    4. Интероп с C и итог по верификации

       Интероп Ada с C (Import/Export, Convention => C, Interfaces.C) и итог курса: эшелонированная надёжность от типов и контрактов до формальной верификации SPARK/GNATprove для критичных систем.