Разделы презентаций


Сергей Рыбин, Октябрь 2018, Орел rybin@adacore.com Язык Ада в современной

Содержание

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

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

Слайд 1Сергей Рыбин,
Октябрь 2018, Орел
rybin@adacore.com
Язык Ада в современной программной индустрии.

Сергей Рыбин,Октябрь 2018, Орелrybin@adacore.comЯзык Ада в современной программной индустрии.

Слайд 2Язык Ада: современное состояние и использование в программной индустрии.
Система программирования

GNAT и компания AdaCore.
Технологические решения на основе Ады.
Вопросы?

О чем пойдет

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

Слайд 3«Золотой век» Ады: конец 70-х – середина 90-х годов прошлого

века.
Уверенно себя чувствует в своей нише:
Авиация (встроенное ПО и системы

управления воздушным движением);
Финансы;
Транспорт;
Связь и телекоммуникации;
Атомная энергетика;
Космос;
Медицина;
...
Тенденция к расширению ниши

Ада – прошлое, настоящее, будущее…

«Золотой век» Ады: конец 70-х – середина 90-х годов прошлого века.Уверенно себя чувствует в своей нише:Авиация (встроенное

Слайд 4Alenia
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

Ада – кто сейчас ее использует

AleniaAlstom TransportAnsaldo STSAtos OriginAWEBAE SystemsBoeingEADSEuropean Space AgencyEurocontrolIPESOFTJEOLLockheed MartinMBDAPhilips SemiconductorRaytheonRockwell CollinsSAABGeneral ElectricThalesАда – кто сейчас ее использует

Слайд 5Ада возникла как стандарт ANSI (1983), утверженный как стандарт ISO

(1987).
Правила ISO требуют пересматривать информационный стандарты раз в 10 лет,

Ада – единственный язык, следующий этому правилу: 1987 => 1995 => 2005 => 2012 (последняя официальная ревизия стандарта) => 202X (в процессе разработки)
Опережающая стандартизация +мощные средства контроля реализаций = отсутствие версий и диалектов языка.

Ада – стандартизация

Ада возникла как стандарт ANSI (1983), утверженный как стандарт ISO (1987).Правила ISO требуют пересматривать информационный стандарты раз

Слайд 6Ада и Оберон – близкие родственники, у них общий дедушка

(Виртовский Паскаль).
Общая философия:
Забота о надежности на всех этапах жизненного цикла

ПО:
Строгая типизация, отсутствие умолчаний, «все, что не разрешено – запрещено»;
Сопоставимый набор предоставляемых возможностей;
Похожий (понятный и легко читаемый!) синтаксис;

Ада и Оберон – что у них общего?

Ада и Оберон – близкие родственники, у них общий дедушка (Виртовский Паскаль).Общая философия:Забота о надежности на всех

Слайд 7Принцип сундука и принцип чемоданчика (Кауфман В.Ш. «Языки программирования. Концепции и

принципы» ДМК Пресс, 2011)
«Принцип чемоданчика»: небольшой набор абсолютно необходимых инструментов,

все остальное сделаем сами по месту => Оберон
«Принцип сундука»: для каждой базовой (да и вообще важной) технологической потребности должно быть готовое решение или легко настраиваемый полуфабрикат => Ада


Ада и Оберон – в чем разница?

Принцип сундука и принцип чемоданчика (Кауфман В.Ш. «Языки программирования. Концепции и принципы» ДМК Пресс, 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";
Атрибуты как средство запросить свойства сущностей и аспекты как средство задать свойства сущностей (от размера переменной до пред- и пост-условий для подпрограммы)


Что есть интересного в Адском сундуке?

Управление асинхронными процессами;Иерархическая модульность;Механизм подтипов (вплоть до определения произвольных множеств) и механизм исключений;subtype Basic_Letter is Character     with Static_Predicate => Basic_Letter in 'A'..'Z' | 'a'..'z' | 'Æ’ 

Слайд 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Ада изначально ориентирована на разработку встроенных систем:
Все, что можно, сдвинуто

на этап компиляции и сборки программы;
Спецификации представления – управление машинно-зависимыми

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

Ада и разработка встроенных приложений

Ада изначально ориентирована на разработку встроенных систем:Все, что можно, сдвинуто на этап компиляции и сборки программы;Спецификации представления

Слайд 11GNAT – AdaCore;
GNAT – FSF;
GNAT – от всех, кому не

лень;
Старые игроки (Rational, Aonix, DDC-I, Green Hills) все еще в

деле, но…

Ада - реализации

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

Слайд 12Образована в 1994 году преподавателями Нью-Йоркского университета;
В настоящее время –

более 100 сотрудников, головные офисы в Париже и Нью-Йорке;
Занимается разработкой

и сопровождением GNAT-технологии;
Основной продукт компании – подписка на оказание технической поддержки для пользователей GNAT-технологии;

Компания AdaCore (www.adacore.com)

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

Слайд 13GNAT = Gnu Nyu Ada Translator
AIX
PowerPC AIX (32 bits)

HP-UX
Itanium HP-UX

Linux
HP

Integrity Itanium GNU Linux
PowerPC GNU Linux (32 bits)
SGI Altix Itanium

GNU Linux
x86 GNU Linux (32 bits)
x86-64 GNU Linux (64 bits)

Mac OS X
x86-64 Mac OS X (64 bits)

Solaris
SPARC Solaris (32 bits)
SPARC Solaris (64 bits)
x86 Solaris/Trusted Solaris (32 bits)

Windows
x86 Windows (32 bits)
x86-64 Windows (64 bits)

Доступен в инструментальных средах:

GNAT = Gnu Nyu Ada TranslatorAIXPowerPC AIX (32 bits)HP-UXItanium HP-UXLinuxHP Integrity Itanium GNU LinuxPowerPC GNU Linux (32

Слайд 14GNAT – позволяет создавать код для:
Android
ARM Android (hosted on Linux)
ARM

Android (hosted on Windows)
Certified VxWorks
PowerPC VxWorks 6.x/Cert (hosted on Linux)
PowerPC

VxWorks 6.x/Cert (hosted on Windows)
PowerPC VxWorks 653 (hosted on Windows)
PowerPC VxWorks MILS (hosted on Windows)
ELF format
ARM ELF format (hosted on Linux)
ARM ELF format (hosted on Windows)
ERC32 ELF format (hosted on Linux)
ERC32 ELF format (hosted on Solaris)
LEON 2 ELF format (hosted on Linux)
LEON 2 ELF format (hosted on Solaris)
LEON 2 ELF format (hosted on Windows)
LEON 3 ELF format (hosted on Linux)
LEON 3 ELF format (hosted on Windows)
PowerPC 55xx and e500v2 ELF format (hosted on Linux)
PowerPC 55xx and e500v2 ELF format (hosted on Windows)
PowerPC ELF format (hosted on Solaris)
PowerPC ELF format (hosted on Windows)
Embedded Linux
ARM GNU Linux (32 bits) (hosted on Linux)
PowerPC ELinOS (hosted on Linux)
x86 ELinOS (hosted on Linux)
Linux
PowerPC e500v2 GNU Linux (32 bits) (hosted on Linux)
LynxOS
PowerPC LynxOS 4.x (hosted on Solaris)

PikeOS
x86 PikeOS (hosted on Linux)
VxWorks 5.x
PowerPC VxWorks 5.x (hosted on Solaris)
PowerPC VxWorks 5.x (hosted on Windows)
VxWorks 6.x
ARM VxWorks 6.x (hosted on Linux)
ARM VxWorks 6.x (hosted on Windows)
PowerPC VxWorks 6.x (hosted on Linux)
PowerPC VxWorks 6.x (hosted on Solaris)
PowerPC VxWorks 6.x (hosted on Windows)
PowerPC e500v2 VxWorks 6.x (hosted on Linux)
PowerPC e500v2 VxWorks 6.x (hosted on Solaris)
PowerPC e500v2 VxWorks 6.x (hosted on Windows)
x86 VxWorks 6.x (hosted on Linux)
x86 VxWorks 6.x (hosted on Solaris)
x86 VxWorks 6.x (hosted on Windows)
VxWorks 7.x
ARM VxWorks 7.x (hosted on Linux)
ARM VxWorks 7.x (hosted on Windows)
PowerPC VxWorks 7.x (hosted on Linux)
PowerPC VxWorks 7.x (hosted on Windows)
PowerPC e500v2 VxWorks 7.x (hosted on Linux)
PowerPC e500v2 VxWorks 7.x (hosted on Windows)
x86-64 VxWorks 7.x (64 bits) (hosted on Linux)
x86-64 VxWorks 7.x (64 bits) (hosted on Windows)
Wind River Linux
PowerPC Wind River Linux (hosted on Linux)
PowerPC e500v2 Wind River Linux (hosted on Linux)

GNAT – позволяет создавать код для:AndroidARM Android (hosted on Linux)ARM Android (hosted on Windows)Certified VxWorksPowerPC VxWorks 6.x/Cert

Слайд 15Компилятор GNAT
Ada front-end
(Написан на Аде!)
gigi (GNAT-to-GNU)
gcc code generator
Ada sources
object code
Преимущества использования gcc:
Ада

есть (может быть) везде, где есть gcc;
Многоязыковое программирование (Ада может

использоваться совместно с любым языком, реализованным в gcc);
GNAT – среда программирования для Ada/C/C++

GNAT way of using gcc:
Параноидально-консервативный: только стабильные версии, только надежные возможности;
Набор своих изменений для gcc;

Фрагменты gcc-подобного дерева, которые еще помнят Аду

Стандартное gcc-дерево, никаких следов Ады

Компилятор GNATAda  front-end(Написан на Аде!)gigi (GNAT-to-GNU)gcc code generatorAda sourcesobject codeПреимущества использования gcc:Ада есть (может быть) везде,

Слайд 16Не только компилятор Ады (поддерживается последняя версия стандарта), но и:
Компиляторы

С и С++;
Специализированные библиотеки;
Инструментарий;
Технологические решения;
SPARK (доказательное программирование);
QGen (автоматическая генерация кода

по моделям);

GNAT-технология

Не только компилятор Ады (поддерживается последняя версия стандарта), но и:Компиляторы С и С++;Специализированные библиотеки;Инструментарий;Технологические решения;SPARK (доказательное программирование);QGen

Слайд 17GNAT Pro:
Полноценная техническая поддержка;
Возможность создавать программы с закрытым кодом;
Все платформы

и все целевые среды, весь инструментарий, все компоненты технологии;
GNAT Developer:
Незначительно

ограниченная техническая поддержка;
Возможность создавать программы с закрытым кодом;
Незначительные ограничения на поддерживаемые конфигурации;
GAP (GNAT Academic Program):
Ограниченная техническая поддержка;
Возможность создавать программы только под лицензией GPL;
Все инструментальные платформы + MINDSTORMS NTX robotic + базовый инструментарий;
Бесплатно для университетов;
GNAT GPL:
То же, что и GAP, но вообще без техподдержки и бесплатно абсолютно для всех;

AdaCore - продукты

GNAT Pro:Полноценная техническая поддержка;Возможность создавать программы с закрытым кодом;Все платформы и все целевые среды, весь инструментарий, все

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

на основе моделей;
Формальная верификация программ, или корректность по построению;
Обучение, консультации,

развитие технологии на основе явных заказов пользователей;

AdaCore – технологические решения

Разработка и тестирование встроенных приложений;Поддержка разработки сертифицированных приложений;Автоматическая генерация Ада-кода на основе моделей;Формальная верификация программ, или корректность

Слайд 19Конфигурируемые библиотеки периода выполнения:
Ravenscar profile;
Zero footprint;
Bare board (возможность создавать приложения

при отсутствии ОС в целевой среде);
gnat emulator – возможность тестировать

встроенное приложение не в целевой, а в инструментальной среде;

Разработка и тестирование встроенных приложений

Конфигурируемые библиотеки периода выполнения:Ravenscar profile;Zero footprint;Bare board (возможность создавать приложения при отсутствии ОС в целевой среде);gnat emulator

Слайд 20Поддержка разработки систем, удовлетворяющих отраслевым стандартам качества:
DO-178 (встроенные авиационные системы);
EN

50128 (железные дороги);
RTCA DO-278 (управление воздушным движением);
ECSS-E-ST-40C, ECSS-Q-ST-80C – космическая

техника;
...

Разработка сертифицированных приложений

Поддержка разработки систем, удовлетворяющих отраслевым стандартам качества:DO-178 (встроенные авиационные системы);EN 50128 (железные дороги);RTCA DO-278 (управление воздушным движением);ECSS-E-ST-40C,

Слайд 21Поддержка тестирования:
gnatcoverage: автоматическая проверка выполнения критериев структурного тестирования (как на

уровне объектного кода, так и на уровне исходного кода на

языках Ада и С);
gnattest: автоматическая генерация тестовых драйверов для выполнения модульного тестирования в среде aunit;
Traceability analysis package:
рекомендации по выбору языкового подмножества, позволяющего проследить соответствие исходного и объектного кода, и нужных режимов компилятора;
набор тестов, демонстрирующих соответствие исходного и объектного кода в пределах выбранного подмножества;

Разработка сертифицированных приложений

Поддержка тестирования:gnatcoverage: автоматическая проверка выполнения критериев структурного тестирования (как на уровне объектного кода, так и на уровне

Слайд 22Инструменты статического анализа кода:
gnatcheck:
Проверка правил, типичных для стандарта кодирования;
Интеграция результатов

проверок, проводимых компилятором, в итоговый отчет;
Позволяет быстро добавлять новые правила

по заказу пользователей;
Codepeer:
Детальный анализ графа управления и графа потока данных (деление на ноль, переполнение, неопределенные и неиспользуемые переменные и т.п.);
gnatstack:
Оценка максимальной глубины стека в целевой среде;
Выявление потенциально опасных ситуаций;
Работает с кодом на Аде, С, С++.

Разработка сертифицированных приложений

Инструменты статического анализа кода:gnatcheck:Проверка правил, типичных для стандарта кодирования;Интеграция результатов проверок, проводимых компилятором, в итоговый отчет;Позволяет быстро

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

и решений;
Разработка сертифицированных приложений

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

Слайд 24QGen:
Поддерживается надежное подмножество Simulink® and Stateflow®;
Проверка корректности модели;
Возможность проследить путь

от модели к коду;
Генерация кода на SPARK и MISRA C;
Цель

– полностью квалифицированная технология для использования там, где действуют стандарты безопасности;

Автоматическая генерация Ада-кода на основе моделей

QGen:Поддерживается надежное подмножество Simulink® and Stateflow®;Проверка корректности модели;Возможность проследить путь от модели к коду;Генерация кода на SPARK

Слайд 25С чего начался SPARK:
(Успешная!) попытка практической реализации идеи формального доказательства

корректности программы;
Использование булевских аннотаций для компонент кода на Аде в

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

SPARK – формальная верификация программ

С чего начался SPARK:(Успешная!) попытка практической реализации идеи формального доказательства корректности программы;Использование булевских аннотаций для компонент кода

Слайд 26Определяемые пользователем проверки, осуществляемые при выполнении программы;
Предусловия – обязательства

того, кто вызывает подпрограмму;
Постусловия – гарантии того, что произойдет

в результате выполнения подпрограммы

Контракт как ключевая идея SPARK-подхода

Обязательство

Гарантия

procedure Push (This : in out Stack; Value : Content) with
Pre => not Full (This),
Post => not Empty (This) and Top (This) = Value;

function Top (This : Stack) return Content;
function Full (This : Stack) return Boolean;

Определяемые пользователем проверки, осуществляемые при выполнении программы; Предусловия – обязательства того, кто вызывает подпрограмму; Постусловия – гарантии

Слайд 27Если вызывающий контекст гарантирует, что предусловие вызываемой подпрограммы истинно, то

подпрограмма обеспечивает истинность пост-условия по завершению вызова;
Все пред- и пост-условия

вычисляются как часть вызова подпрограммы, и если что-либо не оказывается истинным – возбуждается исключение;

Почему это назвали контрактом?

Если вызывающий контекст гарантирует, что предусловие вызываемой подпрограммы истинно, то подпрограмма обеспечивает истинность пост-условия по завершению вызова;Все

Слайд 28package 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, будет возбуждено исключение


Инварианты типов (вишенка на торте :)

Инвариант типа:
Проверяется для любого объекта типа после любого действия, способного изменить значение объекта;
Наследуется для типов-потомков;
Может быть переопределен для типа-потомка;

package Stacks is  type Stack is private   with     Type_Invariant =>

Обратная связь

Если не удалось найти и скачать доклад-презентацию, Вы можете заказать его на нашем сайте. Мы постараемся найти нужный Вам материал и отправим по электронной почте. Не стесняйтесь обращаться к нам, если у вас возникли вопросы или пожелания:

Email: Нажмите что бы посмотреть 

Что такое TheSlide.ru?

Это сайт презентации, докладов, проектов в PowerPoint. Здесь удобно  хранить и делиться своими презентациями с другими пользователями.


Для правообладателей

Яндекс.Метрика