Презентация Язык Ада в современной программной индустрии онлайн
На нашем сайте вы можете скачать и просмотреть онлайн доклад-презентацию на тему Язык Ада в современной программной индустрии абсолютно бесплатно. Урок-презентация на эту тему содержит всего 28 слайдов. Все материалы созданы в программе PowerPoint и имеют формат ppt или же pptx. Материалы и темы для презентаций взяты из открытых источников и загружены их авторами, за качество и достоверность информации в них администрация сайта не отвечает, все права принадлежат их создателям. Если вы нашли то, что искали, отблагодарите авторов - поделитесь ссылкой в социальных сетях, а наш сайт добавьте в закладки.
Презентации » Устройства и комплектующие » Язык Ада в современной программной индустрии
Оцените!
Оцените презентацию от 1 до 5 баллов!
- Тип файла:ppt / pptx (powerpoint)
- Всего слайдов:28 слайдов
- Для класса:1,2,3,4,5,6,7,8,9,10,11
- Размер файла:138.52 kB
- Просмотров:158
- Скачиваний:1
- Автор:неизвестен
Слайды и текст к этой презентации:
№3 слайд
Содержание слайда: Ада – прошлое, настоящее, будущее…
«Золотой век» Ады: конец 70-х – середина 90-х годов прошлого века.
Уверенно себя чувствует в своей нише:
Авиация (встроенное ПО и системы управления воздушным движением);
Финансы;
Транспорт;
Связь и телекоммуникации;
Атомная энергетика;
Космос;
Медицина;
...
Тенденция к расширению ниши
№5 слайд
Содержание слайда: Ада – стандартизация
Ада возникла как стандарт ANSI (1983), утверженный как стандарт ISO (1987).
Правила ISO требуют пересматривать информационный стандарты раз в 10 лет, Ада – единственный язык, следующий этому правилу: 1987 => 1995 => 2005 => 2012 (последняя официальная ревизия стандарта) => 202X (в процессе разработки)
Опережающая стандартизация +мощные средства контроля реализаций = отсутствие версий и диалектов языка.
№6 слайд
Содержание слайда: Ада и Оберон – что у них общего?
Ада и Оберон – близкие родственники, у них общий дедушка (Виртовский Паскаль).
Общая философия:
Забота о надежности на всех этапах жизненного цикла ПО:
Строгая типизация, отсутствие умолчаний, «все, что не разрешено – запрещено»;
Сопоставимый набор предоставляемых возможностей;
Похожий (понятный и легко читаемый!) синтаксис;
№7 слайд
Содержание слайда: Ада и Оберон – в чем разница?
Принцип сундука и принцип чемоданчика
(Кауфман В.Ш. «Языки программирования. Концепции и принципы» ДМК Пресс, 2011)
«Принцип чемоданчика»: небольшой набор абсолютно необходимых инструментов, все остальное сделаем сами по месту => Оберон
«Принцип сундука»: для каждой базовой (да и вообще важной) технологической потребности должно быть готовое решение или легко настраиваемый полуфабрикат => Ада
№8 слайд
Содержание слайда: Что есть интересного в Адском сундуке?
Управление асинхронными процессами;
Иерархическая модульность;
Механизм подтипов (вплоть до определения произвольных множеств) и механизм исключений;
subtype Basic_Letter is Character
with Static_Predicate => Basic_Letter in 'A'..'Z' | 'a'..'z' | 'Æ’
| 'æ' | 'Ð' | 'ð’ | 'Þ' | 'þ' | 'ß';
subtype Even_Integer is Integer
with Dynamic_Predicate => Even_Integer mod 2 = 0,
Predicate_Failure =>
"Even_Integer must be a multiple of 2";
Атрибуты как средство запросить свойства сущностей и аспекты как средство задать свойства сущностей (от размера переменной до пред- и пост-условий для подпрограммы)
№9 слайд
Содержание слайда: Что есть интересного в Адском сундуке?
Исполняемые спецификации (предикаты, пред- и пост-условия, инварианты);
Кванторы всеобщности и существования в логическом выражении;
-- постусловие для подпрограммы, параметром которой является
-- тип-массив А с типом индекса Т (требование упорядоченности
-- результата):
Post => (A'Length < 2 or else
(for all I in A'First .. T'Pred(A'Last) => A (I) <= A (T'Succ (I))))
pragma Assert (for some X in 2 .. N / 2 => N mod X = 0);
Возможность определять технологическое подмножество языка;
pragma Restrictions (No_Tasking);
pragma Profile (Ravenscar);
И много еще всякого-разного …
№10 слайд
Содержание слайда: Ада и разработка встроенных приложений
Ада изначально ориентирована на разработку встроенных систем:
Все, что можно, сдвинуто на этап компиляции и сборки программы;
Спецификации представления – управление машинно-зависимыми аспектами (задание адресов объектов, размера значений, расположения составных данных в памяти и т.п.);
Интерфейс с другими языками;
И все это – не выходя за рамки стандарта языка!
№12 слайд
Содержание слайда: Компания AdaCore (www.adacore.com)
Образована в 1994 году преподавателями Нью-Йоркского университета;
В настоящее время – более 100 сотрудников, головные офисы в Париже и Нью-Йорке;
Занимается разработкой и сопровождением GNAT-технологии;
Основной продукт компании – подписка на оказание технической поддержки для пользователей GNAT-технологии;
№16 слайд
Содержание слайда: GNAT-технология
Не только компилятор Ады (поддерживается последняя версия стандарта), но и:
Компиляторы С и С++;
Специализированные библиотеки;
Инструментарий;
Технологические решения;
SPARK (доказательное программирование);
QGen (автоматическая генерация кода по моделям);
…
№17 слайд
Содержание слайда: AdaCore - продукты
GNAT Pro:
Полноценная техническая поддержка;
Возможность создавать программы с закрытым кодом;
Все платформы и все целевые среды, весь инструментарий, все компоненты технологии;
GNAT Developer:
Незначительно ограниченная техническая поддержка;
Возможность создавать программы с закрытым кодом;
Незначительные ограничения на поддерживаемые конфигурации;
GAP (GNAT Academic Program):
Ограниченная техническая поддержка;
Возможность создавать программы только под лицензией GPL;
Все инструментальные платформы + MINDSTORMS NTX robotic + базовый инструментарий;
Бесплатно для университетов;
GNAT GPL:
То же, что и GAP, но вообще без техподдержки и бесплатно абсолютно для всех;
№18 слайд
Содержание слайда: AdaCore – технологические решения
Разработка и тестирование встроенных приложений;
Поддержка разработки сертифицированных приложений;
Автоматическая генерация Ада-кода на основе моделей;
Формальная верификация программ, или корректность по построению;
Обучение, консультации, развитие технологии на основе явных заказов пользователей;
№19 слайд
Содержание слайда: Разработка и тестирование встроенных приложений
Конфигурируемые библиотеки периода выполнения:
Ravenscar profile;
Zero footprint;
Bare board (возможность создавать приложения при отсутствии ОС в целевой среде);
gnat emulator – возможность тестировать встроенное приложение не в целевой, а в инструментальной среде;
№20 слайд
Содержание слайда: Разработка сертифицированных приложений
Поддержка разработки систем, удовлетворяющих отраслевым стандартам качества:
DO-178 (встроенные авиационные системы);
EN 50128 (железные дороги);
RTCA DO-278 (управление воздушным движением);
ECSS-E-ST-40C, ECSS-Q-ST-80C – космическая техника;
...
№21 слайд
Содержание слайда: Разработка сертифицированных приложений
Поддержка тестирования:
gnatcoverage: автоматическая проверка выполнения критериев структурного тестирования (как на уровне объектного кода, так и на уровне исходного кода на языках Ада и С);
gnattest: автоматическая генерация тестовых драйверов для выполнения модульного тестирования в среде aunit;
Traceability analysis package:
рекомендации по выбору языкового подмножества, позволяющего проследить соответствие исходного и объектного кода, и нужных режимов компилятора;
набор тестов, демонстрирующих соответствие исходного и объектного кода в пределах выбранного подмножества;
№22 слайд
Содержание слайда: Разработка сертифицированных приложений
Инструменты статического анализа кода:
gnatcheck:
Проверка правил, типичных для стандарта кодирования;
Интеграция результатов проверок, проводимых компилятором, в итоговый отчет;
Позволяет быстро добавлять новые правила по заказу пользователей;
Codepeer:
Детальный анализ графа управления и графа потока данных (деление на ноль, переполнение, неопределенные и неиспользуемые переменные и т.п.);
gnatstack:
Оценка максимальной глубины стека в целевой среде;
Выявление потенциально опасных ситуаций;
Работает с кодом на Аде, С, С++.
№24 слайд
Содержание слайда: Автоматическая генерация Ада-кода на основе моделей
QGen:
Поддерживается надежное подмножество Simulink® and Stateflow®;
Проверка корректности модели;
Возможность проследить путь от модели к коду;
Генерация кода на SPARK и MISRA C;
Цель – полностью квалифицированная технология для использования там, где действуют стандарты безопасности;
№25 слайд
Содержание слайда: SPARK – формальная верификация программ
С чего начался SPARK:
(Успешная!) попытка практической реализации идеи формального доказательства корректности программы;
Использование булевских аннотаций для компонент кода на Аде в виде комментариев специального вида (пред- и пост-условия для подпрограмм, инварианты циклов, произвольные утверждения);
Крайне ограниченное подмножество Ады;
Бескомпромиссный подход «всё или ничего»;
Несколько успешных индустриальных проектов;
Развитие SPARK-технологии:
Аннотации, инварианты, утверждения стали исполняемыми компонентами кода на Аде;
Новые способы аннотации;
Существенно расширилось подмножество Ады;
Более гибкий подход – комбинация:
Формального доказательства корректности программных модулей (возможно, не всех);
тестирования;
обнаружения потенциальных проблем (или доказательства их отсутствия!);
Как результат – намного более широкое использование в индустрии;
№27 слайд
Содержание слайда: Почему это назвали контрактом?
Если вызывающий контекст гарантирует, что предусловие вызываемой подпрограммы истинно, то подпрограмма обеспечивает истинность пост-условия по завершению вызова;
Все пред- и пост-условия вычисляются как часть вызова подпрограммы, и если что-либо не оказывается истинным – возбуждается исключение;
№28 слайд
Содержание слайда: Инварианты типов (вишенка на торте :)
package Stacks is
type Stack is private
with
Type_Invariant => Is_Unduplicated (Statck);
function Is_Empty (S : Stack) return Boolean;
function Is_Full (S : Stack) return Boolean;
function Is_Unduplicated (S : Stack) return Boolean;
procedure Push (S : in out Stack; X : Integer);
with
Pre => not Is_Full (S);
Post => Is_Empty (S);
...
end Statcks;
...
Var : Stack;
...
Push (Var, 13);
-- Is_Unduplicated будет вызвана сразу же после завершения этого вызова,
-- и если результатом будет FALSE, будет возбуждено исключение
Скачать все slide презентации Язык Ада в современной программной индустрии одним архивом:
-
«Решение задач на языке программирования» (Подготовка к ОГЭ)
-
Сравнение современных языков программирования
-
Программирование на языке PascalABC. Решение задач. Обмен значений
-
Универсальный современный популярный язык программирования
-
Язык программирования Паскаль. Решение задач
-
Кроссплатформенный фреймворк для разработки программного обеспечения на языке программирования C
-
Этапы решения задач на компьютере. Язык программирования Паскаль
-
«Я – программист», или немного о современных профессиях в индустрии информационных технологий
-
Современные языки программирования семейства СиСи
-
ОГЭ по информатике. Решение заданий 20. 1 с помощью алгоритмического языка в среде Кумир. Исполнитель Робот