Предисловие

Перед вами новая редакция брошюры «Безопасное и надежное программированное обеспечение». Она включает описание новых возможностей языка для поддержки контрактного программирования. Данные новшества были введены в ревизию языка Ада 2012. Они представляют особый интерес в областях, где существуют повышенные требования к безопасности и надежности программного обеспечения, особенно когда речь заходит о сертификации программ.

Я очень благодарен Бену Брасголу (Ben Brosgol) из AdaCore за помощь в подготовке новой редакции этой брошюры. Бен не только подготовил черновик новых разделов, но также исправил некоторые неясные, вводящие в заблуждения, а то и вовсе некорректные моменты в оригинале. К тому же он подготовил всеобъемлющий индекс, который, я уверен, оценят все читатели.

Джон Барнс.

Кавершам. Англия. Январь 2013

С момента публикации предыдущей редакции этой брошюры в 2013 году произошло важное событие: был выпущен SPARK 2014. SPARK представляет собой подмножество языка Ада, позволяющее применить методы формального анализа свойств программы, например, доказать отсуствие ошибок в коде. При этом остается возможность сочетать формальные методы с традиционными методами тестирования программ. Соответствующая глава «Сертификация с помощью SPARK» была значительно переработана, чтобы отразить изменения, введенные в SPARK 2014. Мы надеемся, что эта обновленная глава воодушевит читателей познакомиться поближе с этим интереснейшим новым языком и соответствующими технологиями.