Подробнее
Курсы
Введение в язык Ада
Введение
История
Ада сегодня
Философия
SPARK
Императивы языка
Hello world
Условный оператор
Циклы
Циклы for
Простой цикл
Циклы while
Оператор выбора
Зоны описания
Условные выражения
Условное выражение
Выражение выбора
Подпрограммы
Подпрограммы
Вызовы подпрограмм
Вложенные подпрограммы
Вызов функций
Виды параметров
Вызов процедуры
Параметры in
Параметры in out
Параметры out
Предварительное объявление подпрограмм
Переименование
Модульное программирование
Пакеты
Использование пакета
Тело пакета
Дочерние пакеты
Дочерний пакет от дочернего пакета
Множественные потомки
Видимость
Переименование
Сильно типизированный язык
Что такое тип?
Целочисленные типы - Integers
Семантика операций
Беззнаковые типы
Перечисления
Типы с плавающей запятой
Основные свойства
Точность типов с плавающей запятой
Диапазон значений для типов с плавающей запятой
Строгая типизация
Производные типы
Подтипы
Подтипы в качестве псевдонимов типов
Записи
Объявление типа записи
Агрегаты
Извлечение компонент
Переименование
Массивы
Объявление типа массива
Доступ по индексу
Более простые объявления массива
Атрибут диапазона
Неограниченные массивы
Предопределенный тип String
Ограничения
Возврат неограниченных массивов
Объявление массивов (2)
Отрезки массива
Переименование
Подробнее о типах
Агрегаты: краткая информация
Cовмещение и квалифицированные выражения
Символьные типы
Ссылочные типы
Введение
Выделение (allocation) памяти
Извлечение по ссылке
Другие особенности
Взаимно рекурсивные типы
Подробнее о записях
Типы записей динамически изменяемого размера
Записи с дискриминантом
Записи c вариантами
Типы с фиксированной запятой
Десятичные типы с фиксированной запятой
Обычные типы с фиксированной запятой
Изоляция
Простейшая инкапсуляция
Абстрактные типы данных
Лимитируемые типы
Дочерние пакеты и изоляция
Настраиваемые модули
Введение
Объявление формального типа
Объявление формального объекта
Определение тела настраиваемого модуля
Конкретизация настройки
Настраиваемые пакеты
Формальные подпрограммы
Пример: конкретизация ввода/вывода
Пример: АТД
Пример: Обмен
Пример: Обратный порядок элементов
Пример: Тестовое приложение
Исключения
Объявление исключения
Возбуждение исключения
Обработка исключения
Предопределенные исключения
Управление задачами
Задачи
Простая задача
Простая синхронизация
Оператор задержки
Синхронизация: рандеву
Обрабатывающий цикл
Циклические задачи
Защищенные объекты
Простой объект
Входы
Задачные и защищенные типы
Задачные типы
Защищенные типы
Контрактное проектирование
Пред- и постусловия
Предикаты
Инварианты типа
Взаимодействие с языком C
Многоязычный проект
Соглашение о типах
Подпрограммы на других языках
Вызов подпрограмм C из Ады
Вызов Ада подпрограмм из C
Внешние переменные
Использование глобальных переменных C в Аде
Использование переменных Ада в C
Автоматическое создание связок
Адаптация связок
Объектно-ориентированное программирование
Производные типы
Теговые типы
Надклассовые типы
Операции диспетчеризации
Точечная нотация
Личные и лимитируемые типы с тегами
Надклассовые ссылочные типы
Стандартная библиотека: Контейнеры
Векторы
Создание экземпляра
Инициализация
Добавление элементов
Доступ к первому и последнему элементам
Итерация
Поиск и изменение элементов
Вставка элементов
Удаление элементов
Другие операции
Множества
Инициализация и итерация
Операции с элементами
Другие операции
Отображения для неопределенных типов
Хэшированные отображения
Упорядоченные отображения
Сложность
Стандартная библиотека: Дата и время
Обработка даты и времени
Задержка с использованием даты
Режим реального времени
Анализ производительности
Стандартная библиотека: Строки
Операции со строками
Ограничение строк фиксированной длины
Ограниченные строки
Неограниченные строки
Стандартная библиотека: Файлы и потоки
Текстовый ввод-вывод
Последовательный ввод-вывод
Прямой ввод-вывод
Потоковый ввод-вывод
Стандартная библиотека: Numerics
Элементарные функции
Генерация случайных чисел
Комплексные числа
Работа с векторами и матрицами
Приложения
Приложение A: Формальные типы настройки
Неопределенные версии типов
Приложение B: Контейнеры
Безопасное и надежное программное обеспечение
Вступление
Предисловие
Безопасный синтаксис
Присваивание и проверка на равенство
Группы инструкций
Именованное сопоставление
Целочисленные литералы
Безопасные типы данных
Использование индивидуальных типов
Перечисления и целые
Ограничения и подтипы
Предикаты подтипов
Массивы и ограничения
Установка начальных значений по умолчанию
«Вещественные ошибки»
Безопасные указатели
Ссылки, указатели и адреса
Ссылочные типы и строгая типизация
Ссылочные типы и контроль доступности
Ссылки на подпрограммы
Вложенные подпрограммы в качестве параметров
Безопасная архитектура
Спецификация и тело пакета
Приватные типы
Контрактная модель настраиваемых модулей
Дочерние модули
Модульное тестирование
Взаимозависимые типы
Контрактное программирование
Безопасное объектно‐ориентированное программирование
ООП вместо структурного программирования
Индикатор overriding
Запрет диспетчеризации вызова подпрограмм
Интерфейсы и множественное наследование
Взаимозаменяемость
Безопасное создание объектов
Переменные и константы
Функция-конструктор
Лимитируемые типы
Контролируемые типы
Безопасное управление памятью
Переполнение буфера
Динамическое распределение памяти
Пулы памяти
Ограничения
Безопасный запуск
Предвыполнение
Директивы компилятору, связанные с предвыполнением
Динамическая загрузка
Безопасная коммуникация
Представление данных
Корректность данных
Взаимодействие с другими языками
Потоки ввода/вывода
Фабрики объектов
Безопасный параллелизм
Операционные системы и задачи
Защищенные объекты
Рандеву
Ограничения
Ravenscar
Безопасное завершение
Время и планирование
Сертификация с помощью SPARK
Контракты
SPARK — подмножество языка Ада
Формальные методы анализа
Гибридная верификация
Примеры
Сертификация
Дальнейший процесс
Заключение
Список литературы
Please activate JavaScript to enable the search functionality.