Язык Ада в современной программной индустрии - презентация, доклад, проект скачать

Нажмите для полного просмотра!

Язык Ада в современной программной индустрии, слайд №1

Язык Ада в современной программной индустрии, слайд №2

Язык Ада в современной программной индустрии, слайд №3

Язык Ада в современной программной индустрии, слайд №4

Язык Ада в современной программной индустрии, слайд №5

Язык Ада в современной программной индустрии, слайд №6

Язык Ада в современной программной индустрии, слайд №7

Язык Ада в современной программной индустрии, слайд №8

Язык Ада в современной программной индустрии, слайд №9

Язык Ада в современной программной индустрии, слайд №10

Язык Ада в современной программной индустрии, слайд №11

Язык Ада в современной программной индустрии, слайд №12

Язык Ада в современной программной индустрии, слайд №13

Язык Ада в современной программной индустрии, слайд №14

Язык Ада в современной программной индустрии, слайд №15

Язык Ада в современной программной индустрии, слайд №16

Язык Ада в современной программной индустрии, слайд №17

Язык Ада в современной программной индустрии, слайд №18

Язык Ада в современной программной индустрии, слайд №19

Язык Ада в современной программной индустрии, слайд №20

Язык Ада в современной программной индустрии, слайд №21

Язык Ада в современной программной индустрии, слайд №22

Язык Ада в современной программной индустрии, слайд №23

Язык Ада в современной программной индустрии, слайд №24

Язык Ада в современной программной индустрии, слайд №25

Язык Ада в современной программной индустрии, слайд №26

Язык Ада в современной программной индустрии, слайд №27

Язык Ада в современной программной индустрии, слайд №28

Содержание ▲

Вы можете ознакомиться и скачать презентацию на тему Язык Ада в современной программной индустрии. Доклад-сообщение содержит 28 слайдов. Презентации для любого класса можно скачать бесплатно. Если материал и наш сайт презентаций Mypresentation Вам понравились – поделитесь им с друзьями с помощью социальных кнопок и добавьте в закладки в своем браузере.

Слайды и текст этой презентации

Слайд 1

Описание слайда:

Слайд 2

Описание слайда:

О чем пойдет речь… Язык Ада: современное состояние и использование в программной индустрии. Система программирования GNAT и компания AdaCore. Технологические решения на основе Ады. Вопросы?

Слайд 3

Описание слайда:

Ада – прошлое, настоящее, будущее… «Золотой век» Ады: конец 70-х – середина 90-х годов прошлого века. Уверенно себя чувствует в своей нише: Авиация (встроенное ПО и системы управления воздушным движением); Финансы; Транспорт; Связь и телекоммуникации; Атомная энергетика; Космос; Медицина; ... Тенденция к расширению ниши

Слайд 4

Описание слайда:

Ада – кто сейчас ее использует Alenia Alstom Transport Ansaldo STS Atos Origin AWE BAE Systems Boeing EADS European Space Agency Eurocontrol IPESOFT JEOL Lockheed Martin MBDA Philips Semiconductor Raytheon Rockwell Collins SAAB General Electric Thales

Слайд 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 N mod X = 0); Возможность определять технологическое подмножество языка; pragma Restrictions (No_Tasking); pragma Profile (Ravenscar); И много еще всякого-разного …

Слайд 10

Описание слайда:

Ада и разработка встроенных приложений Ада изначально ориентирована на разработку встроенных систем: Все, что можно, сдвинуто на этап компиляции и сборки программы; Спецификации представления – управление машинно-зависимыми аспектами (задание адресов объектов, размера значений, расположения составных данных в памяти и т.п.); Интерфейс с другими языками; И все это – не выходя за рамки стандарта языка!

Слайд 11

Описание слайда:

Ада - реализации GNAT – AdaCore; GNAT – FSF; GNAT – от всех, кому не лень; Старые игроки (Rational, Aonix, DDC-I, Green Hills) все еще в деле, но…

Слайд 12

Описание слайда:

Компания AdaCore ( Образована в 1994 году преподавателями Нью-Йоркского университета; В настоящее время – более 100 сотрудников, головные офисы в Париже и Нью-Йорке; Занимается разработкой и сопровождением GNAT-технологии; Основной продукт компании – подписка на оказание технической поддержки для пользователей GNAT-технологии;

Слайд 13

Описание слайда:

GNAT = Gnu Nyu Ada Translator

Слайд 14

Описание слайда:

GNAT – позволяет создавать код для:

Слайд 15

Описание слайда:

Компилятор 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: Оценка максимальной глубины стека в целевой среде; Выявление потенциально опасных ситуаций; Работает с кодом на Аде, С, С++.

Слайд 23

Описание слайда:

Разработка сертифицированных приложений Сертифицированные библиотеки периода выполнения; Предоставление квалификационных материалов для (части) предлагаемых инструментов и решений;

Слайд 24

Описание слайда:

Автоматическая генерация Ада-кода на основе моделей QGen: Поддерживается надежное подмножество Simulink® and Stateflow®; Проверка корректности модели; Возможность проследить путь от модели к коду; Генерация кода на SPARK и MISRA C; Цель – полностью квалифицированная технология для использования там, где действуют стандарты безопасности;

Слайд 25

Описание слайда:

SPARK – формальная верификация программ С чего начался SPARK: (Успешная!) попытка практической реализации идеи формального доказательства корректности программы; Использование булевских аннотаций для компонент кода на Аде в виде комментариев специального вида (пред- и пост-условия для подпрограмм, инварианты циклов, произвольные утверждения); Крайне ограниченное подмножество Ады; Бескомпромиссный подход «всё или ничего»; Несколько успешных индустриальных проектов; Развитие SPARK-технологии: Аннотации, инварианты, утверждения стали исполняемыми компонентами кода на Аде; Новые способы аннотации; Существенно расширилось подмножество Ады; Более гибкий подход – комбинация: Формального доказательства корректности программных модулей (возможно, не всех); тестирования; обнаружения потенциальных проблем (или доказательства их отсутствия!); Как результат – намного более широкое использование в индустрии;

Слайд 26

Описание слайда:

Контракт как ключевая идея 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, будет возбуждено исключение