SPARK

SPARK — это формально определённый язык программирования, основанный на языке программирования Ада и предназначенный для разработки программного обеспечения высокой целостности (high integrity) для областей применения, где предсказуемость и высоконадёжное функционирование — ключевые требования. Для собственно компиляции используется компилятор языка Ada, а инструментарий SPARK предназначен для верификации поведения программы.

Не все возможности языка Ada позволяют верифицировать программы, их использущие, поэтому SPARK — в некотором смысле подмножество языка Ада. С другой стороны, SPARK требует документировать поведение программы контрактами, и эти элементы тем или иным способом вносятся в текст программы.

Первое поколение этого языка программирования представлено 3мя версиями: SPARK 83, SPARK 95 и SPARK 2005, основанные на Ada 83, Ada 95 и Ada 2005, соответственно. И отдельно идёт развитие второго поколения, начало которому положил SPARK 2014 на базе Ada 2012.

Принципиальное различие — в том, что в первом поколении контракты записывались в специальным образом оформленных комментариях языка Ada (минус минус решётка), а во втором поколении для их записи используются аспекты, прагмы и другие синтаксические элементы языка Ада. SPARK 2014 и Ada 2012 связаны более тесно. Так, компилятор языка Ada 2012 в режиме проверки утверждений (assertions) добавляет проверки пре- и постусловий методов, а верификатор языка SPARK 2014 — проверяет корректность на этапе верификации. Оборотной стороной является невозможность использования верификаторов SPARK 2014 с компиляторами языка Ada, не поддерживающими версию Ada 2012, то есть, практически со всеми, кроме GNAT.

Верификаторы для обоих поколений SPARK можно скачать на сайте AdaCore Libre, в зависимости от версии GNAT GPL. Самая новая версия верификатора первого поколения (Examiner) — в GNAT 2012 GPL, более новые — это второе поколение (GNATprove).